let I be set ; :: thesis: for G being Group
for F being Subgroup-Family of I,G holds Carrier F is bool the carrier of G -valued
let G be Group; :: thesis: for F being Subgroup-Family of I,G holds Carrier F is bool the carrier of G -valued
let F be Subgroup-Family of I,G; :: thesis: Carrier F is bool the carrier of G -valued

per cases ( I is empty or not I is empty ) ;

suppose I is empty ; :: thesis: Carrier F is bool the carrier of G -valued

then A1: Carrier F = {} ;
( rng {} = {} & {} c= bool the carrier of G ) by XBOOLE_1:2;
hence Carrier F is bool the carrier of G -valued by A1, RELAT_1:def 19; :: thesis: verum

end;

suppose not I is empty ; :: thesis: Carrier F is bool the carrier of G -valued

then reconsider I = I as non empty set ;
reconsider F = F as Subgroup-Family of I,G ;
for z being object st z in rng (Carrier F) holds
z in bool the carrier of G

proof

let z be object ; :: thesis: ( z in rng (Carrier F) implies z in bool the carrier of G )
assume A3: z in rng (Carrier F) ; :: thesis: z in bool the carrier of G
reconsider y = z as set by TARSKI:1;
consider i being object such that
A4: ( i in dom (Carrier F) & y = (Carrier F) . i ) by A3, FUNCT_1:def 3;
reconsider i = i as Element of I by A4;
y = the carrier of (F . i) by A4, Th9;
then y c= the carrier of G by GROUP_2:def 5;
hence z in bool the carrier of G by ZFMISC_1:def 1; :: thesis: verum

end;

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

end;

end;