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 S_{1}[ 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: S_{1}[ 0 ]
_{1}[k] holds

S_{1}[k + 1]
_{1}[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: Product f = Product g

len f is Nat ;

hence Product f = Product g by A13, A12; :: thesis: verum

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 S

for g being FinSequence of H st $1 = len f & f = g holds

Product f = Product g;

A1: S

proof

A4:
for k being Nat st S
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: Product f = Product g

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 A3, GROUP_2:44; :: thesis: verum

end;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: Product f = Product g

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 A3, GROUP_2:44; :: thesis: verum

S

proof

A12:
for k being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A5: S_{1}[k]
; :: thesis: S_{1}[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: Product f = Product g

A7: k + 1 in Seg (k + 1) by FINSEQ_1:4;

then k + 1 in dom f by A6, FINSEQ_1:def 3;

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 A7, A6, FINSEQ_1:def 3;

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 A6, RFINSEQ:7;

A9: g = g1 ^ <*ag*> by A6, RFINSEQ:7;

A10: Product f = (Product f1) * af by GROUP_4:6, A8;

A11: Product g = (Product g1) * ag by GROUP_4:6, A9;

len f1 = k by FINSEQ_1:59, A6, NAT_1:11;

then Product f1 = Product g1 by A6, A5;

hence Product f = Product g by A10, A11, GROUP_2:43, A6; :: thesis: verum

end;assume A5: S

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: Product f = Product g

A7: k + 1 in Seg (k + 1) by FINSEQ_1:4;

then k + 1 in dom f by A6, FINSEQ_1:def 3;

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 A7, A6, FINSEQ_1:def 3;

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 A6, RFINSEQ:7;

A9: g = g1 ^ <*ag*> by A6, RFINSEQ:7;

A10: Product f = (Product f1) * af by GROUP_4:6, A8;

A11: Product g = (Product g1) * ag by GROUP_4:6, A9;

len f1 = k by FINSEQ_1:59, A6, NAT_1:11;

then Product f1 = Product g1 by A6, A5;

hence Product f = Product g by A10, A11, GROUP_2:43, A6; :: thesis: verum

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: Product f = Product g

len f is Nat ;

hence Product f = Product g by A13, A12; :: thesis: verum