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 ())

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 ())

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 ())

let x be Function of I,G; :: thesis: ( x in product F implies x is Function of I,(Union ()) )
assume A1: x in product F ; :: thesis: x is Function of I,(Union ())
A2: dom () = I by PARTFUN1:def 2;
for z being object st z in rng x holds
z in Union ()
proof
let z be object ; :: thesis: ( z in rng x implies z in Union () )
assume z in rng x ; :: thesis: z in Union ()
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 ;
then z in [#] (F . i) by A3;
then A4: z in () . i by PENCIL_3:7;
(Carrier F) . i in rng () by ;
then z in union (rng ()) by ;
hence z in Union () by CARD_3:def 4; :: thesis: verum
end;
then rng x c= Union () ;
hence x is Function of I,(Union ()) by FUNCT_2:6; :: thesis: verum