let I be non empty set ; 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; 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; 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; 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; 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; ( 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
; 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 ;
( y in rng h0 implies y in [#] (gr UFi) )
assume
y in rng h0
;
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
;
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;
verum 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
; verum