defpred S₁[ Nat] means for f being FinSequence of F_Complex
for g being FinSequence of REAL st len f = len g & ( for i being Element of NAT st i in dom f holds
|.(f /. i).| = g . i ) & $1 = len f holds
|.(Product f).| = Product g;
set FC = F_Complex ;
set cFC = the carrier of F_Complex;
A1: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A2: S₁[i] ; :: thesis: S₁[i + 1]
let f be FinSequence of F_Complex; :: thesis: for g being FinSequence of REAL st len f = len g & ( for i being Element of NAT st i in dom f holds
|.(f /. i).| = g . i ) & i + 1 = len f holds
|.(Product f).| = Product g
let g be FinSequence of REAL ; :: thesis: ( len f = len g & ( for i being Element of NAT st i in dom f holds
|.(f /. i).| = g . i ) & i + 1 = len f implies |.(Product f).| = Product g )
assume that
A3: len f = len g and
A4: for i being Element of NAT st i in dom f holds
|.(f /. i).| = g . i and
A5: i + 1 = len f ; :: thesis: |.(Product f).| = Product g
consider g1 being FinSequence of REAL , r being Element of REAL such that
A6: g = g1 ^ <*r*> by A3, A5, FINSEQ_2:19;
A7: len g = (len g1) + (len <*r*>) by A6, FINSEQ_1:22
.= (len g1) + 1 by FINSEQ_1:39 ;
then A8: g . (len f) = r by A3, A6, FINSEQ_1:42;
consider f1 being FinSequence of F_Complex, c being Element of the carrier of F_Complex such that
A9: f = f1 ^ <*c*> by A5, FINSEQ_2:19;
A10: len f = (len f1) + (len <*c*>) by A9, FINSEQ_1:22
.= (len f1) + 1 by FINSEQ_1:39 ;
then A11: dom f1 = dom g1 by A3, A7, FINSEQ_3:29;

A12: now :: thesis: for i being Element of NAT st i in dom f1 holds
|.(f1 /. i).| = g1 . i

let i be Element of NAT ; :: thesis: ( i in dom f1 implies |.(f1 /. i).| = g1 . i )
A13: dom f1 c= dom f by A9, FINSEQ_1:26;
assume A14: i in dom f1 ; :: thesis: |.(f1 /. i).| = g1 . i
then f1 /. i = f1 . i by PARTFUN1:def 6
.= f . i by A9, A14, FINSEQ_1:def 7
.= f /. i by A14, A13, PARTFUN1:def 6 ;
hence |.(f1 /. i).| = g . i by A4, A14, A13
.= g1 . i by A6, A11, A14, FINSEQ_1:def 7 ;
:: thesis: verum

end;

reconsider Pf1 = Product f1 as Element of COMPLEX by COMPLFLD:def 1;
A15: Product g = (Product g1) * r by A6, RVSUM_1:96;
reconsider cc = c as Element of COMPLEX by COMPLFLD:def 1;
f <> {} by A5;
then A16: len f in dom f by FINSEQ_5:6;
then f /. (len f) = f . (len f) by PARTFUN1:def 6
.= c by A9, A10, FINSEQ_1:42 ;
then A17: |.cc.| = r by A4, A16, A8;
Product f = (Product f1) * c by A9, GROUP_4:6;
hence |.(Product f).| = |.Pf1.| * |.cc.| by COMPLEX1:65
.= Product g by A2, A3, A5, A15, A10, A7, A12, A17 ;
:: thesis: verum

end;

A18: S₁[ 0 ]

proof

let f be FinSequence of F_Complex; :: thesis: for g being FinSequence of REAL st len f = len g & ( for i being Element of NAT st i in dom f holds
|.(f /. i).| = g . i ) & 0 = len f holds
|.(Product f).| = Product g
let g be FinSequence of REAL ; :: thesis: ( len f = len g & ( for i being Element of NAT st i in dom f holds
|.(f /. i).| = g . i ) & 0 = len f implies |.(Product f).| = Product g )
assume that
A19: len f = len g and
for i being Element of NAT st i in dom f holds
|.(f /. i).| = g . i and
A20: 0 = len f ; :: thesis: |.(Product f).| = Product g
A21: f = <*> the carrier of F_Complex by A20;
then A22: g = <*> the carrier of F_Complex by A19;
Product f = 1r by A21, COMPLFLD:8, GROUP_4:8;
hence |.(Product f).| = Product g by A22, COMPLEX1:48, RVSUM_1:94; :: thesis: verum

end;

A23: for i being Nat holds S₁[i] from NAT_1:sch 2(A18, A1);
let f be FinSequence of F_Complex; :: thesis: for g being FinSequence of REAL st len f = len g & ( for i being Element of NAT st i in dom f holds
|.(f /. i).| = g . i ) holds
|.(Product f).| = Product g
let g be FinSequence of REAL ; :: thesis: ( len f = len g & ( for i being Element of NAT st i in dom f holds
|.(f /. i).| = g . i ) implies |.(Product f).| = Product g )
assume ( len f = len g & ( for i being Element of NAT st i in dom f holds
|.(f /. i).| = g . i ) ) ; :: thesis: |.(Product f).| = Product g
hence |.(Product f).| = Product g by A23; :: thesis: verum