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 f).| = 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;
( S1[i] implies S1[i + 1] )
assume A2:
S1[
i]
;
S1[i + 1]
let f be
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 ) & i + 1 = len f holds
|.(Product f).| = Product glet g be
FinSequence of
REAL ;
( 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
;
|.(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 for i being Element of NAT st i in dom f1 holds
|.(f1 /. i).| = g1 . ilet i be
Element of
NAT ;
( 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
;
|.(f1 /. i).| = g1 . ithen 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
;
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
;
verum
end;
A18:
S1[ 0 ]
A23:
for i being Nat holds S1[i]
from NAT_1:sch 2(A18, A1);
let f be 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 ) holds
|.(Product f).| = Product g
let g be FinSequence of REAL ; ( 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 ) )
; |.(Product f).| = Product g
hence
|.(Product f).| = Product g
by A23; verum