let I be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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); :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: verum