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 y being finite-support Function of I,(gr UF)
for i being Element of I
for g being Element of (gr UF) st y in product F & y . i = 1_ (F . i) & g in F . i holds
(Product y) * g = g * (Product y)
let G be Group; :: thesis: for F being component-commutative Subgroup-Family of I,G
for UF being Subset of G
for y being finite-support Function of I,(gr UF)
for i being Element of I
for g being Element of (gr UF) st y in product F & y . i = 1_ (F . i) & g in F . i holds
(Product y) * g = g * (Product y)
let F be component-commutative Subgroup-Family of I,G; :: thesis: for UF being Subset of G
for y being finite-support Function of I,(gr UF)
for i being Element of I
for g being Element of (gr UF) st y in product F & y . i = 1_ (F . i) & g in F . i holds
(Product y) * g = g * (Product y)
let UF be Subset of G; :: thesis: for y being finite-support Function of I,(gr UF)
for i being Element of I
for g being Element of (gr UF) st y in product F & y . i = 1_ (F . i) & g in F . i holds
(Product y) * g = g * (Product y)
let y be finite-support Function of I,(gr UF); :: thesis: for i being Element of I
for g being Element of (gr UF) st y in product F & y . i = 1_ (F . i) & g in F . i holds
(Product y) * g = g * (Product y)
let i be Element of I; :: thesis: for g being Element of (gr UF) st y in product F & y . i = 1_ (F . i) & g in F . i holds
(Product y) * g = g * (Product y)
let g be Element of (gr UF); :: thesis: ( y in product F & y . i = 1_ (F . i) & g in F . i implies (Product y) * g = g * (Product y) )
assume that
A1: y in product F and
A2: y . i = 1_ (F . i) and
A3: g in F . i ; :: thesis: (Product y) * g = g * (Product y)
reconsider x = y +* (i,g) as finite-support Function of I,(gr UF) by GROUP_19:26;
A4: y = x +* (i,(1_ (F . i))) by A2, Th7;
A5: x in product F by A1, A3, GROUP_19:24;
dom y = I by PARTFUN1:def 2;
then x . i = g by FUNCT_7:31;
hence (Product y) * g = g * (Product y) by A4, A5, Th9; :: thesis: verum