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
() * g = g * ()

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
() * g = g * ()

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
() * g = g * ()

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
() * g = g * ()

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
() * g = g * ()

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
() * g = g * ()

let g be Element of (gr UF); :: thesis: ( y in product F & y . i = 1_ (F . i) & g in F . i implies () * g = g * () )
assume that
A1: y in product F and
A2: y . i = 1_ (F . i) and
A3: g in F . i ; :: thesis: () * g = g * ()
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 ;
A5: x in product F by ;
dom y = I by PARTFUN1:def 2;
then x . i = g by FUNCT_7:31;
hence (Product y) * g = g * () by A4, A5, Th9; :: thesis: verum