let F be FinSequence of COMPLEX ; ( len (F *') >= 1 implies addcomplex $$ (F *') = (addcomplex $$ F) *' )
A1:
len F = len (F *')
by COMPLSP2:def 1;
assume A2:
len (F *') >= 1
; addcomplex $$ (F *') = (addcomplex $$ F) *'
then consider f22 being sequence of COMPLEX such that
A3:
f22 . 1 = (F *') . 1
and
A4:
for n being Nat st 0 <> n & n < len (F *') holds
f22 . (n + 1) = addcomplex . ((f22 . n),((F *') . (n + 1)))
and
A5:
addcomplex $$ (F *') = f22 . (len (F *'))
by FINSOP_1:1;
A6:
len (F *') in Seg (len (F *'))
by A2, FINSEQ_1:1;
defpred S1[ set , set ] means $2 = f22 . $1;
A7:
for k being Nat st k in Seg (len (F *')) holds
ex x being Element of COMPLEX st S1[k,x]
;
ex f2 being FinSequence of COMPLEX st
( dom f2 = Seg (len (F *')) & ( for k being Nat st k in Seg (len (F *')) holds
S1[k,f2 . k] ) )
from FINSEQ_1:sch 5(A7);
then consider f2 being FinSequence of COMPLEX such that
A8:
dom f2 = Seg (len (F *'))
and
A9:
for k being Nat st k in Seg (len (F *')) holds
S1[k,f2 . k]
;
consider f9 being sequence of COMPLEX such that
A10:
for n being Nat st 1 <= n & n <= len (f2 *') holds
f9 . n = (f2 *') . n
by Th19;
A11:
len (f2 *') = len f2
by COMPLSP2:def 1;
then
1 <= len (f2 *')
by A2, A8, FINSEQ_1:def 3;
then A12:
f9 . 1 = (f2 *') . 1
by A10;
A13:
len f2 = len (F *')
by A8, FINSEQ_1:def 3;
A14:
for n being Nat st 0 <> n & n < len (F *') holds
f2 . (n + 1) = addcomplex . ((f2 . n),((F *') . (n + 1)))
proof
let n be
Nat;
( 0 <> n & n < len (F *') implies f2 . (n + 1) = addcomplex . ((f2 . n),((F *') . (n + 1))) )
assume that A15:
0 <> n
and A16:
n < len (F *')
;
f2 . (n + 1) = addcomplex . ((f2 . n),((F *') . (n + 1)))
A17:
n + 1
<= len (F *')
by A16, NAT_1:13;
A18:
0 + 1
<= n
by A15, NAT_1:13;
then A19:
n in Seg (len (F *'))
by A16, FINSEQ_1:1;
1
<= n + 1
by A18, NAT_1:13;
then
n + 1
in Seg (len (F *'))
by A17, FINSEQ_1:1;
then f2 . (n + 1) =
f22 . (n + 1)
by A9
.=
addcomplex . (
(f22 . n),
((F *') . (n + 1)))
by A4, A15, A16
.=
addcomplex . (
(f2 . n),
((F *') . (n + 1)))
by A9, A19
;
hence
f2 . (n + 1) = addcomplex . (
(f2 . n),
((F *') . (n + 1)))
;
verum
end;
A20:
for n being Nat st 0 <> n & n < len F holds
(f2 *') . (n + 1) = addcomplex . (((f2 *') . n),(F . (n + 1)))
proof
let n be
Nat;
( 0 <> n & n < len F implies (f2 *') . (n + 1) = addcomplex . (((f2 *') . n),(F . (n + 1))) )
assume that A21:
0 <> n
and A22:
n < len F
;
(f2 *') . (n + 1) = addcomplex . (((f2 *') . n),(F . (n + 1)))
A23:
n <= len f2
by A1, A8, A22, FINSEQ_1:def 3;
A24:
0 + 1
<= n
by A21, NAT_1:13;
then A25:
1
<= n + 1
by NAT_1:13;
reconsider c =
(F . (n + 1)) *' as
Element of
COMPLEX by XCMPLX_0:def 2;
A26:
n + 1
<= len F
by A22, NAT_1:13;
then
n + 1
<= len f2
by A1, A8, FINSEQ_1:def 3;
then (f2 *') . (n + 1) =
(f2 . (n + 1)) *'
by A25, COMPLSP2:def 1
.=
(addcomplex . ((f2 . n),((F *') . (n + 1)))) *'
by A1, A14, A21, A22
.=
(addcomplex . ((f2 . n),c)) *'
by A25, A26, COMPLSP2:def 1
.=
((f2 . n) + c) *'
by BINOP_2:def 3
.=
((f2 . n) *') + (c *')
by COMPLEX1:32
.=
addcomplex . (
((f2 . n) *'),
(F . (n + 1)))
by BINOP_2:def 3
;
hence
(f2 *') . (n + 1) = addcomplex . (
((f2 *') . n),
(F . (n + 1)))
by A24, A23, COMPLSP2:def 1;
verum
end;
A27:
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 A28:
0 <> n
and A29:
n < len F
;
f9 . (n + 1) = addcomplex . ((f9 . n),(F . (n + 1)))
A30:
0 + 1
<= n
by A28, NAT_1:13;
n + 1
<= len (f2 *')
by A1, A13, A11, A29, NAT_1:13;
then A31:
f9 . (n + 1) = (f2 *') . (n + 1)
by A10, NAT_1:11;
n <= len (f2 *')
by A1, A13, A29, COMPLSP2:def 1;
then
f9 . n = (f2 *') . n
by A10, A30;
hence
f9 . (n + 1) = addcomplex . (
(f9 . n),
(F . (n + 1)))
by A20, A28, A29, A31;
verum
end;
A32:
1 in Seg (len (F *'))
by A2, FINSEQ_1:1;
set d = (addcomplex $$ (F *')) *' ;
A33:
len F >= 1
by A2, COMPLSP2:def 1;
(f2 *') . (len F) =
(f2 *') . (len (F *'))
by COMPLSP2:def 1
.=
(f2 . (len (F *'))) *'
by A2, A13, COMPLSP2:def 1
.=
(addcomplex $$ (F *')) *'
by A5, A9, A6
;
then A34:
(addcomplex $$ (F *')) *' = f9 . (len F)
by A2, A1, A13, A10, A11;
F . 1 =
((F . 1) *') *'
.=
((F *') . 1) *'
by A33, COMPLSP2:def 1
.=
(f2 . 1) *'
by A3, A9, A32
.=
(f2 *') . 1
by A2, A13, COMPLSP2:def 1
;
then
(addcomplex $$ (F *')) *' = addcomplex $$ F
by A33, A12, A27, A34, FINSOP_1:2;
hence
addcomplex $$ (F *') = (addcomplex $$ F) *'
; verum