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₁ -valued total Function
for x0 being I -defined the carrier of b₂ -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₁ -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