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)

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

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

then
rng x c= Union (Carrier F)
;
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;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

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