let I be non empty set ; :: thesis: for G being Group

for H being Subgroup of G

for x being finite-support Function of I,G

for y being finite-support Function of I,H st x = y holds

Product x = Product y

let G be Group; :: thesis: for H being Subgroup of G

for x being finite-support Function of I,G

for y being finite-support Function of I,H st x = y holds

Product x = Product y

let H be Subgroup of G; :: thesis: for x being finite-support Function of I,G

for y being finite-support Function of I,H st x = y holds

Product x = Product y

let x be finite-support Function of I,G; :: thesis: for y being finite-support Function of I,H st x = y holds

Product x = Product y

let y be finite-support Function of I,H; :: thesis: ( x = y implies Product x = Product y )

assume A1: x = y ; :: thesis: Product x = Product y

then A2: support x = support y by Th3;

reconsider fx = (x | (support x)) * (canFS (support x)) as FinSequence of G by FINSEQ_2:32;

reconsider fy = (y | (support y)) * (canFS (support y)) as FinSequence of H by FINSEQ_2:32;

thus Product x = Product fx by GROUP_17:def 1

.= Product fy by A1, A2, GROUP_19:45

.= Product y by GROUP_17:def 1 ; :: thesis: verum

for H being Subgroup of G

for x being finite-support Function of I,G

for y being finite-support Function of I,H st x = y holds

Product x = Product y

let G be Group; :: thesis: for H being Subgroup of G

for x being finite-support Function of I,G

for y being finite-support Function of I,H st x = y holds

Product x = Product y

let H be Subgroup of G; :: thesis: for x being finite-support Function of I,G

for y being finite-support Function of I,H st x = y holds

Product x = Product y

let x be finite-support Function of I,G; :: thesis: for y being finite-support Function of I,H st x = y holds

Product x = Product y

let y be finite-support Function of I,H; :: thesis: ( x = y implies Product x = Product y )

assume A1: x = y ; :: thesis: Product x = Product y

then A2: support x = support y by Th3;

reconsider fx = (x | (support x)) * (canFS (support x)) as FinSequence of G by FINSEQ_2:32;

reconsider fy = (y | (support y)) * (canFS (support y)) as FinSequence of H by FINSEQ_2:32;

thus Product x = Product fx by GROUP_17:def 1

.= Product fy by A1, A2, GROUP_19:45

.= Product y by GROUP_17:def 1 ; :: thesis: verum