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 (() | (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 (() | (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 (() | (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 (() | (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 (() | (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 (() | (I \ {i})) & h0 = h +* (i,(1_ (F . i))) & h in product F implies Product h0 in gr UFi )
assume that
A1: UFi = Union (() | (I \ {i})) and
A2: h0 = h +* (i,(1_ (F . i))) and
A3: h in product F ; :: thesis: Product h0 in gr UFi
set CFi = () | (I \ {i});
dom () = I by PARTFUN1:def 2;
then A4: dom (() | (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 (() | (I \ {i})) by ;
A8: h0 . j = h . j by ;
h . j in F . j by ;
then h . j in [#] (F . j) ;
then h . j in () . j by PENCIL_3:7;
then A9: h0 . j in (() | (I \ {i})) . j by ;
((Carrier F) | (I \ {i})) . j c= union (rng (() | (I \ {i}))) by ;
then A10: ((Carrier F) | (I \ {i})) . j c= UFi by ;
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 ;
then A12: h0 . j = 1_ (F . j) by ;
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 ; :: 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