let G be Group; :: thesis: for H being Subgroup of G
for f being FinSequence of G
for g being FinSequence of H st f = g holds
Product f = Product g

let H be Subgroup of G; :: thesis: for f being FinSequence of G
for g being FinSequence of H st f = g holds
Product f = Product g

defpred S1[ Nat] means for f being FinSequence of G
for g being FinSequence of H st \$1 = len f & f = g holds
Product f = Product g;
A1: S1[ 0 ]
proof
let f be FinSequence of G; :: thesis: for g being FinSequence of H st 0 = len f & f = g holds
Product f = Product g

let g be FinSequence of H; :: thesis: ( 0 = len f & f = g implies Product f = Product g )
assume A2: ( 0 = len f & f = g ) ; :: thesis:
then f = <*> the carrier of G ;
then A3: Product f = 1_ G by GROUP_4:8;
g = <*> the carrier of H by A2;
then Product g = 1_ H by GROUP_4:8;
hence Product f = Product g by ; :: thesis: verum
end;
A4: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A5: S1[k] ; :: thesis: S1[k + 1]
let f be FinSequence of G; :: thesis: for g being FinSequence of H st k + 1 = len f & f = g holds
Product f = Product g

let g be FinSequence of H; :: thesis: ( k + 1 = len f & f = g implies Product f = Product g )
assume A6: ( k + 1 = len f & f = g ) ; :: thesis:
A7: k + 1 in Seg (k + 1) by FINSEQ_1:4;
then k + 1 in dom f by ;
then f . (k + 1) in rng f by FUNCT_1:3;
then reconsider af = f . (k + 1) as Element of G ;
k + 1 in dom g by ;
then g . (k + 1) in rng g by FUNCT_1:3;
then reconsider ag = g . (k + 1) as Element of H ;
reconsider f1 = f | k as FinSequence of G ;
reconsider g1 = g | k as FinSequence of H ;
A8: f = f1 ^ <*af*> by ;
A9: g = g1 ^ <*ag*> by ;
A10: Product f = (Product f1) * af by ;
A11: Product g = (Product g1) * ag by ;
len f1 = k by ;
then Product f1 = Product g1 by A6, A5;
hence Product f = Product g by ; :: thesis: verum
end;
A12: for k being Nat holds S1[k] from NAT_1:sch 2(A1, A4);
let f be FinSequence of G; :: thesis: for g being FinSequence of H st f = g holds
Product f = Product g

let g be FinSequence of H; :: thesis: ( f = g implies Product f = Product g )
assume A13: f = g ; :: thesis:
len f is Nat ;
hence Product f = Product g by ; :: thesis: verum