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 that
A1: R = F and
A2: len R >= 1 ; :: thesis: 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 S₁[ 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 S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg (len R) implies ex x being Element of REAL st S₁[k,x] )
f22 . k in REAL by XREAL_0:def 1;
hence ( k in Seg (len R) implies ex x being Element of REAL st S₁[k,x] ) ; :: thesis: verum

end;

ex f2 being FinSequence of REAL st
( dom f2 = Seg (len R) & ( for k being Nat st k in Seg (len R) holds
S₁[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
S₁[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; :: thesis: ( 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 ; :: thesis: 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))) ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: 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; :: thesis: verum