set f = dprod2prod F;
set h = (dprod2prod F) | (dsum F);
A1: [#] (dsum F) c= [#] (dprod F) by GROUP_2:def 5;
reconsider h = (dprod2prod F) | (dsum F) as Function of (dsum F),(product (Union F)) ;
A2: [#] (sum (Union F)) c= [#] (product (Union F)) by GROUP_2:def 5;
rng h = [#] (sum (Union F)) by Th33;
then reconsider h = h as Function of (dsum F),(sum (Union F)) by FUNCT_2:6;
for a, b being Element of (dsum F) holds h . (a * b) = (h . a) * (h . b)

proof

let a, b be Element of (dsum F); :: thesis: h . (a * b) = (h . a) * (h . b)
reconsider a0 = a, b0 = b as Element of (dprod F) by A1;
reconsider ha = h . a, hb = h . b as Element of (product (Union F)) by A2;
A3: ( ha = (dprod2prod F) . a0 & hb = (dprod2prod F) . b0 ) by FUNCT_1:49;
h . (a * b) = (dprod2prod F) . (a * b) by FUNCT_1:49
.= (dprod2prod F) . (a0 * b0) by GROUP_2:43
.= ha * hb by A3, GROUP_6:def 6
.= (h . a) * (h . b) by GROUP_2:43 ;
hence h . (a * b) = (h . a) * (h . b) ; :: thesis: verum

end;

hence (dprod2prod F) | (dsum F) is Homomorphism of (dsum F),(sum (Union F)) by GROUP_6:def 6; :: thesis: verum