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