let I be non empty set ; :: thesis: for G being Group
for F being Group-Family of I
for x being Function of I,G st x in product F holds
x is Function of I,(Union (Carrier F))
let G be Group; :: thesis: for F being Group-Family of I
for x being Function of I,G st x in product F holds
x is Function of I,(Union (Carrier F))
let F be Group-Family of I; :: thesis: for x being Function of I,G st x in product F holds
x is Function of I,(Union (Carrier F))
let x be Function of I,G; :: thesis: ( x in product F implies x is Function of I,(Union (Carrier F)) )
assume A1: x in product F ; :: thesis: x is Function of I,(Union (Carrier F))
A2: dom (Carrier F) = I by PARTFUN1:def 2;
for z being object st z in rng x holds
z in Union (Carrier F)

proof

let z be object ; :: thesis: ( z in rng x implies z in Union (Carrier F) )
assume z in rng x ; :: thesis: z in Union (Carrier F)
then consider i being object such that
A3: ( i in I & z = x . i ) by FUNCT_2:11;
reconsider i = i as Element of I by A3;
x . i in F . i by A1, GROUP_19:5;
then z in [#] (F . i) by A3;
then A4: z in (Carrier F) . i by PENCIL_3:7;
(Carrier F) . i in rng (Carrier F) by A2, FUNCT_1:3;
then z in union (rng (Carrier F)) by A4, TARSKI:def 4;
hence z in Union (Carrier F) by CARD_3:def 4; :: thesis: verum

end;

then rng x c= Union (Carrier F) ;
hence x is Function of I,(Union (Carrier F)) by FUNCT_2:6; :: thesis: verum