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 Function of NAT ,COMPLEX such that
A3:
f22 . 1 = (F *' ) . 1
and
A4:
for n being Element of 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:2;
A6:
len (F *' ) in Seg (len (F *' ))
by A2, FINSEQ_1:3;
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 Function of NAT ,COMPLEX such that
A10:
for n being Nat st 1 <= n & n <= len (f2 *' ) holds
f9 . n = (f2 *' ) . n
by Th22;
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:3;
1
<= n + 1
by A18, NAT_1:13;
then
n + 1
in Seg (len (F *' ))
by A17, FINSEQ_1:3;
then f2 . (n + 1) =
f22 . (n + 1)
by A9
.=
addcomplex . (f22 . n),
((F *' ) . (n + 1))
by A4, A15, A16, A19
.=
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 Element of NAT st 0 <> n & n < len F holds
(f2 *' ) . (n + 1) = addcomplex . ((f2 *' ) . n),(F . (n + 1))
proof
let n be
Element of
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;
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),((F . (n + 1)) *' )) *'
by A25, A26, COMPLSP2:def 1
.=
addcomplex . ((f2 . n) *' ),
(F . (n + 1))
by Th21
;
hence
(f2 *' ) . (n + 1) = addcomplex . ((f2 *' ) . n),
(F . (n + 1))
by A24, A23, COMPLSP2:def 1;
verum
end;
A27:
for n being Element of NAT st 0 <> n & n < len F holds
f9 . (n + 1) = addcomplex . (f9 . n),(F . (n + 1))
proof
let n be
Element of
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:3;
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:3;
hence
addcomplex $$ (F *' ) = (addcomplex $$ F) *'
; verum