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:
then A2: support x = support y by Th3;
reconsider fx = (x | ()) * (canFS ()) as FinSequence of G by FINSEQ_2:32;
reconsider fy = (y | ()) * (canFS ()) as FinSequence of H by FINSEQ_2:32;
thus Product x = Product fx by GROUP_17:def 1
.= Product fy by
.= Product y by GROUP_17:def 1 ; :: thesis: verum