let R be FinSequence of REAL ; :: thesis: for F being FinSequence of COMPLEX st R = F & len R >= 1 holds
addreal $$ R = addcomplex $$ F
let F be FinSequence of COMPLEX ; :: thesis: ( R = F & len R >= 1 implies addreal $$ R = addcomplex $$ F )
assume A1:
( R = F & len R >= 1 )
; :: thesis: addreal $$ R = addcomplex $$ F
set d = addreal $$ R;
consider f22 being Function of NAT ,REAL such that
A2:
f22 . 1 = R . 1
and
A3:
for n being Element of NAT st 0 <> n & n < len R holds
f22 . (n + 1) = addreal . (f22 . n),(R . (n + 1))
and
A4:
addreal $$ R = f22 . (len R)
by A1, FINSOP_1:2;
defpred S1[ set , set ] means $2 = f22 . $1;
A5:
for k being Nat st k in Seg (len R) holds
ex x being Element of REAL st S1[k,x]
;
ex f2 being FinSequence of REAL st
( dom f2 = Seg (len R) & ( for k being Nat st k in Seg (len R) holds
S1[k,f2 . k] ) )
from FINSEQ_1:sch 5(A5);
then consider f2 being FinSequence of REAL such that
A6:
( dom f2 = Seg (len R) & ( for k being Nat st k in Seg (len R) holds
S1[k,f2 . k] ) )
;
A7:
len f2 = len R
by A6, FINSEQ_1:def 3;
A8:
1 in Seg (len R)
by A1, FINSEQ_1:3;
A9:
for n being Nat st 0 <> n & n < len R holds
f2 . (n + 1) = addreal . (f2 . n),(R . (n + 1))
proof
let n be
Nat;
:: thesis: ( 0 <> n & n < len R implies f2 . (n + 1) = addreal . (f2 . n),(R . (n + 1)) )
assume A10:
(
0 <> n &
n < len R )
;
:: thesis: f2 . (n + 1) = addreal . (f2 . n),(R . (n + 1))
then
0 < n
;
then A11:
0 + 1
<= n
by NAT_1:13;
then A12:
1
<= n + 1
by NAT_1:13;
A13:
n + 1
<= len R
by A10, NAT_1:13;
A14:
n in Seg (len R)
by A10, A11, FINSEQ_1:3;
n + 1
in Seg (len R)
by A12, A13, FINSEQ_1:3;
then f2 . (n + 1) =
f22 . (n + 1)
by A6
.=
addreal . (f22 . n),
(R . (n + 1))
by A3, A10, A14
.=
addreal . (f2 . n),
(R . (n + 1))
by A6, A14
;
hence
f2 . (n + 1) = addreal . (f2 . n),
(R . (n + 1))
;
:: thesis: verum
end;
A15:
len R in Seg (len R)
by A1, FINSEQ_1:3;
A16:
F . 1 = (FR2FC f2) . 1
by A1, A2, A6, A8;
A17:
(FR2FC f2) . (len F) = addreal $$ R
by A1, A4, A6, A15;
consider f' being Function of NAT ,COMPLEX such that
A18:
for n being Nat st 1 <= n & n <= len (FR2FC f2) holds
f' . n = (FR2FC f2) . n
by Th22;
A19:
f' . 1 = (FR2FC f2) . 1
by A1, A7, A18;
A20:
for n being Element of NAT st 0 <> n & n < len F holds
f' . (n + 1) = addcomplex . (f' . n),(F . (n + 1))
proof
let n be
Element of
NAT ;
:: thesis: ( 0 <> n & n < len F implies f' . (n + 1) = addcomplex . (f' . n),(F . (n + 1)) )
assume A21:
(
0 <> n &
n < len F )
;
:: thesis: f' . (n + 1) = addcomplex . (f' . n),(F . (n + 1))
then
n > 0
;
then A22:
0 + 1
<= n
by NAT_1:13;
A23:
n <= len (FR2FC f2)
by A1, A6, A21, FINSEQ_1:def 3;
n + 1
<= len (FR2FC f2)
by A1, A7, A21, NAT_1:13;
then A24:
f' . (n + 1) = (FR2FC f2) . (n + 1)
by A18, NAT_1:11;
f' . n = (FR2FC f2) . n
by A18, A22, A23;
then
addcomplex . (f' . n),
(F . (n + 1)) = addreal . (f2 . n),
(R . (n + 1))
by A1, COMPLSP2:44;
hence
f' . (n + 1) = addcomplex . (f' . n),
(F . (n + 1))
by A1, A9, A21, A24;
:: thesis: verum
end;
(FR2FC f2) . (len F) = f' . (len F)
by A1, A7, A18;
hence
addreal $$ R = addcomplex $$ F
by A1, A16, A17, A19, A20, FINSOP_1:3; :: thesis: verum