let I be non empty set ; :: thesis: for G being Group

for F being Subgroup-Family of I,G

for h, h0 being finite-support Function of I,G

for i being Element of I

for UFi being Subset of G st UFi = Union ((Carrier F) | (I \ {i})) & h0 = h +* (i,(1_ (F . i))) & h in product F holds

Product h0 in gr UFi

let G be Group; :: thesis: for F being Subgroup-Family of I,G

for h, h0 being finite-support Function of I,G

for i being Element of I

for UFi being Subset of G st UFi = Union ((Carrier F) | (I \ {i})) & h0 = h +* (i,(1_ (F . i))) & h in product F holds

Product h0 in gr UFi

let F be Subgroup-Family of I,G; :: thesis: for h, h0 being finite-support Function of I,G

for i being Element of I

for UFi being Subset of G st UFi = Union ((Carrier F) | (I \ {i})) & h0 = h +* (i,(1_ (F . i))) & h in product F holds

Product h0 in gr UFi

let h, h0 be finite-support Function of I,G; :: thesis: for i being Element of I

for UFi being Subset of G st UFi = Union ((Carrier F) | (I \ {i})) & h0 = h +* (i,(1_ (F . i))) & h in product F holds

Product h0 in gr UFi

let i be Element of I; :: thesis: for UFi being Subset of G st UFi = Union ((Carrier F) | (I \ {i})) & h0 = h +* (i,(1_ (F . i))) & h in product F holds

Product h0 in gr UFi

let UFi be Subset of G; :: thesis: ( UFi = Union ((Carrier F) | (I \ {i})) & h0 = h +* (i,(1_ (F . i))) & h in product F implies Product h0 in gr UFi )

assume that

A1: UFi = Union ((Carrier F) | (I \ {i})) and

A2: h0 = h +* (i,(1_ (F . i))) and

A3: h in product F ; :: thesis: Product h0 in gr UFi

set CFi = (Carrier F) | (I \ {i});

dom (Carrier F) = I by PARTFUN1:def 2;

then A4: dom ((Carrier F) | (I \ {i})) = I \ {i} by RELAT_1:62;

for y being object st y in rng h0 holds

y in [#] (gr UFi)

then reconsider x0 = h0 as finite-support Function of I,(gr UFi) by Th5;

Product x0 = Product h0 by Th6;

hence Product h0 in gr UFi ; :: thesis: verum

for F being Subgroup-Family of I,G

for h, h0 being finite-support Function of I,G

for i being Element of I

for UFi being Subset of G st UFi = Union ((Carrier F) | (I \ {i})) & h0 = h +* (i,(1_ (F . i))) & h in product F holds

Product h0 in gr UFi

let G be Group; :: thesis: for F being Subgroup-Family of I,G

for h, h0 being finite-support Function of I,G

for i being Element of I

for UFi being Subset of G st UFi = Union ((Carrier F) | (I \ {i})) & h0 = h +* (i,(1_ (F . i))) & h in product F holds

Product h0 in gr UFi

let F be Subgroup-Family of I,G; :: thesis: for h, h0 being finite-support Function of I,G

for i being Element of I

for UFi being Subset of G st UFi = Union ((Carrier F) | (I \ {i})) & h0 = h +* (i,(1_ (F . i))) & h in product F holds

Product h0 in gr UFi

let h, h0 be finite-support Function of I,G; :: thesis: for i being Element of I

for UFi being Subset of G st UFi = Union ((Carrier F) | (I \ {i})) & h0 = h +* (i,(1_ (F . i))) & h in product F holds

Product h0 in gr UFi

let i be Element of I; :: thesis: for UFi being Subset of G st UFi = Union ((Carrier F) | (I \ {i})) & h0 = h +* (i,(1_ (F . i))) & h in product F holds

Product h0 in gr UFi

let UFi be Subset of G; :: thesis: ( UFi = Union ((Carrier F) | (I \ {i})) & h0 = h +* (i,(1_ (F . i))) & h in product F implies Product h0 in gr UFi )

assume that

A1: UFi = Union ((Carrier F) | (I \ {i})) and

A2: h0 = h +* (i,(1_ (F . i))) and

A3: h in product F ; :: thesis: Product h0 in gr UFi

set CFi = (Carrier F) | (I \ {i});

dom (Carrier F) = I by PARTFUN1:def 2;

then A4: dom ((Carrier F) | (I \ {i})) = I \ {i} by RELAT_1:62;

for y being object st y in rng h0 holds

y in [#] (gr UFi)

proof

then
rng h0 c= [#] (gr UFi)
;
let y be object ; :: thesis: ( y in rng h0 implies y in [#] (gr UFi) )

assume y in rng h0 ; :: thesis: y in [#] (gr UFi)

then consider j being Element of I such that

A5: y = h0 . j by FUNCT_2:113;

end;assume y in rng h0 ; :: thesis: y in [#] (gr UFi)

then consider j being Element of I such that

A5: y = h0 . j by FUNCT_2:113;

per cases
( j <> i or j = i )
;

end;

suppose A6:
j <> i
; :: thesis: y in [#] (gr UFi)

then
not j in {i}
by TARSKI:def 1;

then A7: j in dom ((Carrier F) | (I \ {i})) by A4, XBOOLE_0:def 5;

A8: h0 . j = h . j by A2, A6, FUNCT_7:32;

h . j in F . j by A3, GROUP_19:5;

then h . j in [#] (F . j) ;

then h . j in (Carrier F) . j by PENCIL_3:7;

then A9: h0 . j in ((Carrier F) | (I \ {i})) . j by A7, A8, FUNCT_1:47;

((Carrier F) | (I \ {i})) . j c= union (rng ((Carrier F) | (I \ {i}))) by A7, FUNCT_1:3, ZFMISC_1:74;

then A10: ((Carrier F) | (I \ {i})) . j c= UFi by A1, CARD_3:def 4;

UFi c= [#] (gr UFi) by GROUP_4:def 4;

hence y in [#] (gr UFi) by A5, A9, A10; :: thesis: verum

end;then A7: j in dom ((Carrier F) | (I \ {i})) by A4, XBOOLE_0:def 5;

A8: h0 . j = h . j by A2, A6, FUNCT_7:32;

h . j in F . j by A3, GROUP_19:5;

then h . j in [#] (F . j) ;

then h . j in (Carrier F) . j by PENCIL_3:7;

then A9: h0 . j in ((Carrier F) | (I \ {i})) . j by A7, A8, FUNCT_1:47;

((Carrier F) | (I \ {i})) . j c= union (rng ((Carrier F) | (I \ {i}))) by A7, FUNCT_1:3, ZFMISC_1:74;

then A10: ((Carrier F) | (I \ {i})) . j c= UFi by A1, CARD_3:def 4;

UFi c= [#] (gr UFi) by GROUP_4:def 4;

hence y in [#] (gr UFi) by A5, A9, A10; :: thesis: verum

then reconsider x0 = h0 as finite-support Function of I,(gr UFi) by Th5;

Product x0 = Product h0 by Th6;

hence Product h0 in gr UFi ; :: thesis: verum