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

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