let g be Element of F; :: thesis: g is the carrier of G -valued
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 i being Element of I such that
A1: y = g . i by MssRng;
g . i is Element of (F . i) by EltGF;
then g . i is Element of G by GROUP_2:42;
hence y in the carrier of G by A1; :: thesis: verum

end;

hence g is the carrier of G -valued by RELAT_1:def 19, TARSKI:def 3; :: thesis: verum