let g be Element of (product F); :: thesis: ( g is I -defined & g is the carrier of G -valued & g is total )
A1: dom g = I by GROUP_19:3;
for y being object st y in rng g holds
y in the carrier of G

proof

let y be object ; :: thesis: ( y in rng g implies y in the carrier of G )
assume y in rng g ; :: thesis: y in the carrier of G
then consider i0 being object such that
A3: ( i0 in dom g & y = g . i0 ) by FUNCT_1:def 3;
reconsider i = i0 as Element of I by A3;
g in product F ;
then y in F . i by A3, GROUP_19:5;
then y in G by GROUP_2:40;
hence y in the carrier of G ; :: thesis: verum

end;

hence ( g is I -defined & g is the carrier of G -valued & g is total ) by A1, PARTFUN1:def 2, TARSKI:def 3, RELAT_1:def 19; :: thesis: verum