let I be non empty set ; for G being Group
for F being component-commutative Subgroup-Family of I,G
for UF being Subset of G
for i being Element of I
for x, y being finite-support Function of I,(gr UF) st y = x +* (i,(1_ (F . i))) & x in product F holds
( Product x = (Product y) * (x . i) & (Product y) * (x . i) = (x . i) * (Product y) )
let G be Group; for F being component-commutative Subgroup-Family of I,G
for UF being Subset of G
for i being Element of I
for x, y being finite-support Function of I,(gr UF) st y = x +* (i,(1_ (F . i))) & x in product F holds
( Product x = (Product y) * (x . i) & (Product y) * (x . i) = (x . i) * (Product y) )
let F be component-commutative Subgroup-Family of I,G; for UF being Subset of G
for i being Element of I
for x, y being finite-support Function of I,(gr UF) st y = x +* (i,(1_ (F . i))) & x in product F holds
( Product x = (Product y) * (x . i) & (Product y) * (x . i) = (x . i) * (Product y) )
let UF be Subset of G; for i being Element of I
for x, y being finite-support Function of I,(gr UF) st y = x +* (i,(1_ (F . i))) & x in product F holds
( Product x = (Product y) * (x . i) & (Product y) * (x . i) = (x . i) * (Product y) )
let i be Element of I; for x, y being finite-support Function of I,(gr UF) st y = x +* (i,(1_ (F . i))) & x in product F holds
( Product x = (Product y) * (x . i) & (Product y) * (x . i) = (x . i) * (Product y) )
let x, y be finite-support Function of I,(gr UF); ( y = x +* (i,(1_ (F . i))) & x in product F implies ( Product x = (Product y) * (x . i) & (Product y) * (x . i) = (x . i) * (Product y) ) )
assume that
A1:
y = x +* (i,(1_ (F . i)))
and
A2:
x in product F
; ( Product x = (Product y) * (x . i) & (Product y) * (x . i) = (x . i) * (Product y) )
reconsider x0 = x, y0 = y as finite-support Function of I,G by Th4;
A3:
Product x = Product x0
by Th6;
A4:
Product y = Product y0
by Th6;
A5:
( Product x0 = (Product y0) * (x0 . i) & (Product y0) * (x0 . i) = (x0 . i) * (Product y0) )
by A1, A2, Th8;
then
Product x = (Product y) * (x . i)
by A3, A4, GROUP_2:43;
hence
( Product x = (Product y) * (x . i) & (Product y) * (x . i) = (x . i) * (Product y) )
by A3, A4, A5, GROUP_2:43; verum