let F be FinSequence of COMPLEX ; :: thesis: ( len (F *' ) >= 1 implies addcomplex $$ (F *' ) = (addcomplex $$ F) *' )
assume A1:
len (F *' ) >= 1
; :: thesis: addcomplex $$ (F *' ) = (addcomplex $$ F) *'
then A2:
len F >= 1
by COMPLSP2:def 1;
A3:
len F = len (F *' )
by COMPLSP2:def 1;
set d = (addcomplex $$ (F *' )) *' ;
consider f22 being Function of NAT ,COMPLEX such that
A4:
f22 . 1 = (F *' ) . 1
and
A5:
for n being Element of NAT st 0 <> n & n < len (F *' ) holds
f22 . (n + 1) = addcomplex . (f22 . n),((F *' ) . (n + 1))
and
A6:
addcomplex $$ (F *' ) = f22 . (len (F *' ))
by A1, FINSOP_1:2;
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 *' )) & ( for k being Nat st k in Seg (len (F *' )) holds
S1[k,f2 . k] ) )
;
A9:
len f2 = len (F *' )
by A8, FINSEQ_1:def 3;
A10:
1 in Seg (len (F *' ))
by A1, FINSEQ_1:3;
A11:
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;
:: thesis: ( 0 <> n & n < len (F *' ) implies f2 . (n + 1) = addcomplex . (f2 . n),((F *' ) . (n + 1)) )
assume A12:
(
0 <> n &
n < len (F *' ) )
;
:: thesis: f2 . (n + 1) = addcomplex . (f2 . n),((F *' ) . (n + 1))
then
0 < n
;
then A13:
0 + 1
<= n
by NAT_1:13;
then A14:
1
<= n + 1
by NAT_1:13;
A15:
n + 1
<= len (F *' )
by A12, NAT_1:13;
A16:
n in Seg (len (F *' ))
by A12, A13, FINSEQ_1:3;
n + 1
in Seg (len (F *' ))
by A14, A15, FINSEQ_1:3;
then f2 . (n + 1) =
f22 . (n + 1)
by A8
.=
addcomplex . (f22 . n),
((F *' ) . (n + 1))
by A5, A12, A16
.=
addcomplex . (f2 . n),
((F *' ) . (n + 1))
by A8, A16
;
hence
f2 . (n + 1) = addcomplex . (f2 . n),
((F *' ) . (n + 1))
;
:: thesis: verum
end;
A17:
len (F *' ) in Seg (len (F *' ))
by A1, FINSEQ_1:3;
A18: F . 1 =
((F . 1) *' ) *'
.=
((F *' ) . 1) *'
by A2, COMPLSP2:def 1
.=
(f2 . 1) *'
by A4, A8, A10
.=
(f2 *' ) . 1
by A1, A9, COMPLSP2:def 1
;
A19:
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 ;
:: thesis: ( 0 <> n & n < len F implies (f2 *' ) . (n + 1) = addcomplex . ((f2 *' ) . n),(F . (n + 1)) )
assume A20:
(
0 <> n &
n < len F )
;
:: thesis: (f2 *' ) . (n + 1) = addcomplex . ((f2 *' ) . n),(F . (n + 1))
then
0 < n
;
then A21:
0 + 1
<= n
by NAT_1:13;
then A22:
1
<= n + 1
by NAT_1:13;
A23:
n + 1
<= len F
by A20, NAT_1:13;
then A24:
n + 1
<= len f2
by A3, A8, FINSEQ_1:def 3;
A25:
n <= len f2
by A3, A8, A20, FINSEQ_1:def 3;
(f2 *' ) . (n + 1) =
(f2 . (n + 1)) *'
by A22, A24, COMPLSP2:def 1
.=
(addcomplex . (f2 . n),((F *' ) . (n + 1))) *'
by A3, A11, A20
.=
(addcomplex . (f2 . n),((F . (n + 1)) *' )) *'
by A22, A23, COMPLSP2:def 1
.=
addcomplex . ((f2 . n) *' ),
(F . (n + 1))
by Th21
;
hence
(f2 *' ) . (n + 1) = addcomplex . ((f2 *' ) . n),
(F . (n + 1))
by A21, A25, COMPLSP2:def 1;
:: thesis: verum
end;
A26: (f2 *' ) . (len F) =
(f2 *' ) . (len (F *' ))
by COMPLSP2:def 1
.=
(f2 . (len (F *' ))) *'
by A1, A9, COMPLSP2:def 1
.=
(addcomplex $$ (F *' )) *'
by A6, A8, A17
;
consider f' being Function of NAT ,COMPLEX such that
A27:
for n being Nat st 1 <= n & n <= len (f2 *' ) holds
f' . n = (f2 *' ) . n
by Th22;
A28:
len (f2 *' ) = len f2
by COMPLSP2:def 1;
then
1 <= len (f2 *' )
by A1, A8, FINSEQ_1:def 3;
then A29:
f' . 1 = (f2 *' ) . 1
by A27;
A30:
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 A31:
(
0 <> n &
n < len F )
;
:: thesis: f' . (n + 1) = addcomplex . (f' . n),(F . (n + 1))
then
n > 0
;
then A32:
0 + 1
<= n
by NAT_1:13;
A33:
n <= len (f2 *' )
by A3, A9, A31, COMPLSP2:def 1;
n + 1
<= len (f2 *' )
by A3, A9, A28, A31, NAT_1:13;
then A34:
f' . (n + 1) = (f2 *' ) . (n + 1)
by A27, NAT_1:11;
f' . n = (f2 *' ) . n
by A27, A32, A33;
hence
f' . (n + 1) = addcomplex . (f' . n),
(F . (n + 1))
by A19, A31, A34;
:: thesis: verum
end;
(addcomplex $$ (F *' )) *' = f' . (len F)
by A1, A3, A9, A26, A27, A28;
then
(addcomplex $$ (F *' )) *' = addcomplex $$ F
by A2, A18, A29, A30, FINSOP_1:3;
hence
addcomplex $$ (F *' ) = (addcomplex $$ F) *'
; :: thesis: verum