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)

proof

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;

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

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;

suppose A11: j = i ; :: thesis: y in [#] (gr UFi)

dom h = I by A3, GROUP_19:3;
then A12: h0 . j = 1_ (F . j) by A2, A11, FUNCT_7:31;
F . j is Subgroup of G by Def1;
then 1_ (F . j) = 1_ (gr UFi) by GROUP_2:45;
hence y in [#] (gr UFi) by A5, A12; :: thesis: verum

end;

end;

end;

then rng h0 c= [#] (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