defpred S1[ 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 g;
set FC = F_Complex ;
set cFC = the carrier of F_Complex;
A1: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A2: S1[i] ; :: thesis: S1[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 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 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 g
consider g1 being FinSequence of REAL , r being Element of REAL such that
A6: g = g1 ^ <*r*> by ;
A7: len g = (len g1) + () by
.= (len g1) + 1 by FINSEQ_1:39 ;
then A8: g . (len f) = r by ;
consider f1 being FinSequence of F_Complex, c being Element of the carrier of F_Complex such that
A9: f = f1 ^ <*c*> by ;
A10: len f = (len f1) + () by
.= (len f1) + 1 by FINSEQ_1:39 ;
then A11: dom f1 = dom g1 by ;
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 ;
assume A14: i in dom f1 ; :: thesis: |.(f1 /. i).| = g1 . i
then f1 /. i = f1 . i by PARTFUN1:def 6
.= f . i by
.= f /. i by ;
hence |.(f1 /. i).| = g . i by A4, A14, A13
.= g1 . i by ;
:: thesis: verum
end;
reconsider Pf1 = Product f1 as Element of COMPLEX by COMPLFLD:def 1;
A15: Product g = (Product g1) * r by ;
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 ;
then A17: |.cc.| = r by A4, A16, A8;
Product f = (Product f1) * c by ;
hence |.().| = |.Pf1.| * |.cc.| by COMPLEX1:65
.= Product g by A2, A3, A5, A15, A10, A7, A12, A17 ;
:: thesis: verum
end;
A18: S1[ 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 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 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 g
A21: f = <*> the carrier of F_Complex by A20;
then A22: g = <*> the carrier of F_Complex by A19;
Product f = 1r by ;
hence |.().| = Product g by ; :: thesis: verum
end;
A23: for i being Nat holds S1[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 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 g )

assume ( len f = len g & ( for i being Element of NAT st i in dom f holds
|.(f /. i).| = g . i ) ) ; :: thesis: |.().| = Product g
hence |.().| = Product g by A23; :: thesis: verum