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