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

for H being Subgroup of G

for x being I -defined the carrier of b_{1} -valued total Function

for x0 being I -defined the carrier of b_{2} -valued total Function st x = x0 holds

Product x = Product x0

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

for x being I -defined the carrier of G -valued total Function

for x0 being I -defined the carrier of b_{1} -valued total Function st x = x0 holds

Product x = Product x0

let H be Subgroup of G; :: thesis: for x being I -defined the carrier of G -valued total Function

for x0 being I -defined the carrier of H -valued total Function st x = x0 holds

Product x = Product x0

let x be I -defined the carrier of G -valued total Function; :: thesis: for x0 being I -defined the carrier of H -valued total Function st x = x0 holds

Product x = Product x0

let x0 be I -defined the carrier of H -valued total Function; :: thesis: ( x = x0 implies Product x = Product x0 )

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

consider f being FinSequence of G such that

A2: ( Product x = Product f & f = x * (canFS I) ) by Def1;

consider g being FinSequence of the carrier of H such that

A3: ( Product x0 = Product g & g = x0 * (canFS I) ) by Def1;

thus Product x = Product x0 by A2, A1, A3, Th31; :: thesis: verum

for H being Subgroup of G

for x being I -defined the carrier of b

for x0 being I -defined the carrier of b

Product x = Product x0

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

for x being I -defined the carrier of G -valued total Function

for x0 being I -defined the carrier of b

Product x = Product x0

let H be Subgroup of G; :: thesis: for x being I -defined the carrier of G -valued total Function

for x0 being I -defined the carrier of H -valued total Function st x = x0 holds

Product x = Product x0

let x be I -defined the carrier of G -valued total Function; :: thesis: for x0 being I -defined the carrier of H -valued total Function st x = x0 holds

Product x = Product x0

let x0 be I -defined the carrier of H -valued total Function; :: thesis: ( x = x0 implies Product x = Product x0 )

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

consider f being FinSequence of G such that

A2: ( Product x = Product f & f = x * (canFS I) ) by Def1;

consider g being FinSequence of the carrier of H such that

A3: ( Product x0 = Product g & g = x0 * (canFS I) ) by Def1;

thus Product x = Product x0 by A2, A1, A3, Th31; :: thesis: verum