9.4.1 - proof by induction over as

Induction base:
    Suppose as = []. Then we have:

    map f (as ++ bs)                        // assumption as = []
    = map f ([] ++ bs)                      // definition of ++, rule 1
    = map f bs                              // definition of ++, rule 1
    = [] ++ (map f bs)                      // definition of map, rule 3
    = (map f []) ++ (map f bs)              // assumption as = []
    = (map f as) ++ (map f bs).

Induction step:
    Suppose map f (as ++ bs) = (map f as) ++ (map f bs) for certain as and any bs (induction hypothesis). Then we have:
    
    map f ([a:as] ++ bs)                    // definition of ++, rule 2
    = map f [a:as ++ bs]                    // definition of map, rule 4
    = [f a : map f (as ++ bs)]              // induction hypothesis: assumption map f (as ++ bs) = (map f as) ++ (map f bs)
    = [f a : (map f as) ++ (map f bs)]      // rewriting list
    = [f a : map f as] ++ (map f bs)        // definition of map, rule 4
    = (map f [a:as]) ++ (map f bs).

By the principle of induction we have now proven that map f (as ++ bs) = (map f as) ++ (map f bs) for any finite lists as, bs.