set f = trans_sum (F,a);
A2: trans_sum (F,a) = (trans_prod (F,a)) | (sum F) by A1, Def3;
rng (trans_sum (F,a)) c= [#] (sum (F * a)) ;
hence trans_sum (F,a) is Homomorphism of (sum F),(sum (F * a)) by A2, Th11; :: thesis: verum