:: COMPLSP2 semantic presentation

begin


definition
let z be FinSequence of COMPLEX ;
funcz *'  ->  FinSequence of COMPLEX  means :Def1: :: COMPLSP2:def 1
( len it = len z & ( for i being Nat st 1 <= i & i <= len z holds
it . i = (z . i) *' ) );
existence
 ex b1 being FinSequence of COMPLEX st
( len b1 = len z & ( for i being Nat st 1 <= i & i <= len z holds
b1 . i = (z . i) *' ) )
proof
deffunc H1( Nat) ->  Element of COMPLEX = (z . $1) *' ;
consider p being FinSequence such that
A1: ( len p = len z & ( for k being Nat st k in dom p holds
p . k = H1(k) ) ) from FINSEQ_1:sch_2();
 rng p c= COMPLEX
proof
let s2 be set ; :: according to TARSKI:def_3 ::_thesis: ( not s2 in rng p or s2 in COMPLEX )
assume  s2 in rng p ; ::_thesis: s2 in COMPLEX
then consider s1 being set  such that
A2: s1 in dom p and
A3: s2 = p . s1 by FUNCT_1:def_3;
reconsider nx = s1 as Element of NAT by A2;
 p . nx = (z . nx) *' by A1, A2;
hence  s2 in COMPLEX by A3; ::_thesis: verum
end;
then A4: p is FinSequence of COMPLEX by FINSEQ_1:def_4;
 for i being Nat st 1 <= i & i <= len z holds
(z . i) *' = p . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len z implies (z . i) *' = p . i )
assume  ( 1 <= i & i <= len z ) ; ::_thesis: (z . i) *' = p . i
then  i in dom p by A1, FINSEQ_3:25;
hence  (z . i) *' = p . i by A1; ::_thesis: verum
end;
hence  ex b1 being FinSequence of COMPLEX st
( len b1 = len z & ( for i being Nat st 1 <= i & i <= len z holds
b1 . i = (z . i) *' ) ) by A1, A4; ::_thesis: verum
end;
uniqueness
 for b1, b2 being FinSequence of COMPLEX st len b1 = len z & ( for i being Nat st 1 <= i & i <= len z holds
b1 . i = (z . i) *' ) & len b2 = len z & ( for i being Nat st 1 <= i & i <= len z holds
b2 . i = (z . i) *' ) holds
b1 = b2
proof
let p1, p2 be FinSequence of COMPLEX ; ::_thesis: ( len p1 = len z & ( for i being Nat st 1 <= i & i <= len z holds
p1 . i = (z . i) *' ) & len p2 = len z & ( for i being Nat st 1 <= i & i <= len z holds
p2 . i = (z . i) *' ) implies p1 = p2 )
assume that
A5: len p1 = len z and
A6: for i being Nat st 1 <= i & i <= len z holds
(z . i) *' = p1 . i and
A7: len p2 = len z and
A8: for i being Nat st 1 <= i & i <= len z holds
(z . i) *' = p2 . i ; ::_thesis: p1 = p2
 for i being Nat st 1 <= i & i <= len p1 holds
p1 . i = p2 . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len p1 implies p1 . i = p2 . i )
assume A9: ( 1 <= i & i <= len p1 ) ; ::_thesis: p1 . i = p2 . i
then  (z . i) *' = p1 . i by A5, A6;
hence  p1 . i = p2 . i by A5, A8, A9; ::_thesis: verum
end;
hence  p1 = p2 by A5, A7, FINSEQ_1:14; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines *' COMPLSP2:def_1_:_
 for z, b2 being FinSequence of COMPLEX holds
( b2 = z *' iff ( len b2 = len z & ( for i being Nat st 1 <= i & i <= len z holds
b2 . i = (z . i) *' ) ) );

Lm1:  for x being FinSequence of COMPLEX
for c being Element of COMPLEX holds c * x = (multcomplex [;] (c,(id COMPLEX))) * x
proof
let x be FinSequence of COMPLEX ; ::_thesis: for c being Element of COMPLEX holds c * x = (multcomplex [;] (c,(id COMPLEX))) * x
let c be Element of COMPLEX ; ::_thesis: c * x = (multcomplex [;] (c,(id COMPLEX))) * x
 c multcomplex = multcomplex [;] (c,(id COMPLEX)) by SEQ_4:def_4;
hence  c * x = (multcomplex [;] (c,(id COMPLEX))) * x by SEQ_4:def_9; ::_thesis: verum
end;

theorem :: COMPLSP2:1
for i being Element of NAT
for x, y being FinSequence of COMPLEX st i in dom (x + y) holds
(x + y) . i = (x . i) + (y . i) by VALUED_1:def_1;

theorem :: COMPLSP2:2
for i being Element of NAT
for x, y being FinSequence of COMPLEX st i in dom (x - y) holds
(x - y) . i = (x . i) - (y . i) by VALUED_1:13;

definition
let i be Element of NAT ;
let R1, R2 be Element of i -tuples_on COMPLEX;
:: original: -
redefine funcR1 - R2 ->  Element of i -tuples_on COMPLEX;
coherence
 R1 - R2 is Element of i -tuples_on COMPLEX
proof
 R1 - R2 = diffcomplex .: (R1,R2) by SEQ_4:def_7;
hence  R1 - R2 is Element of i -tuples_on COMPLEX by FINSEQ_2:120; ::_thesis: verum
end;
end;

definition
let i be Element of NAT ;
let R1, R2 be Element of i -tuples_on COMPLEX;
:: original: +
redefine funcR1 + R2 ->  Element of i -tuples_on COMPLEX;
coherence
 R1 + R2 is Element of i -tuples_on COMPLEX
proof
 R1 + R2 = addcomplex .: (R1,R2) by SEQ_4:def_6;
hence  R1 + R2 is Element of i -tuples_on COMPLEX by FINSEQ_2:120; ::_thesis: verum
end;
end;

definition
let i be Element of NAT ;
let R be Element of i -tuples_on COMPLEX;
let r be complex number ;
:: original: *
redefine funcr * R ->  Element of i -tuples_on COMPLEX;
coherence
 r * R is Element of i -tuples_on COMPLEX
proof
reconsider q = r as Element of COMPLEX by XCMPLX_0:def_2;
 q * R = (multcomplex [;] (q,(id COMPLEX))) * R by Lm1;
hence  r * R is Element of i -tuples_on COMPLEX by FINSEQ_2:113; ::_thesis: verum
end;
end;

theorem Th3: :: COMPLSP2:3
for a being complex number
for x being FinSequence of COMPLEX holds len (a * x) = len x
proof
let a be complex number ; ::_thesis: for x being FinSequence of COMPLEX holds len (a * x) = len x
let x be FinSequence of COMPLEX ; ::_thesis: len (a * x) = len x
set n = len x;
reconsider z = x as Element of (len x) -tuples_on COMPLEX by FINSEQ_2:92;
reconsider a9 = a as Element of COMPLEX by XCMPLX_0:def_2;
 len (a9 * z) = len x by CARD_1:def_7;
hence  len (a * x) = len x ; ::_thesis: verum
end;

theorem :: COMPLSP2:4
for x being complex-yielding FinSequence holds dom x = dom (- x) by VALUED_1:8;

theorem Th5: :: COMPLSP2:5
for x being complex-valued FinSequence holds len (- x) = len x
proof
let x be complex-valued FinSequence; ::_thesis: len (- x) = len x
 dom (- x) = dom x by VALUED_1:8;
hence  len (- x) = len x by FINSEQ_3:29; ::_thesis: verum
end;

Lm2:  for F being complex-valued FinSequence holds F is FinSequence of COMPLEX
proof
let F be complex-valued FinSequence; ::_thesis: F is FinSequence of COMPLEX
 rng F c= COMPLEX by VALUED_0:def_1;
hence  F is FinSequence of COMPLEX by FINSEQ_1:def_4; ::_thesis: verum
end;

theorem Th6: :: COMPLSP2:6
for x1, x2 being complex-valued FinSequence st len x1 = len x2 holds
len (x1 + x2) = len x1
proof
let x1, x2 be complex-valued FinSequence; ::_thesis: ( len x1 = len x2 implies len (x1 + x2) = len x1 )
set n = len x1;
A1: x2 is FinSequence of COMPLEX by Lm2;
 x1 is FinSequence of COMPLEX by Lm2;
then reconsider z1 = x1 as Element of (len x1) -tuples_on COMPLEX by FINSEQ_2:92;
assume  len x1 = len x2 ; ::_thesis: len (x1 + x2) = len x1
then reconsider z2 = x2 as Element of (len x1) -tuples_on COMPLEX by A1, FINSEQ_2:92;
 dom (z1 + z2) = Seg (len x1) by FINSEQ_2:124;
hence  len (x1 + x2) = len x1 by FINSEQ_1:def_3; ::_thesis: verum
end;

theorem Th7: :: COMPLSP2:7
for x1, x2 being complex-valued FinSequence st len x1 = len x2 holds
len (x1 - x2) = len x1
proof
let x1, x2 be complex-valued FinSequence; ::_thesis: ( len x1 = len x2 implies len (x1 - x2) = len x1 )
set n = len x1;
A1: x2 is FinSequence of COMPLEX by Lm2;
 x1 is FinSequence of COMPLEX by Lm2;
then reconsider z1 = x1 as Element of (len x1) -tuples_on COMPLEX by FINSEQ_2:92;
assume  len x1 = len x2 ; ::_thesis: len (x1 - x2) = len x1
then reconsider z2 = x2 as Element of (len x1) -tuples_on COMPLEX by A1, FINSEQ_2:92;
 dom (z1 - z2) = Seg (len x1) by FINSEQ_2:124;
hence  len (x1 - x2) = len x1 by FINSEQ_1:def_3; ::_thesis: verum
end;

theorem :: COMPLSP2:8
for f being complex-valued FinSequence holds f is Element of COMPLEX (len f)
proof
let f be complex-valued FinSequence; ::_thesis: f is Element of COMPLEX (len f)
 f is FinSequence of COMPLEX by Lm2;
then  f is Element of COMPLEX * by FINSEQ_1:def_11;
then  f in  {  s where s is Element of COMPLEX * : len s = len f  }  ;
then  f in (len f) -tuples_on COMPLEX by FINSEQ_2:def_4;
hence  f is Element of COMPLEX (len f) by SEQ_4:def_11; ::_thesis: verum
end;

theorem :: COMPLSP2:9
for i being Element of NAT
for R1, R2 being Element of i -tuples_on COMPLEX holds R1 - R2 = R1 + (- R2) ;

theorem :: COMPLSP2:10
for x, y being complex-valued FinSequence st len x = len y holds
x - y = x + (- y) ;

theorem :: COMPLSP2:11
for i being Element of NAT
for R being Element of i -tuples_on COMPLEX holds (- 1) * R = - R ;

theorem :: COMPLSP2:12
for x being FinSequence of COMPLEX holds (- 1) * x = - x ;

theorem Th13: :: COMPLSP2:13
for i being Element of NAT
for x being FinSequence of COMPLEX holds (- x) . i = - (x . i)
proof
let i be Element of NAT ; ::_thesis: for x being FinSequence of COMPLEX holds (- x) . i = - (x . i)
let x be FinSequence of COMPLEX ; ::_thesis: (- x) . i = - (x . i)
percases ( not i in dom (- x) or i in dom (- x) ) ;
supposeA1: not i in dom (- x) ; ::_thesis: (- x) . i = - (x . i)
then A2: not i in dom x by VALUED_1:8;
thus (- x) . i = - 0 by A1, FUNCT_1:def_2
.= - (x . i) by A2, FUNCT_1:def_2 ; ::_thesis: verum
end;
supposeA3: i in dom (- x) ; ::_thesis: (- x) . i = - (x . i)
set r = x . i;
 - x = compcomplex * x by SEQ_4:def_8;
then  (- x) . i = compcomplex . (x . i) by A3, FUNCT_1:12;
hence  (- x) . i = - (x . i) by BINOP_2:def_1; ::_thesis: verum
end;
end;
end;

definition
let i be Element of NAT ;
let R be Element of i -tuples_on COMPLEX;
:: original: -
redefine func - R ->  Element of i -tuples_on COMPLEX;
coherence
 - R is Element of i -tuples_on COMPLEX
proof
 - R = compcomplex * R by SEQ_4:def_8;
hence  - R is Element of i -tuples_on COMPLEX by FINSEQ_2:113; ::_thesis: verum
end;
end;

theorem :: COMPLSP2:14
for i, j being Element of NAT
for c being Element of COMPLEX
for R being Element of i -tuples_on COMPLEX st c = R . j holds
(- R) . j = - c by Th13;

theorem Th15: :: COMPLSP2:15
for x being FinSequence of COMPLEX
for a being complex number holds dom (a * x) = dom x
proof
let x be FinSequence of COMPLEX ; ::_thesis: for a being complex number holds dom (a * x) = dom x
let a be complex number ; ::_thesis: dom (a * x) = dom x
 dom (a multcomplex) = COMPLEX by FUNCT_2:def_1;
then  rng x c= dom (a multcomplex) by FINSEQ_1:def_4;
hence  dom x = dom ((a multcomplex) * x) by RELAT_1:27
.= dom (a * x) by SEQ_4:def_9 ;
::_thesis: verum
end;

theorem Th16: :: COMPLSP2:16
for x being FinSequence of COMPLEX
for i being Nat
for a being complex number holds (a * x) . i = a * (x . i)
proof
let x be FinSequence of COMPLEX ; ::_thesis: for i being Nat
for a being complex number holds (a * x) . i = a * (x . i)
let i be Nat; ::_thesis: for a being complex number holds (a * x) . i = a * (x . i)
let a be complex number ; ::_thesis: (a * x) . i = a * (x . i)
reconsider aa = a as Element of COMPLEX by XCMPLX_0:def_2;
percases ( not i in dom (a * x) or i in dom (a * x) ) ;
supposeA1: not i in dom (a * x) ; ::_thesis: (a * x) . i = a * (x . i)
then A2: not i in dom x by Th15;
thus (a * x) . i = a * 0 by A1, FUNCT_1:def_2
.= a * (x . i) by A2, FUNCT_1:def_2 ; ::_thesis: verum
end;
supposeA3: i in dom (a * x) ; ::_thesis: (a * x) . i = a * (x . i)
set a9 = x . i;
A4: a * x = (multcomplex [;] (aa,(id COMPLEX))) * x by Lm1;
then A5: x . i in dom (multcomplex [;] (aa,(id COMPLEX))) by A3, FUNCT_1:11;
thus (a * x) . i = (multcomplex [;] (aa,(id COMPLEX))) . (x . i) by A3, A4, FUNCT_1:12
.= multcomplex . (a,((id COMPLEX) . (x . i))) by A5, FUNCOP_1:32
.= multcomplex . (aa,(x . i)) by FUNCT_1:18
.= a * (x . i) by BINOP_2:def_5 ; ::_thesis: verum
end;
end;
end;

theorem Th17: :: COMPLSP2:17
for x being FinSequence of COMPLEX
for a being complex number holds (a * x) *' = (a *') * (x *')
proof
let x be FinSequence of COMPLEX ; ::_thesis: for a being complex number holds (a * x) *' = (a *') * (x *')
let a be complex number ; ::_thesis: (a * x) *' = (a *') * (x *')
reconsider aa = a as Element of COMPLEX by XCMPLX_0:def_2;
 len ((a *') * (x *')) = len (x *') by Th3;
then A1: len ((a *') * (x *')) = len x by Def1;
A2: len (a * x) = len x by Th3;
A3: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_((a_*_x)_*')_holds_
((a_*_x)_*')_._i_=_((a_*')_*_(x_*'))_._i
let i be Nat; ::_thesis: ( 1 <= i & i <= len ((a * x) *') implies ((a * x) *') . i = ((a *') * (x *')) . i )
assume that
A4: 1 <= i and
A5: i <= len ((a * x) *') ; ::_thesis: ((a * x) *') . i = ((a *') * (x *')) . i
A6: i <= len (a * x) by A5, Def1;
hence ((a * x) *') . i = ((a * x) . i) *' by A4, Def1
.= (aa * (x . i)) *' by Th16
.= (aa *') * ((x . i) *') by COMPLEX1:35
.= (a *') * ((x *') . i) by A2, A4, A6, Def1
.= ((a *') * (x *')) . i by Th16 ;
::_thesis: verum
end;
 len ((a * x) *') = len (a * x) by Def1;
hence  (a * x) *' = (a *') * (x *') by A1, A3, Th3, FINSEQ_1:14; ::_thesis: verum
end;

theorem Th18: :: COMPLSP2:18
for i, j being Element of NAT
for R1, R2 being Element of i -tuples_on COMPLEX holds (R1 + R2) . j = (R1 . j) + (R2 . j)
proof
let i, j be Element of NAT ; ::_thesis: for R1, R2 being Element of i -tuples_on COMPLEX holds (R1 + R2) . j = (R1 . j) + (R2 . j)
let R1, R2 be Element of i -tuples_on COMPLEX; ::_thesis: (R1 + R2) . j = (R1 . j) + (R2 . j)
percases ( not j in Seg i or j in Seg i ) ;
supposeA1: not j in Seg i ; ::_thesis: (R1 + R2) . j = (R1 . j) + (R2 . j)
then A2: not j in dom R2 by FINSEQ_2:124;
A3: not j in dom R1 by A1, FINSEQ_2:124;
 not j in dom (R1 + R2) by A1, FINSEQ_2:124;
hence (R1 + R2) . j = 0 + 0 by FUNCT_1:def_2
.= (R1 . j) + 0 by A3, FUNCT_1:def_2
.= (R1 . j) + (R2 . j) by A2, FUNCT_1:def_2 ;
::_thesis: verum
end;
suppose j in Seg i ; ::_thesis: (R1 + R2) . j = (R1 . j) + (R2 . j)
then  j in dom (R1 + R2) by FINSEQ_2:124;
hence  (R1 + R2) . j = (R1 . j) + (R2 . j) by VALUED_1:def_1; ::_thesis: verum
end;
end;
end;

theorem Th19: :: COMPLSP2:19
for x1, x2 being FinSequence of COMPLEX st len x1 = len x2 holds
(x1 + x2) *' = (x1 *') + (x2 *')
proof
let x1, x2 be FinSequence of COMPLEX ; ::_thesis: ( len x1 = len x2 implies (x1 + x2) *' = (x1 *') + (x2 *') )
reconsider x9 = x1 as Element of (len x1) -tuples_on COMPLEX by FINSEQ_2:92;
reconsider y9 = x2 as Element of (len x2) -tuples_on COMPLEX by FINSEQ_2:92;
reconsider x3 = x1 *' as Element of (len (x1 *')) -tuples_on COMPLEX by FINSEQ_2:92;
reconsider x4 = x2 *' as Element of (len (x2 *')) -tuples_on COMPLEX by FINSEQ_2:92;
assume A1: len x1 = len x2 ; ::_thesis: (x1 + x2) *' = (x1 *') + (x2 *')
then A2: len (x1 + x2) = len x1 by Th6;
A3: ( len x1 = len (x1 *') & len x2 = len (x2 *') ) by Def1;
A4: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_((x1_+_x2)_*')_holds_
((x1_+_x2)_*')_._i_=_(x3_+_x4)_._i
let i be Nat; ::_thesis: ( 1 <= i & i <= len ((x1 + x2) *') implies ((x1 + x2) *') . i = (x3 + x4) . i )
A5: i in NAT by ORDINAL1:def_12;
assume that
A6: 1 <= i and
A7: i <= len ((x1 + x2) *') ; ::_thesis: ((x1 + x2) *') . i = (x3 + x4) . i
A8: i <= len (x1 + x2) by A7, Def1;
hence ((x1 + x2) *') . i = ((x1 + x2) . i) *' by A6, Def1
.= ((x9 . i) + (y9 . i)) *' by A1, A5, Th18
.= ((x1 . i) *') + ((x2 . i) *') by COMPLEX1:32
.= ((x1 *') . i) + ((x2 . i) *') by A2, A6, A8, Def1
.= ((x1 *') . i) + ((x2 *') . i) by A1, A2, A6, A8, Def1
.= (x3 + x4) . i by A1, A3, A5, Th18 ;
::_thesis: verum
end;
 len ((x1 *') + (x2 *')) = len x1 by A1, A3, Th6;
then  len ((x1 + x2) *') = len ((x1 *') + (x2 *')) by A2, Def1;
hence  (x1 + x2) *' = (x1 *') + (x2 *') by A4, FINSEQ_1:14; ::_thesis: verum
end;

theorem Th20: :: COMPLSP2:20
for i, j being Element of NAT
for R1, R2 being Element of i -tuples_on COMPLEX holds (R1 - R2) . j = (R1 . j) - (R2 . j)
proof
let i, j be Element of NAT ; ::_thesis: for R1, R2 being Element of i -tuples_on COMPLEX holds (R1 - R2) . j = (R1 . j) - (R2 . j)
let R1, R2 be Element of i -tuples_on COMPLEX; ::_thesis: (R1 - R2) . j = (R1 . j) - (R2 . j)
percases ( not j in Seg i or j in Seg i ) ;
supposeA1: not j in Seg i ; ::_thesis: (R1 - R2) . j = (R1 . j) - (R2 . j)
then A2: not j in dom R2 by FINSEQ_2:124;
A3: not j in dom R1 by A1, FINSEQ_2:124;
 not j in dom (R1 - R2) by A1, FINSEQ_2:124;
hence (R1 - R2) . j = 0 - 0 by FUNCT_1:def_2
.= (R1 . j) - 0 by A3, FUNCT_1:def_2
.= (R1 . j) - (R2 . j) by A2, FUNCT_1:def_2 ;
::_thesis: verum
end;
suppose j in Seg i ; ::_thesis: (R1 - R2) . j = (R1 . j) - (R2 . j)
then  j in dom (R1 - R2) by FINSEQ_2:124;
hence  (R1 - R2) . j = (R1 . j) - (R2 . j) by VALUED_1:13; ::_thesis: verum
end;
end;
end;

theorem Th21: :: COMPLSP2:21
for x1, x2 being FinSequence of COMPLEX st len x1 = len x2 holds
(x1 - x2) *' = (x1 *') - (x2 *')
proof
let x1, x2 be FinSequence of COMPLEX ; ::_thesis: ( len x1 = len x2 implies (x1 - x2) *' = (x1 *') - (x2 *') )
reconsider x9 = x1 as Element of (len x1) -tuples_on COMPLEX by FINSEQ_2:92;
reconsider y9 = x2 as Element of (len x2) -tuples_on COMPLEX by FINSEQ_2:92;
reconsider x3 = x1 *' as Element of (len (x1 *')) -tuples_on COMPLEX by FINSEQ_2:92;
reconsider x4 = x2 *' as Element of (len (x2 *')) -tuples_on COMPLEX by FINSEQ_2:92;
assume A1: len x1 = len x2 ; ::_thesis: (x1 - x2) *' = (x1 *') - (x2 *')
then A2: len (x1 - x2) = len x1 by Th7;
A3: ( len x1 = len (x1 *') & len x2 = len (x2 *') ) by Def1;
A4: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_((x1_-_x2)_*')_holds_
((x1_-_x2)_*')_._i_=_(x3_-_x4)_._i
let i be Nat; ::_thesis: ( 1 <= i & i <= len ((x1 - x2) *') implies ((x1 - x2) *') . i = (x3 - x4) . i )
A5: i in NAT by ORDINAL1:def_12;
assume that
A6: 1 <= i and
A7: i <= len ((x1 - x2) *') ; ::_thesis: ((x1 - x2) *') . i = (x3 - x4) . i
A8: i <= len (x1 - x2) by A7, Def1;
hence ((x1 - x2) *') . i = ((x1 - x2) . i) *' by A6, Def1
.= ((x9 . i) - (y9 . i)) *' by A1, A5, Th20
.= ((x1 . i) *') - ((x2 . i) *') by COMPLEX1:34
.= ((x1 *') . i) - ((x2 . i) *') by A2, A6, A8, Def1
.= ((x1 *') . i) - ((x2 *') . i) by A1, A2, A6, A8, Def1
.= (x3 - x4) . i by A1, A3, A5, Th20 ;
::_thesis: verum
end;
 len ((x1 *') - (x2 *')) = len x1 by A1, A3, Th7;
then  len ((x1 - x2) *') = len ((x1 *') - (x2 *')) by A2, Def1;
hence  (x1 - x2) *' = (x1 *') - (x2 *') by A4, FINSEQ_1:14; ::_thesis: verum
end;

theorem :: COMPLSP2:22
for z being FinSequence of COMPLEX holds (z *') *' = z
proof
let z be FinSequence of COMPLEX ; ::_thesis: (z *') *' = z
A1: len (z *') = len z by Def1;
A2: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_((z_*')_*')_holds_
((z_*')_*')_._i_=_z_._i
let i be Nat; ::_thesis: ( 1 <= i & i <= len ((z *') *') implies ((z *') *') . i = z . i )
assume that
A3: 1 <= i and
A4: i <= len ((z *') *') ; ::_thesis: ((z *') *') . i = z . i
A5: i <= len (z *') by A4, Def1;
then  (z *') . i = (z . i) *' by A1, A3, Def1;
hence ((z *') *') . i = ((z . i) *') *' by A3, A5, Def1
.= z . i ;
::_thesis: verum
end;
 len ((z *') *') = len (z *') by Def1;
hence  (z *') *' = z by A1, A2, FINSEQ_1:14; ::_thesis: verum
end;

theorem :: COMPLSP2:23
for z being FinSequence of COMPLEX holds (- z) *' = - (z *')
proof
let z be FinSequence of COMPLEX ; ::_thesis: (- z) *' = - (z *')
(- z) *' = ((- 1r) *') * (z *') by Th17, COMPLEX1:def_4
.= - (z *') by COMPLEX1:30, COMPLEX1:33, COMPLEX1:def_4 ;
hence  (- z) *' = - (z *') ; ::_thesis: verum
end;

theorem Th24: :: COMPLSP2:24
for z being complex number holds z + (z *') = 2 * (Re z)
proof
let z be complex number ; ::_thesis: z + (z *') = 2 * (Re z)
 z is Element of COMPLEX by XCMPLX_0:def_2;
then z + (z *') = ((Re z) + (Re (z *'))) + (((Im z) + (Im (z *'))) * <i>) by COMPLEX1:def_5
.= ((Re z) + (Re (z *'))) + (((Im z) + (- (Im z))) * <i>) by COMPLEX1:27
.= (Re z) + (Re z) by COMPLEX1:27
.= 2 * (Re z) ;
hence  z + (z *') = 2 * (Re z) ; ::_thesis: verum
end;

theorem Th25: :: COMPLSP2:25
for i being Element of NAT
for x, y being complex-valued FinSequence st len x = len y holds
(x - y) . i = (x . i) - (y . i)
proof
let i be Element of NAT ; ::_thesis: for x, y being complex-valued FinSequence st len x = len y holds
(x - y) . i = (x . i) - (y . i)
let x, y be complex-valued FinSequence; ::_thesis: ( len x = len y implies (x - y) . i = (x . i) - (y . i) )
A1: ( x is FinSequence of COMPLEX & y is FinSequence of COMPLEX ) by Lm2;
then reconsider x2 = x as Element of (len x) -tuples_on COMPLEX by FINSEQ_2:92;
reconsider y2 = y as Element of (len y) -tuples_on COMPLEX by A1, FINSEQ_2:92;
reconsider y29 = x2 - y2 as Element of (len (x2 - y2)) -tuples_on COMPLEX by FINSEQ_2:92;
assume A2: len x = len y ; ::_thesis: (x - y) . i = (x . i) - (y . i)
then A3: len (x - y) = len x by Th7;
percases ( not i in Seg (len x) or i in Seg (len x) ) ;
supposeA4: not i in Seg (len x) ; ::_thesis: (x - y) . i = (x . i) - (y . i)
then A5: not i in dom x2 by FINSEQ_2:124;
A6: not i in dom y2 by A2, A4, FINSEQ_2:124;
 not i in dom y29 by A3, A4, FINSEQ_2:124;
then (x2 - y2) . i = 0 - 0 by FUNCT_1:def_2
.= (x2 . i) - 0 by A5, FUNCT_1:def_2
.= (x2 . i) - (y2 . i) by A6, FUNCT_1:def_2 ;
hence  (x - y) . i = (x . i) - (y . i) ; ::_thesis: verum
end;
suppose i in Seg (len x) ; ::_thesis: (x - y) . i = (x . i) - (y . i)
then  i in dom y29 by A3, FINSEQ_2:124;
hence  (x - y) . i = (x . i) - (y . i) by VALUED_1:13; ::_thesis: verum
end;
end;
end;

theorem Th26: :: COMPLSP2:26
for i being Element of NAT
for x, y being complex-valued FinSequence st len x = len y holds
(x + y) . i = (x . i) + (y . i)
proof
let i be Element of NAT ; ::_thesis: for x, y being complex-valued FinSequence st len x = len y holds
(x + y) . i = (x . i) + (y . i)
let x, y be complex-valued FinSequence; ::_thesis: ( len x = len y implies (x + y) . i = (x . i) + (y . i) )
A1: ( x is FinSequence of COMPLEX & y is FinSequence of COMPLEX ) by Lm2;
then reconsider x2 = x as Element of (len x) -tuples_on COMPLEX by FINSEQ_2:92;
reconsider y2 = y as Element of (len y) -tuples_on COMPLEX by A1, FINSEQ_2:92;
reconsider y29 = x2 + y2 as Element of (len (x2 + y2)) -tuples_on COMPLEX by FINSEQ_2:92;
assume A2: len x = len y ; ::_thesis: (x + y) . i = (x . i) + (y . i)
then A3: len (x + y) = len x by Th6;
percases ( not i in Seg (len x) or i in Seg (len x) ) ;
supposeA4: not i in Seg (len x) ; ::_thesis: (x + y) . i = (x . i) + (y . i)
then A5: not i in dom x2 by FINSEQ_2:124;
A6: not i in dom y2 by A2, A4, FINSEQ_2:124;
 not i in dom y29 by A3, A4, FINSEQ_2:124;
then (x2 + y2) . i = 0 + 0 by FUNCT_1:def_2
.= (x2 . i) + 0 by A5, FUNCT_1:def_2
.= (x2 . i) + (y2 . i) by A6, FUNCT_1:def_2 ;
hence  (x + y) . i = (x . i) + (y . i) ; ::_thesis: verum
end;
suppose i in Seg (len x) ; ::_thesis: (x + y) . i = (x . i) + (y . i)
then  i in dom y29 by A3, FINSEQ_2:124;
hence  (x + y) . i = (x . i) + (y . i) by VALUED_1:def_1; ::_thesis: verum
end;
end;
end;

definition
let z be FinSequence of COMPLEX ;
func Re z ->  FinSequence of REAL  equals :: COMPLSP2:def 2
(1 / 2) * (z + (z *'));
coherence
 (1 / 2) * (z + (z *')) is FinSequence of REAL
proof
A1: len z = len (z *') by Def1;
A2: len ((1 / 2) * (z + (z *'))) = len (z + (z *')) by Th3
.= len z by A1, Th6 ;
 rng ((1 / 2) * (z + (z *'))) c= REAL
proof
let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in rng ((1 / 2) * (z + (z *'))) or w in REAL )
assume  w in rng ((1 / 2) * (z + (z *'))) ; ::_thesis: w in REAL
then consider x being set  such that
A3: x in dom ((1 / 2) * (z + (z *'))) and
A4: w = ((1 / 2) * (z + (z *'))) . x by FUNCT_1:def_3;
reconsider i = x as Element of NAT by A3;
 x in Seg (len ((1 / 2) * (z + (z *')))) by A3, FINSEQ_1:def_3;
then A5: ( 1 <= i & i <= len z ) by A2, FINSEQ_1:1;
((1 / 2) * (z + (z *'))) . i = (1 / 2) * ((z + (z *')) . i) by Th16
.= (1 / 2) * ((z . i) + ((z *') . i)) by A1, Th26
.= (1 / 2) * ((z . i) + ((z . i) *')) by A5, Def1
.= (1 / 2) * (2 * (Re (z . i))) by Th24 ;
hence  w in REAL by A4; ::_thesis: verum
end;
hence  (1 / 2) * (z + (z *')) is FinSequence of REAL by FINSEQ_1:def_4; ::_thesis: verum
end;
end;

:: deftheorem  defines Re COMPLSP2:def_2_:_
 for z being FinSequence of COMPLEX holds Re z = (1 / 2) * (z + (z *'));

theorem Th27: :: COMPLSP2:27
for z being complex number holds z - (z *') = (2 * (Im z)) * <i>
proof
let z be complex number ; ::_thesis: z - (z *') = (2 * (Im z)) * <i>
 z is Element of COMPLEX by XCMPLX_0:def_2;
then z - (z *') = ((Re z) - (Re (z *'))) + (((Im z) - (Im (z *'))) * <i>) by COMPLEX1:def_8
.= ((Re z) - (Re (z *'))) + (((Im z) - (- (Im z))) * <i>) by COMPLEX1:27
.= ((Re z) - (Re z)) + (((Im z) - (- (Im z))) * <i>) by COMPLEX1:27
.= (2 * (Im z)) * <i> ;
hence  z - (z *') = (2 * (Im z)) * <i> ; ::_thesis: verum
end;

definition
let z be FinSequence of COMPLEX ;
func Im z ->  FinSequence of REAL  equals :: COMPLSP2:def 3
(- ((1 / 2) * <i>)) * (z - (z *'));
coherence
 (- ((1 / 2) * <i>)) * (z - (z *')) is FinSequence of REAL
proof
A1: len z = len (z *') by Def1;
A2: len ((- ((1 / 2) * <i>)) * (z - (z *'))) = len (z - (z *')) by Th3
.= len z by A1, Th7 ;
 rng ((- ((1 / 2) * <i>)) * (z - (z *'))) c= REAL
proof
let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in rng ((- ((1 / 2) * <i>)) * (z - (z *'))) or w in REAL )
assume  w in rng ((- ((1 / 2) * <i>)) * (z - (z *'))) ; ::_thesis: w in REAL
then consider x being set  such that
A3: x in dom ((- ((1 / 2) * <i>)) * (z - (z *'))) and
A4: w = ((- ((1 / 2) * <i>)) * (z - (z *'))) . x by FUNCT_1:def_3;
reconsider i = x as Element of NAT by A3;
 x in Seg (len ((- ((1 / 2) * <i>)) * (z - (z *')))) by A3, FINSEQ_1:def_3;
then A5: ( 1 <= i & i <= len z ) by A2, FINSEQ_1:1;
((- ((1 / 2) * <i>)) * (z - (z *'))) . i = (- ((1 / 2) * <i>)) * ((z - (z *')) . i) by Th16
.= (- ((1 / 2) * <i>)) * ((z . i) - ((z *') . i)) by A1, Th25
.= (- ((1 / 2) * <i>)) * ((z . i) - ((z . i) *')) by A5, Def1
.= (- ((1 / 2) * <i>)) * ((2 * (Im (z . i))) * <i>) by Th27 ;
hence  w in REAL by A4; ::_thesis: verum
end;
hence  (- ((1 / 2) * <i>)) * (z - (z *')) is FinSequence of REAL by FINSEQ_1:def_4; ::_thesis: verum
end;
end;

:: deftheorem  defines Im COMPLSP2:def_3_:_
 for z being FinSequence of COMPLEX holds Im z = (- ((1 / 2) * <i>)) * (z - (z *'));

definition
let x, y be FinSequence of COMPLEX ;
func|(x,y)| ->  Element of COMPLEX  equals :: COMPLSP2:def 4
((|((Re x),(Re y))| - (<i> * |((Re x),(Im y))|)) + (<i> * |((Im x),(Re y))|)) + |((Im x),(Im y))|;
coherence
 ((|((Re x),(Re y))| - (<i> * |((Re x),(Im y))|)) + (<i> * |((Im x),(Re y))|)) + |((Im x),(Im y))| is Element of COMPLEX ;
end;

:: deftheorem  defines |( COMPLSP2:def_4_:_
 for x, y being FinSequence of COMPLEX holds |(x,y)| = ((|((Re x),(Re y))| - (<i> * |((Re x),(Im y))|)) + (<i> * |((Im x),(Re y))|)) + |((Im x),(Im y))|;

theorem Th28: :: COMPLSP2:28
for x, y, z being complex-valued FinSequence st len x = len y & len y = len z holds
x + (y + z) = (x + y) + z
proof
let x, y, z be complex-valued FinSequence; ::_thesis: ( len x = len y & len y = len z implies x + (y + z) = (x + y) + z )
reconsider x1 = x, y1 = y, z1 = z as FinSequence of COMPLEX by Lm2;
assume A1: ( len x = len y & len y = len z ) ; ::_thesis: x + (y + z) = (x + y) + z
reconsider z9 = z1 as Element of (len z) -tuples_on COMPLEX by FINSEQ_2:92;
reconsider y9 = y1 as Element of (len y) -tuples_on COMPLEX by FINSEQ_2:92;
reconsider x9 = x1 as Element of (len x) -tuples_on COMPLEX by FINSEQ_2:92;
x + (y + z) = addcomplex .: (x1,(y1 + z1)) by SEQ_4:def_6
.= addcomplex .: (x1,(addcomplex .: (y1,z1))) by SEQ_4:def_6
.= addcomplex .: ((addcomplex .: (x9,y9)),z9) by A1, FINSEQOP:28
.= addcomplex .: ((x1 + y1),z1) by SEQ_4:def_6
.= (x + y) + z by SEQ_4:def_6 ;
hence  x + (y + z) = (x + y) + z ; ::_thesis: verum
end;

theorem :: COMPLSP2:29
for x, y being complex-valued FinSequence st len x = len y holds
x + y = y + x ;

theorem Th30: :: COMPLSP2:30
for c being complex number
for x, y being FinSequence of COMPLEX st len x = len y holds
c * (x + y) = (c * x) + (c * y)
proof
let c be complex number ; ::_thesis: for x, y being FinSequence of COMPLEX st len x = len y holds
c * (x + y) = (c * x) + (c * y)
let x, y be FinSequence of COMPLEX ; ::_thesis: ( len x = len y implies c * (x + y) = (c * x) + (c * y) )
assume A1: len x = len y ; ::_thesis: c * (x + y) = (c * x) + (c * y)
set cM = c multcomplex ;
reconsider y9 = y as Element of (len y) -tuples_on COMPLEX by FINSEQ_2:92;
reconsider x9 = x as Element of (len x) -tuples_on COMPLEX by FINSEQ_2:92;
A2: c is Element of COMPLEX by XCMPLX_0:def_2;
c * (x + y) = (c multcomplex) * (x + y) by SEQ_4:def_9
.= (c multcomplex) * (addcomplex .: (x,y)) by SEQ_4:def_6
.= addcomplex .: (((c multcomplex) * x9),((c multcomplex) * y9)) by A1, A2, FINSEQOP:51, SEQ_4:56
.= ((c multcomplex) * x) + ((c multcomplex) * y) by SEQ_4:def_6
.= (c * x) + ((c multcomplex) * y) by SEQ_4:def_9
.= (c * x) + (c * y) by SEQ_4:def_9 ;
hence  c * (x + y) = (c * x) + (c * y) ; ::_thesis: verum
end;

theorem :: COMPLSP2:31
for x, y being complex-valued FinSequence st len x = len y holds
x - y = x + (- y) ;

theorem Th32: :: COMPLSP2:32
for x, y being complex-valued FinSequence st len x = len y & x + y = 0c (len x) holds
( x = - y & y = - x )
proof
let x, y be complex-valued FinSequence; ::_thesis: ( len x = len y & x + y = 0c (len x) implies ( x = - y & y = - x ) )
assume that
A1: len x = len y and
A2: x + y = 0c (len x) ; ::_thesis: ( x = - y & y = - x )
reconsider x1 = x, y1 = y as FinSequence of COMPLEX by Lm2;
reconsider x9 = x1 as Element of (len x) -tuples_on COMPLEX by FINSEQ_2:92;
reconsider y9 = y1 as Element of (len y) -tuples_on COMPLEX by FINSEQ_2:92;
A3: ( x + y = addcomplex .: (x1,y1) & - y = compcomplex * y1 ) by SEQ_4:def_6, SEQ_4:def_8;
 x + y = (len x) |-> 0c by A2, SEQ_4:def_12;
then  x9 = - y9 by A1, A3, BINOP_2:1, FINSEQOP:74, SEQ_4:51, SEQ_4:52;
hence  ( x = - y & y = - x ) ; ::_thesis: verum
end;

theorem Th33: :: COMPLSP2:33
for x being complex-valued FinSequence holds x + (0c (len x)) = x
proof
let x be complex-valued FinSequence; ::_thesis: x + (0c (len x)) = x
A1: x is FinSequence of COMPLEX by Lm2;
then reconsider x9 = x as Element of (len x) -tuples_on COMPLEX by FINSEQ_2:92;
x + (0c (len x)) = x + ((len x) |-> 0c) by SEQ_4:def_12
.= addcomplex .: (x,((len x) |-> 0c)) by A1, SEQ_4:def_6
.= x9 by BINOP_2:1, FINSEQOP:56 ;
hence  x + (0c (len x)) = x ; ::_thesis: verum
end;

theorem Th34: :: COMPLSP2:34
for x being complex-valued FinSequence holds x + (- x) = 0c (len x)
proof
let x be complex-valued FinSequence; ::_thesis: x + (- x) = 0c (len x)
A1: ( x is FinSequence of COMPLEX & - x is FinSequence of COMPLEX ) by Lm2;
then reconsider x9 = x as Element of (len x) -tuples_on COMPLEX by FINSEQ_2:92;
x + (- x) = addcomplex .: (x,(- x)) by A1, SEQ_4:def_6
.= addcomplex .: (x,(compcomplex * x)) by A1, SEQ_4:def_8
.= (len x9) |-> 0c by BINOP_2:1, FINSEQOP:73, SEQ_4:51, SEQ_4:52
.= 0c (len x9) by SEQ_4:def_12 ;
hence  x + (- x) = 0c (len x) ; ::_thesis: verum
end;

theorem Th35: :: COMPLSP2:35
for x, y being complex-valued FinSequence st len x = len y holds
- (x + y) = (- x) + (- y)
proof
let x, y be complex-valued FinSequence; ::_thesis: ( len x = len y implies - (x + y) = (- x) + (- y) )
assume A1: len x = len y ; ::_thesis: - (x + y) = (- x) + (- y)
A2: len (- y) = len y by Th5;
then A3: len ((- x) + (- y)) = len (- x) by A1, Th5, Th6;
A4: len (- x) = len x by Th5;
A5: len (x + y) = len x by A1, Th6;
then (x + y) + ((- x) + (- y)) = ((y + x) + (- x)) + (- y) by A1, A2, A4, Th28
.= (y + (x + (- x))) + (- y) by A1, A4, Th28
.= (y + (0c (len x))) + (- y) by Th34
.= y + (- y) by A1, Th33
.= 0c (len y) by Th34 ;
hence  - (x + y) = (- x) + (- y) by A1, A4, A5, A3, Th32; ::_thesis: verum
end;

theorem Th36: :: COMPLSP2:36
for x, y, z being complex-valued FinSequence st len x = len y & len y = len z holds
(x - y) - z = x - (y + z)
proof
let x, y, z be complex-valued FinSequence; ::_thesis: ( len x = len y & len y = len z implies (x - y) - z = x - (y + z) )
assume that
A1: len x = len y and
A2: len y = len z ; ::_thesis: (x - y) - z = x - (y + z)
 ( len (- y) = len y & len (- z) = len z ) by Th5;
then (x - y) - z = x + ((- y) + (- z)) by A1, A2, Th28
.= x - (y + z) by A2, Th35 ;
hence  (x - y) - z = x - (y + z) ; ::_thesis: verum
end;

theorem Th37: :: COMPLSP2:37
for x, y, z being complex-valued FinSequence st len x = len y & len y = len z holds
x + (y - z) = (x + y) - z
proof
let x, y, z be complex-valued FinSequence; ::_thesis: ( len x = len y & len y = len z implies x + (y - z) = (x + y) - z )
assume A1: ( len x = len y & len y = len z ) ; ::_thesis: x + (y - z) = (x + y) - z
 len (- z) = len z by Th5;
hence  x + (y - z) = (x + y) - z by A1, Th28; ::_thesis: verum
end;

theorem :: COMPLSP2:38
canceled;

theorem Th39: :: COMPLSP2:39
for x, y being complex-valued FinSequence st len x = len y holds
- (x - y) = (- x) + y
proof
let x, y be complex-valued FinSequence; ::_thesis: ( len x = len y implies - (x - y) = (- x) + y )
assume A1: len x = len y ; ::_thesis: - (x - y) = (- x) + y
 len (- y) = len y by Th5;
then  - (x - y) = (- x) + (- (- y)) by A1, Th35
.= (- x) + y ;
hence  - (x - y) = (- x) + y ; ::_thesis: verum
end;

theorem Th40: :: COMPLSP2:40
for x, y, z being complex-valued FinSequence st len x = len y & len y = len z holds
x - (y - z) = (x - y) + z
proof
let x, y, z be complex-valued FinSequence; ::_thesis: ( len x = len y & len y = len z implies x - (y - z) = (x - y) + z )
assume that
A1: len x = len y and
A2: len y = len z ; ::_thesis: x - (y - z) = (x - y) + z
A3: len (- y) = len y by Th5;
x - (y - z) = x + ((- y) + z) by A2, Th39
.= (x - y) + z by A1, A2, A3, Th28 ;
hence  x - (y - z) = (x - y) + z ; ::_thesis: verum
end;

theorem Th41: :: COMPLSP2:41
for x being FinSequence of COMPLEX
for c being complex number holds c * (0c (len x)) = 0c (len x)
proof
let x be FinSequence of COMPLEX ; ::_thesis: for c being complex number holds c * (0c (len x)) = 0c (len x)
let c be complex number ; ::_thesis: c * (0c (len x)) = 0c (len x)
reconsider cc = c as Element of COMPLEX by XCMPLX_0:def_2;
A1: rng (0c (len x)) c= COMPLEX by FINSEQ_1:def_4;
c * (0c (len x)) = (multcomplex [;] (cc,(id COMPLEX))) * (0c (len x)) by Lm1
.= multcomplex [;] (cc,((id COMPLEX) * (0c (len x)))) by FUNCOP_1:34
.= multcomplex [;] (cc,(0c (len x))) by A1, RELAT_1:53
.= multcomplex [;] (cc,((len x) |-> 0c)) by SEQ_4:def_12
.= (len x) |-> (multcomplex . (cc,0c)) by FINSEQOP:18
.= (len x) |-> (cc * 0c) by BINOP_2:def_5
.= 0c (len x) by SEQ_4:def_12 ;
hence  c * (0c (len x)) = 0c (len x) ; ::_thesis: verum
end;

theorem Th42: :: COMPLSP2:42
for x being FinSequence of COMPLEX
for c being complex number holds - (c * x) = c * (- x)
proof
let x be FinSequence of COMPLEX ; ::_thesis: for c being complex number holds - (c * x) = c * (- x)
let c be complex number ; ::_thesis: - (c * x) = c * (- x)
A1: ( len (c * (- x)) = len (- x) & len (c * x) = len x ) by Th3;
A2: len x = len (- x) by Th5;
then (c * (- x)) + (c * x) = c * (x + (- x)) by Th30
.= c * (0c (len x)) by Th34
.= 0c (len x) by Th41 ;
hence  - (c * x) = c * (- x) by A2, A1, Th32; ::_thesis: verum
end;

theorem Th43: :: COMPLSP2:43
for c being complex number
for x, y being FinSequence of COMPLEX st len x = len y holds
c * (x - y) = (c * x) - (c * y)
proof
let c be complex number ; ::_thesis: for x, y being FinSequence of COMPLEX st len x = len y holds
c * (x - y) = (c * x) - (c * y)
let x, y be FinSequence of COMPLEX ; ::_thesis: ( len x = len y implies c * (x - y) = (c * x) - (c * y) )
assume A1: len x = len y ; ::_thesis: c * (x - y) = (c * x) - (c * y)
reconsider cc = c as Element of COMPLEX by XCMPLX_0:def_2;
reconsider y9 = y as Element of (len y) -tuples_on COMPLEX by FINSEQ_2:92;
reconsider x9 = x as Element of (len x) -tuples_on COMPLEX by FINSEQ_2:92;
set cM = cc multcomplex ;
c * (x - y) = (cc multcomplex) * (x + (- y)) by SEQ_4:def_9
.= (cc multcomplex) * (addcomplex .: (x,(- y))) by SEQ_4:def_6
.= addcomplex .: (((cc multcomplex) * x9),((cc multcomplex) * (- y9))) by A1, FINSEQOP:51, SEQ_4:56
.= ((cc multcomplex) * x) + ((cc multcomplex) * (- y)) by SEQ_4:def_6
.= (c * x) + ((cc multcomplex) * (- y)) by SEQ_4:def_9
.= (c * x) + (c * (- y)) by SEQ_4:def_9
.= (c * x) - (c * y) by Th42 ;
hence  c * (x - y) = (c * x) - (c * y) ; ::_thesis: verum
end;

theorem :: COMPLSP2:44
for x1, y1 being Element of COMPLEX
for x2, y2 being Real st x1 = x2 & y1 = y2 holds
addcomplex . (x1,y1) = addreal . (x2,y2)
proof
let x1, y1 be Element of COMPLEX ; ::_thesis: for x2, y2 being Real st x1 = x2 & y1 = y2 holds
addcomplex . (x1,y1) = addreal . (x2,y2)
let x2, y2 be Real; ::_thesis: ( x1 = x2 & y1 = y2 implies addcomplex . (x1,y1) = addreal . (x2,y2) )
A1: addcomplex . (x1,y1) = x1 + y1 by BINOP_2:def_3;
assume  ( x1 = x2 & y1 = y2 ) ; ::_thesis: addcomplex . (x1,y1) = addreal . (x2,y2)
hence  addcomplex . (x1,y1) = addreal . (x2,y2) by A1, BINOP_2:def_9; ::_thesis: verum
end;


theorem Th45: :: COMPLSP2:45
for C being Function of [:COMPLEX,COMPLEX:],COMPLEX
for G being Function of [:REAL,REAL:],REAL
for x1, y1 being FinSequence of COMPLEX
for x2, y2 being FinSequence of REAL st x1 = x2 & y1 = y2 & len x1 = len y2 & ( for i being Element of NAT st i in dom x1 holds
C . ((x1 . i),(y1 . i)) = G . ((x2 . i),(y2 . i)) ) holds
C .: (x1,y1) = G .: (x2,y2)
proof
let C be Function of [:COMPLEX,COMPLEX:],COMPLEX; ::_thesis: for G being Function of [:REAL,REAL:],REAL
for x1, y1 being FinSequence of COMPLEX
for x2, y2 being FinSequence of REAL st x1 = x2 & y1 = y2 & len x1 = len y2 & ( for i being Element of NAT st i in dom x1 holds
C . ((x1 . i),(y1 . i)) = G . ((x2 . i),(y2 . i)) ) holds
C .: (x1,y1) = G .: (x2,y2)
let G be Function of [:REAL,REAL:],REAL; ::_thesis: for x1, y1 being FinSequence of COMPLEX
for x2, y2 being FinSequence of REAL st x1 = x2 & y1 = y2 & len x1 = len y2 & ( for i being Element of NAT st i in dom x1 holds
C . ((x1 . i),(y1 . i)) = G . ((x2 . i),(y2 . i)) ) holds
C .: (x1,y1) = G .: (x2,y2)
let x1, y1 be FinSequence of COMPLEX ; ::_thesis: for x2, y2 being FinSequence of REAL st x1 = x2 & y1 = y2 & len x1 = len y2 & ( for i being Element of NAT st i in dom x1 holds
C . ((x1 . i),(y1 . i)) = G . ((x2 . i),(y2 . i)) ) holds
C .: (x1,y1) = G .: (x2,y2)
let x2, y2 be FinSequence of REAL ; ::_thesis: ( x1 = x2 & y1 = y2 & len x1 = len y2 & ( for i being Element of NAT st i in dom x1 holds
C . ((x1 . i),(y1 . i)) = G . ((x2 . i),(y2 . i)) ) implies C .: (x1,y1) = G .: (x2,y2) )
assume that
A1: x1 = x2 and
A2: y1 = y2 and
A3: len x1 = len y2 and
A4: for i being Element of NAT st i in dom x1 holds
C . ((x1 . i),(y1 . i)) = G . ((x2 . i),(y2 . i)) ; ::_thesis: C .: (x1,y1) = G .: (x2,y2)
A5: len (G .: (x2,y2)) = len x1 by A1, A3, FINSEQ_2:72;
A6: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_(C_.:_(x1,y1))_holds_
(C_.:_(x1,y1))_._i_=_(G_.:_(x2,y2))_._i
let i be Nat; ::_thesis: ( 1 <= i & i <= len (C .: (x1,y1)) implies (C .: (x1,y1)) . i = (G .: (x2,y2)) . i )
assume that
A7: 1 <= i and
A8: i <= len (C .: (x1,y1)) ; ::_thesis: (C .: (x1,y1)) . i = (G .: (x2,y2)) . i
A9: i <= len x1 by A2, A3, A8, FINSEQ_2:72;
then A10: i in dom x1 by A7, FINSEQ_3:25;
A11: i in dom (G .: (x2,y2)) by A5, A7, A9, FINSEQ_3:25;
 i in dom (C .: (x1,y1)) by A7, A8, FINSEQ_3:25;
hence (C .: (x1,y1)) . i = C . ((x1 . i),(y1 . i)) by FUNCOP_1:22
.= G . ((x2 . i),(y2 . i)) by A4, A10
.= (G .: (x2,y2)) . i by A11, FUNCOP_1:22 ;
::_thesis: verum
end;
 len (C .: (x1,y1)) = len x1 by A2, A3, FINSEQ_2:72;
hence  C .: (x1,y1) = G .: (x2,y2) by A5, A6, FINSEQ_1:14; ::_thesis: verum
end;

theorem :: COMPLSP2:46
for x1, y1 being FinSequence of COMPLEX
for x2, y2 being FinSequence of REAL st x1 = x2 & y1 = y2 & len x1 = len y2 holds
addcomplex .: (x1,y1) = addreal .: (x2,y2)
proof
let x1, y1 be FinSequence of COMPLEX ; ::_thesis: for x2, y2 being FinSequence of REAL st x1 = x2 & y1 = y2 & len x1 = len y2 holds
addcomplex .: (x1,y1) = addreal .: (x2,y2)
let x2, y2 be FinSequence of REAL ; ::_thesis: ( x1 = x2 & y1 = y2 & len x1 = len y2 implies addcomplex .: (x1,y1) = addreal .: (x2,y2) )
assume that
A1: ( x1 = x2 & y1 = y2 ) and
A2: len x1 = len y2 ; ::_thesis: addcomplex .: (x1,y1) = addreal .: (x2,y2)
 for i being Element of NAT st i in dom x1 holds
addcomplex . ((x1 . i),(y1 . i)) = addreal . ((x2 . i),(y2 . i))
proof
let i be Element of NAT ; ::_thesis: ( i in dom x1 implies addcomplex . ((x1 . i),(y1 . i)) = addreal . ((x2 . i),(y2 . i)) )
 (x1 . i) + (y1 . i) = addcomplex . ((x1 . i),(y1 . i)) by BINOP_2:def_3;
hence  ( i in dom x1 implies addcomplex . ((x1 . i),(y1 . i)) = addreal . ((x2 . i),(y2 . i)) ) by A1, BINOP_2:def_9; ::_thesis: verum
end;
hence  addcomplex .: (x1,y1) = addreal .: (x2,y2) by A1, A2, Th45; ::_thesis: verum
end;

theorem :: COMPLSP2:47
for x1, y1 being FinSequence of COMPLEX
for x2, y2 being FinSequence of REAL st x1 = x2 & y1 = y2 & len x1 = len y2 holds
x1 + y1 = x2 + y2 ;

theorem Th48: :: COMPLSP2:48
for x being FinSequence of COMPLEX holds
( len (Re x) = len x & len (Im x) = len x )
proof
let x be FinSequence of COMPLEX ; ::_thesis: ( len (Re x) = len x & len (Im x) = len x )
A1: len x = len (x *') by Def1;
A2: len (Im x) = len (x - (x *')) by Th3
.= len x by A1, Th7 ;
len (Re x) = len (x + (x *')) by Th3
.= len x by A1, Th6 ;
hence  ( len (Re x) = len x & len (Im x) = len x ) by A2; ::_thesis: verum
end;

theorem Th49: :: COMPLSP2:49
for x, y being FinSequence of COMPLEX st len x = len y holds
( Re (x + y) = (Re x) + (Re y) & Im (x + y) = (Im x) + (Im y) )
proof
let x, y be FinSequence of COMPLEX ; ::_thesis: ( len x = len y implies ( Re (x + y) = (Re x) + (Re y) & Im (x + y) = (Im x) + (Im y) ) )
A1: len (- (x *')) = len (x *') by Th5;
assume A2: len x = len y ; ::_thesis: ( Re (x + y) = (Re x) + (Re y) & Im (x + y) = (Im x) + (Im y) )
then A3: len (x + y) = len x by Th6;
A4: len y = len (y *') by Def1;
then A5: len (y + (y *')) = len y by Th6;
A6: len x = len (x *') by Def1;
then A7: len (x + (x *')) = len x by Th6;
A8: len (x - (x *')) = len x by A6, Th7;
A9: len (y - (y *')) = len y by A4, Th7;
thus  Re (x + y) = (1 / 2) * ((x + y) + ((x *') + (y *'))) by A2, Th19
.= (1 / 2) * (((x + y) + (x *')) + (y *')) by A2, A4, A6, A3, Th28
.= (1 / 2) * (((x + (x *')) + y) + (y *')) by A2, A6, Th28
.= (1 / 2) * ((x + (x *')) + (y + (y *'))) by A2, A4, A7, Th28
.= (Re x) + (Re y) by A2, A7, A5, Th30 ; ::_thesis: Im (x + y) = (Im x) + (Im y)
thus  Im (x + y) = (- ((1 / 2) * <i>)) * ((x + y) - ((x *') + (y *'))) by A2, Th19
.= (- ((1 / 2) * <i>)) * (((x + y) - (x *')) - (y *')) by A2, A4, A6, A3, Th36
.= (- ((1 / 2) * <i>)) * (((x + (- (x *'))) + y) - (y *')) by A2, A6, A1, Th28
.= (- ((1 / 2) * <i>)) * ((x - (x *')) + (y - (y *'))) by A2, A4, A8, Th37
.= (Im x) + (Im y) by A2, A8, A9, Th30 ; ::_thesis: verum
end;

theorem :: COMPLSP2:50
for x1, y1 being FinSequence of COMPLEX
for x2, y2 being FinSequence of REAL st x1 = x2 & y1 = y2 & len x1 = len y2 holds
diffcomplex .: (x1,y1) = diffreal .: (x2,y2)
proof
let x1, y1 be FinSequence of COMPLEX ; ::_thesis: for x2, y2 being FinSequence of REAL st x1 = x2 & y1 = y2 & len x1 = len y2 holds
diffcomplex .: (x1,y1) = diffreal .: (x2,y2)
let x2, y2 be FinSequence of REAL ; ::_thesis: ( x1 = x2 & y1 = y2 & len x1 = len y2 implies diffcomplex .: (x1,y1) = diffreal .: (x2,y2) )
assume that
A1: ( x1 = x2 & y1 = y2 ) and
A2: len x1 = len y2 ; ::_thesis: diffcomplex .: (x1,y1) = diffreal .: (x2,y2)
 for i being Element of NAT st i in dom x1 holds
diffcomplex . ((x1 . i),(y1 . i)) = diffreal . ((x2 . i),(y2 . i))
proof
let i be Element of NAT ; ::_thesis: ( i in dom x1 implies diffcomplex . ((x1 . i),(y1 . i)) = diffreal . ((x2 . i),(y2 . i)) )
 (x1 . i) - (y1 . i) = diffcomplex . ((x1 . i),(y1 . i)) by BINOP_2:def_4;
hence  ( i in dom x1 implies diffcomplex . ((x1 . i),(y1 . i)) = diffreal . ((x2 . i),(y2 . i)) ) by A1, BINOP_2:def_10; ::_thesis: verum
end;
hence  diffcomplex .: (x1,y1) = diffreal .: (x2,y2) by A1, A2, Th45; ::_thesis: verum
end;

theorem :: COMPLSP2:51
for x1, y1 being FinSequence of COMPLEX
for x2, y2 being FinSequence of REAL st x1 = x2 & y1 = y2 & len x1 = len y2 holds
x1 - y1 = x2 - y2 ;

theorem Th52: :: COMPLSP2:52
for x, y being FinSequence of COMPLEX st len x = len y holds
( Re (x - y) = (Re x) - (Re y) & Im (x - y) = (Im x) - (Im y) )
proof
let x, y be FinSequence of COMPLEX ; ::_thesis: ( len x = len y implies ( Re (x - y) = (Re x) - (Re y) & Im (x - y) = (Im x) - (Im y) ) )
assume A1: len x = len y ; ::_thesis: ( Re (x - y) = (Re x) - (Re y) & Im (x - y) = (Im x) - (Im y) )
then A2: len (x - y) = len x by Th7;
A3: len x = len (x *') by Def1;
then A4: len (x + (x *')) = len x by Th6;
A5: len y = len (y *') by Def1;
then A6: len (y + (y *')) = len y by Th6;
thus  Re (x - y) = (1 / 2) * ((x - y) + ((x *') - (y *'))) by A1, Th21
.= (1 / 2) * (((x *') + (x - y)) - (y *')) by A1, A5, A3, A2, Th37
.= (1 / 2) * ((x *') + ((x - y) - (y *'))) by A1, A5, A3, A2, Th37
.= (1 / 2) * ((x *') + (x - (y + (y *')))) by A1, A5, Th36
.= (1 / 2) * ((x + (x *')) - (y + (y *'))) by A1, A3, A6, Th37
.= (Re x) - (Re y) by A1, A4, A6, Th43 ; ::_thesis: Im (x - y) = (Im x) - (Im y)
A7: len (x - (x *')) = len x by A3, Th7;
A8: len (y - (y *')) = len y by A5, Th7;
thus  Im (x - y) = (- ((1 / 2) * <i>)) * ((x - y) - ((x *') - (y *'))) by A1, Th21
.= (- ((1 / 2) * <i>)) * (((x - y) - (x *')) + (y *')) by A1, A5, A3, A2, Th40
.= (- ((1 / 2) * <i>)) * ((x - ((x *') + y)) + (y *')) by A1, A3, Th36
.= (- ((1 / 2) * <i>)) * (((x - (x *')) - y) + (y *')) by A1, A3, Th36
.= (- ((1 / 2) * <i>)) * ((x - (x *')) - (y - (y *'))) by A1, A5, A7, Th40
.= (Im x) - (Im y) by A1, A7, A8, Th43 ; ::_thesis: verum
end;

theorem Th53: :: COMPLSP2:53
for z being FinSequence of COMPLEX
for a, b being complex number holds a * (b * z) = (a * b) * z
proof
let z be FinSequence of COMPLEX ; ::_thesis: for a, b being complex number holds a * (b * z) = (a * b) * z
let a, b be complex number ; ::_thesis: a * (b * z) = (a * b) * z
reconsider aa = a, bb = b as Element of COMPLEX by XCMPLX_0:def_2;
thus (a * b) * z = (multcomplex [;] ((aa * bb),(id COMPLEX))) * z by Lm1
.= (multcomplex [;] ((multcomplex . (aa,bb)),(id COMPLEX))) * z by BINOP_2:def_5
.= (multcomplex [;] (aa,(multcomplex [;] (bb,(id COMPLEX))))) * z by FUNCOP_1:62
.= ((multcomplex [;] (aa,(id COMPLEX))) * (multcomplex [;] (bb,(id COMPLEX)))) * z by FUNCOP_1:55
.= (multcomplex [;] (aa,(id COMPLEX))) * ((multcomplex [;] (bb,(id COMPLEX))) * z) by RELAT_1:36
.= (multcomplex [;] (aa,(id COMPLEX))) * (b * z) by Lm1
.= a * (b * z) by Lm1 ; ::_thesis: verum
end;

Lm3:  for x being FinSequence of COMPLEX holds - (0c (len x)) = 0c (len x)
proof
let x be FinSequence of COMPLEX ; ::_thesis: - (0c (len x)) = 0c (len x)
- (0c (len x)) = - ((len x) |-> 0c) by SEQ_4:def_12
.= compcomplex * ((len x) |-> 0c) by SEQ_4:def_8
.= (len x) |-> (compcomplex . 0c) by FINSEQOP:16
.= (len x) |-> (- 0c) by BINOP_2:def_1
.= 0c (len x) by SEQ_4:def_12 ;
hence  - (0c (len x)) = 0c (len x) ; ::_thesis: verum
end;

theorem Th54: :: COMPLSP2:54
for x being FinSequence of COMPLEX
for c being complex number holds (- c) * x = - (c * x)
proof
let x be FinSequence of COMPLEX ; ::_thesis: for c being complex number holds (- c) * x = - (c * x)
let c be complex number ; ::_thesis: (- c) * x = - (c * x)
A1: len ((- c) * x) = len x by Th3;
A2: len (c * x) = len x by Th3;
((- c) * x) + (c * x) = (((- 1) * c) * x) + (c * x)
.= (- (c * x)) + (c * x) by Th53
.= - ((c * x) - (c * x)) by A2, Th39
.= - (0c (len x)) by A2, Th34
.= 0c (len x) by Lm3 ;
hence  (- c) * x = - (c * x) by A1, A2, Th32; ::_thesis: verum
end;


theorem Th55: :: COMPLSP2:55
for h being Function of COMPLEX,COMPLEX
for g being Function of REAL,REAL
for y1 being FinSequence of COMPLEX
for y2 being FinSequence of REAL st len y1 = len y2 & ( for i being Element of NAT st i in dom y1 holds
h . (y1 . i) = g . (y2 . i) ) holds
h * y1 = g * y2
proof
let h be Function of COMPLEX,COMPLEX; ::_thesis: for g being Function of REAL,REAL
for y1 being FinSequence of COMPLEX
for y2 being FinSequence of REAL st len y1 = len y2 & ( for i being Element of NAT st i in dom y1 holds
h . (y1 . i) = g . (y2 . i) ) holds
h * y1 = g * y2
let g be Function of REAL,REAL; ::_thesis: for y1 being FinSequence of COMPLEX
for y2 being FinSequence of REAL st len y1 = len y2 & ( for i being Element of NAT st i in dom y1 holds
h . (y1 . i) = g . (y2 . i) ) holds
h * y1 = g * y2
let y1 be FinSequence of COMPLEX ; ::_thesis: for y2 being FinSequence of REAL st len y1 = len y2 & ( for i being Element of NAT st i in dom y1 holds
h . (y1 . i) = g . (y2 . i) ) holds
h * y1 = g * y2
let y2 be FinSequence of REAL ; ::_thesis: ( len y1 = len y2 & ( for i being Element of NAT st i in dom y1 holds
h . (y1 . i) = g . (y2 . i) ) implies h * y1 = g * y2 )
assume that
A1: len y1 = len y2 and
A2: for i being Element of NAT st i in dom y1 holds
h . (y1 . i) = g . (y2 . i) ; ::_thesis: h * y1 = g * y2
A3: len (g * y2) = len y1 by A1, FINSEQ_2:33;
A4: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_(h_*_y1)_holds_
(h_*_y1)_._i_=_(g_*_y2)_._i
let i be Nat; ::_thesis: ( 1 <= i & i <= len (h * y1) implies (h * y1) . i = (g * y2) . i )
assume that
A5: 1 <= i and
A6: i <= len (h * y1) ; ::_thesis: (h * y1) . i = (g * y2) . i
A7: i <= len y1 by A6, FINSEQ_2:33;
then A8: i in dom y1 by A5, FINSEQ_3:25;
A9: i in dom (g * y2) by A3, A5, A7, FINSEQ_3:25;
 i in dom (h * y1) by A5, A6, FINSEQ_3:25;
hence (h * y1) . i = h . (y1 . i) by FUNCT_1:12
.= g . (y2 . i) by A2, A8
.= (g * y2) . i by A9, FUNCT_1:12 ;
::_thesis: verum
end;
 len (h * y1) = len y1 by FINSEQ_2:33;
hence  h * y1 = g * y2 by A3, A4, FINSEQ_1:14; ::_thesis: verum
end;

theorem :: COMPLSP2:56
for y1 being FinSequence of COMPLEX
for y2 being FinSequence of REAL st y1 = y2 & len y1 = len y2 holds
compcomplex * y1 = compreal * y2
proof
let y1 be FinSequence of COMPLEX ; ::_thesis: for y2 being FinSequence of REAL st y1 = y2 & len y1 = len y2 holds
compcomplex * y1 = compreal * y2
let y2 be FinSequence of REAL ; ::_thesis: ( y1 = y2 & len y1 = len y2 implies compcomplex * y1 = compreal * y2 )
assume that
A1: y1 = y2 and
A2: len y1 = len y2 ; ::_thesis: compcomplex * y1 = compreal * y2
 for i being Element of NAT st i in dom y1 holds
compcomplex . (y1 . i) = compreal . (y2 . i)
proof
let i be Element of NAT ; ::_thesis: ( i in dom y1 implies compcomplex . (y1 . i) = compreal . (y2 . i) )
assume  i in dom y1 ; ::_thesis: compcomplex . (y1 . i) = compreal . (y2 . i)
 - (y1 . i) = compcomplex . (y1 . i) by BINOP_2:def_1;
hence  compcomplex . (y1 . i) = compreal . (y2 . i) by A1, BINOP_2:def_7; ::_thesis: verum
end;
hence  compcomplex * y1 = compreal * y2 by A2, Th55; ::_thesis: verum
end;

theorem :: COMPLSP2:57
for y1 being FinSequence of COMPLEX
for y2 being FinSequence of REAL st y1 = y2 & len y1 = len y2 holds
- y1 = - y2 ;

theorem Th58: :: COMPLSP2:58
for x being FinSequence of COMPLEX holds
( Re (<i> * x) = - (Im x) & Im (<i> * x) = Re x )
proof
let x be FinSequence of COMPLEX ; ::_thesis: ( Re (<i> * x) = - (Im x) & Im (<i> * x) = Re x )
A1: len (x *') = len x by Def1;
A2: Im (<i> * x) = ((- (1 / 2)) * <i>) * ((<i> * x) - ((- <i>) * (x *'))) by Th17, COMPLEX1:31
.= ((- (1 / 2)) * <i>) * ((<i> * x) + (- (- (<i> * (x *'))))) by Th54
.= ((- (1 / 2)) * <i>) * (<i> * (x + (x *'))) by A1, Th30
.= (((- (1 / 2)) * <i>) * <i>) * (x + (x *')) by Th53
.= Re x ;
Re (<i> * x) = (1 / 2) * ((<i> * x) + ((- <i>) * (x *'))) by Th17, COMPLEX1:31
.= (1 / 2) * ((<i> * x) - (<i> * (x *'))) by Th54
.= (1 / 2) * (<i> * (x - (x *'))) by A1, Th43
.= ((1 / 2) * <i>) * (x - (x *')) by Th53
.= ((- 1) * ((- (1 / 2)) * <i>)) * (x - (x *'))
.= - (Im x) by Th53 ;
hence  ( Re (<i> * x) = - (Im x) & Im (<i> * x) = Re x ) by A2; ::_thesis: verum
end;

theorem Th59: :: COMPLSP2:59
for x, y being FinSequence of COMPLEX st len x = len y holds
|((<i> * x),y)| = <i> * |(x,y)|
proof
let x, y be FinSequence of COMPLEX ; ::_thesis: ( len x = len y implies |((<i> * x),y)| = <i> * |(x,y)| )
assume A1: len x = len y ; ::_thesis: |((<i> * x),y)| = <i> * |(x,y)|
A2: len (Im y) = len y by Th48;
A3: len (Re y) = len y by Th48;
A4: len (Im x) = len x by Th48;
|((<i> * x),y)| = ((|((- (Im x)),(Re y))| - (<i> * |((Re (<i> * x)),(Im y))|)) + (<i> * |((Im (<i> * x)),(Re y))|)) + |((Im (<i> * x)),(Im y))| by Th58
.= ((|((- (Im x)),(Re y))| - (<i> * |((- (Im x)),(Im y))|)) + (<i> * |((Im (<i> * x)),(Re y))|)) + |((Im (<i> * x)),(Im y))| by Th58
.= ((|((- (Im x)),(Re y))| - (<i> * |((- (Im x)),(Im y))|)) + (<i> * |((Re x),(Re y))|)) + |((Im (<i> * x)),(Im y))| by Th58
.= ((|((- (Im x)),(Re y))| - (<i> * |((- (Im x)),(Im y))|)) + (<i> * |((Re x),(Re y))|)) + |((Re x),(Im y))| by Th58
.= (((- |((Im x),(Re y))|) - (<i> * |((- (Im x)),(Im y))|)) + (<i> * |((Re x),(Re y))|)) + |((Re x),(Im y))| by A1, A3, A4, RVSUM_1:122
.= (((- |((Im x),(Re y))|) - (<i> * (- |((Im x),(Im y))|))) + (<i> * |((Re x),(Re y))|)) + |((Re x),(Im y))| by A1, A4, A2, RVSUM_1:122
.= <i> * |(x,y)| ;
hence  |((<i> * x),y)| = <i> * |(x,y)| ; ::_thesis: verum
end;

theorem Th60: :: COMPLSP2:60
for x, y being FinSequence of COMPLEX st len x = len y holds
|(x,(<i> * y))| = - (<i> * |(x,y)|)
proof
let x, y be FinSequence of COMPLEX ; ::_thesis: ( len x = len y implies |(x,(<i> * y))| = - (<i> * |(x,y)|) )
assume A1: len x = len y ; ::_thesis: |(x,(<i> * y))| = - (<i> * |(x,y)|)
A2: len (Im x) = len x by Th48;
A3: len (Re x) = len x by Th48;
A4: len (Im y) = len y by Th48;
|(x,(<i> * y))| = ((|((Re x),(- (Im y)))| - (<i> * |((Re x),(Im (<i> * y)))|)) + (<i> * |((Im x),(Re (<i> * y)))|)) + |((Im x),(Im (<i> * y)))| by Th58
.= ((|((Re x),(- (Im y)))| - (<i> * |((Re x),(Re y))|)) + (<i> * |((Im x),(Re (<i> * y)))|)) + |((Im x),(Im (<i> * y)))| by Th58
.= ((|((Re x),(- (Im y)))| - (<i> * |((Re x),(Re y))|)) + (<i> * |((Im x),(- (Im y)))|)) + |((Im x),(Im (<i> * y)))| by Th58
.= ((|((Re x),(- (Im y)))| - (<i> * |((Re x),(Re y))|)) + (<i> * |((Im x),(- (Im y)))|)) + |((Im x),(Re y))| by Th58
.= (((- |((Re x),(Im y))|) - (<i> * |((Re x),(Re y))|)) + (<i> * |((Im x),(- (Im y)))|)) + |((Im x),(Re y))| by A1, A3, A4, RVSUM_1:122
.= (((- |((Re x),(Im y))|) - (<i> * |((Re x),(Re y))|)) + (<i> * (- |((Im x),(Im y))|))) + |((Im x),(Re y))| by A1, A2, A4, RVSUM_1:122
.= - (<i> * |(x,y)|) ;
hence  |(x,(<i> * y))| = - (<i> * |(x,y)|) ; ::_thesis: verum
end;

theorem :: COMPLSP2:61
for a1 being Element of COMPLEX
for y1 being FinSequence of COMPLEX
for a2 being Element of REAL
for y2 being FinSequence of REAL st a1 = a2 & y1 = y2 & len y1 = len y2 holds
(a1 multcomplex) * y1 = (a2 multreal) * y2
proof
let a1 be Element of COMPLEX ; ::_thesis: for y1 being FinSequence of COMPLEX
for a2 being Element of REAL
for y2 being FinSequence of REAL st a1 = a2 & y1 = y2 & len y1 = len y2 holds
(a1 multcomplex) * y1 = (a2 multreal) * y2
let y1 be FinSequence of COMPLEX ; ::_thesis: for a2 being Element of REAL
for y2 being FinSequence of REAL st a1 = a2 & y1 = y2 & len y1 = len y2 holds
(a1 multcomplex) * y1 = (a2 multreal) * y2
let a2 be Element of REAL ; ::_thesis: for y2 being FinSequence of REAL st a1 = a2 & y1 = y2 & len y1 = len y2 holds
(a1 multcomplex) * y1 = (a2 multreal) * y2
let y2 be FinSequence of REAL ; ::_thesis: ( a1 = a2 & y1 = y2 & len y1 = len y2 implies (a1 multcomplex) * y1 = (a2 multreal) * y2 )
assume that
A1: ( a1 = a2 & y1 = y2 ) and
A2: len y1 = len y2 ; ::_thesis: (a1 multcomplex) * y1 = (a2 multreal) * y2
 for i being Element of NAT st i in dom y1 holds
(a1 multcomplex) . (y1 . i) = (a2 multreal) . (y2 . i)
proof
let i be Element of NAT ; ::_thesis: ( i in dom y1 implies (a1 multcomplex) . (y1 . i) = (a2 multreal) . (y2 . i) )
assume  i in dom y1 ; ::_thesis: (a1 multcomplex) . (y1 . i) = (a2 multreal) . (y2 . i)
A3: (a2 * y2) . i = a2 * (y2 . i) by RVSUM_1:44
.= multreal . (a2,(y2 . i)) by BINOP_2:def_11
.= multreal . (a2,((id REAL) . (y2 . i))) by FUNCT_1:18
.= (multreal [;] (a2,(id REAL))) . (y2 . i) by FUNCOP_1:53
.= (a2 multreal) . (y2 . i) by RVSUM_1:def_3 ;
(a1 * y1) . i = a1 * (y1 . i) by Th16
.= multcomplex . (a1,(y1 . i)) by BINOP_2:def_5
.= multcomplex . (a1,((id COMPLEX) . (y1 . i))) by FUNCT_1:18
.= (multcomplex [;] (a1,(id COMPLEX))) . (y1 . i) by FUNCOP_1:53
.= (a1 multcomplex) . (y1 . i) by SEQ_4:def_4 ;
hence  (a1 multcomplex) . (y1 . i) = (a2 multreal) . (y2 . i) by A1, A3; ::_thesis: verum
end;
hence  (a1 multcomplex) * y1 = (a2 multreal) * y2 by A2, Th55; ::_thesis: verum
end;

theorem :: COMPLSP2:62
for a1 being complex number
for y1 being FinSequence of COMPLEX
for a2 being Element of REAL
for y2 being FinSequence of REAL st a1 = a2 & y1 = y2 & len y1 = len y2 holds
a1 * y1 = a2 * y2 ;

theorem Th63: :: COMPLSP2:63
for z being FinSequence of COMPLEX
for a, b being complex number holds (a + b) * z = (a * z) + (b * z)
proof
let z be FinSequence of COMPLEX ; ::_thesis: for a, b being complex number holds (a + b) * z = (a * z) + (b * z)
let a, b be complex number ; ::_thesis: (a + b) * z = (a * z) + (b * z)
reconsider aa = a, bb = b as Element of COMPLEX by XCMPLX_0:def_2;
set c1M = multcomplex [;] (aa,(id COMPLEX));
set c2M = multcomplex [;] (bb,(id COMPLEX));
thus (a + b) * z = (multcomplex [;] ((aa + bb),(id COMPLEX))) * z by Lm1
.= (multcomplex [;] ((addcomplex . (aa,bb)),(id COMPLEX))) * z by BINOP_2:def_3
.= (addcomplex .: ((multcomplex [;] (aa,(id COMPLEX))),(multcomplex [;] (bb,(id COMPLEX))))) * z by FINSEQOP:35, SEQ_4:54
.= addcomplex .: (((multcomplex [;] (aa,(id COMPLEX))) * z),((multcomplex [;] (bb,(id COMPLEX))) * z)) by FUNCOP_1:25
.= ((multcomplex [;] (aa,(id COMPLEX))) * z) + ((multcomplex [;] (bb,(id COMPLEX))) * z) by SEQ_4:def_6
.= (a * z) + ((multcomplex [;] (bb,(id COMPLEX))) * z) by Lm1
.= (a * z) + (b * z) by Lm1 ; ::_thesis: verum
end;

theorem Th64: :: COMPLSP2:64
for z being FinSequence of COMPLEX
for a, b being complex number holds (a - b) * z = (a * z) - (b * z)
proof
let z be FinSequence of COMPLEX ; ::_thesis: for a, b being complex number holds (a - b) * z = (a * z) - (b * z)
let a, b be complex number ; ::_thesis: (a - b) * z = (a * z) - (b * z)
reconsider aa = a, bb = b as Element of COMPLEX by XCMPLX_0:def_2;
(a - b) * z = (a + (- b)) * z
.= (aa * z) + ((- bb) * z) by Th63
.= (a * z) - (b * z) by Th54 ;
hence  (a - b) * z = (a * z) - (b * z) ; ::_thesis: verum
end;

theorem Th65: :: COMPLSP2:65
for a being Element of COMPLEX
for x being FinSequence of COMPLEX holds
( Re (a * x) = ((Re a) * (Re x)) - ((Im a) * (Im x)) & Im (a * x) = ((Im a) * (Re x)) + ((Re a) * (Im x)) )
proof
let a be Element of COMPLEX ; ::_thesis: for x being FinSequence of COMPLEX holds
( Re (a * x) = ((Re a) * (Re x)) - ((Im a) * (Im x)) & Im (a * x) = ((Im a) * (Re x)) + ((Re a) * (Im x)) )
let x be FinSequence of COMPLEX ; ::_thesis: ( Re (a * x) = ((Re a) * (Re x)) - ((Im a) * (Im x)) & Im (a * x) = ((Im a) * (Re x)) + ((Re a) * (Im x)) )
reconsider z5 = Re a, z6 = Im a as Element of COMPLEX by XCMPLX_0:def_2;
A1: len (x *') = len x by Def1;
 len (((1 / 2) * z5) * x) = len x by Th3;
then A2: len (((((1 / 2) * <i>) * z6) * x) + (((1 / 2) * z5) * x)) = len ((((1 / 2) * <i>) * z6) * x) by Th3, Th6;
A3: len (((1 / 2) * z5) * x) = len x by Th3;
A4: ( len (z5 * x) = len x & len ((<i> * z6) * x) = len x ) by Th3;
A5: (Re a) * (Re x) = (z5 * (1 / 2)) * (x + (x *')) by Th53
.= (((z5 * 1) / 2) * x) + (((z5 * 1) / 2) * (x *')) by A1, Th30 ;
A6: ( len (Re x) = len x & len ((Re a) * (Re x)) = len (Re x) ) by Th48, RVSUM_1:117;
A7: ( len ((z5 - (z6 * <i>)) * (x *')) = len (x *') & len ((z5 + (<i> * z6)) * x) = len x ) by Th3;
A8: len (((- ((1 / 2) * <i>)) * z6) * (x *')) = len (x *') by Th3;
A9: (Im a) * (Im x) = (z6 * (- ((1 / 2) * <i>))) * (x - (x *')) by Th53
.= (((- ((1 / 2) * <i>)) * z6) * x) - (((- ((1 / 2) * <i>)) * z6) * (x *')) by A1, Th43 ;
A10: len (((- ((1 / 2) * <i>)) * z6) * x) = len x by Th3;
A11: ( len (z5 * (x *')) = len (x *') & len ((z6 * <i>) * (x *')) = len (x *') ) by Th3;
A12: ( len (((1 / 2) * z5) * (x *')) = len (x *') & len ((((1 / 2) * <i>) * z6) * x) = len x ) by Th3;
A13: Re (a * x) = (1 / 2) * (((a *') * (x *')) + (a * x)) by Th17
.= (1 / 2) * (((a *') * (x *')) + ((z5 + (<i> * z6)) * x)) by COMPLEX1:13
.= (1 / 2) * (((z5 - (z6 * <i>)) * (x *')) + ((z5 + (<i> * z6)) * x)) by COMPLEX1:def_11
.= ((1 / 2) * ((z5 - (z6 * <i>)) * (x *'))) + ((1 / 2) * ((z5 + (<i> * z6)) * x)) by A1, A7, Th30
.= ((1 / 2) * ((z5 - (z6 * <i>)) * (x *'))) + ((1 / 2) * ((z5 * x) + ((<i> * z6) * x))) by Th63
.= ((1 / 2) * ((z5 * (x *')) - ((z6 * <i>) * (x *')))) + ((1 / 2) * ((z5 * x) + ((<i> * z6) * x))) by Th64
.= ((1 / 2) * ((z5 * (x *')) - ((z6 * <i>) * (x *')))) + (((1 / 2) * (z5 * x)) + ((1 / 2) * ((<i> * z6) * x))) by A4, Th30
.= (((1 / 2) * (z5 * (x *'))) - ((1 / 2) * ((z6 * <i>) * (x *')))) + (((1 / 2) * (z5 * x)) + ((1 / 2) * ((<i> * z6) * x))) by A11, Th43
.= (((1 / 2) * (z5 * (x *'))) - ((1 / 2) * ((<i> * z6) * (x *')))) + (((1 / 2) * (z5 * x)) + (((1 / 2) * (<i> * z6)) * x)) by Th53
.= (((1 / 2) * (z5 * (x *'))) + (- ((((1 / 2) * <i>) * z6) * (x *')))) + (((1 / 2) * (z5 * x)) + ((((1 / 2) * <i>) * z6) * x)) by Th53
.= (((1 / 2) * (z5 * (x *'))) + ((- (((1 / 2) * <i>) * z6)) * (x *'))) + (((1 / 2) * (z5 * x)) + ((((1 / 2) * <i>) * z6) * x)) by Th54
.= ((((1 / 2) * z5) * (x *')) + (((- ((1 / 2) * <i>)) * z6) * (x *'))) + (((1 / 2) * (z5 * x)) + ((((1 / 2) * <i>) * z6) * x)) by Th53
.= ((((1 / 2) * z5) * x) + ((((1 / 2) * <i>) * z6) * x)) + ((((1 / 2) * z5) * (x *')) + (((- ((1 / 2) * <i>)) * z6) * (x *'))) by Th53
.= ((((((1 / 2) * <i>) * z6) * x) + (((1 / 2) * z5) * x)) + (((1 / 2) * z5) * (x *'))) + (((- ((1 / 2) * <i>)) * z6) * (x *')) by A1, A8, A12, A2, Th28
.= (((((1 / 2) * z5) * x) + (((1 / 2) * z5) * (x *'))) + ((- ((- ((1 / 2) * <i>)) * z6)) * x)) + (((- ((1 / 2) * <i>)) * z6) * (x *')) by A1, A3, A12, Th28
.= (((((1 / 2) * z5) * x) + (((1 / 2) * z5) * (x *'))) - (((- ((1 / 2) * <i>)) * z6) * x)) + (((- ((1 / 2) * <i>)) * z6) * (x *')) by Th54
.= ((Re a) * (Re x)) - ((Im a) * (Im x)) by A1, A5, A9, A6, A10, A8, Th40 ;
A14: len ((((1 / 2) * <i>) * z5) * (x *')) = len (x *') by Th3;
A15: (Im a) * (Re x) = (z6 * (1 / 2)) * (x + (x *')) by Th53
.= (((1 / 2) * z6) * x) + (((1 / 2) * z6) * (x *')) by A1, Th30 ;
A16: ( len ((<i> * z6) * (x *')) = len (x *') & len ((- z5) * (x *')) = len (x *') ) by Th3;
A17: len ((1 / 2) * (z6 * x)) = len (z6 * x) by Th3;
A18: ( len (z6 * (x *')) = len (x *') & len ((1 / 2) * (z6 * (x *'))) = len (z6 * (x *')) ) by Th3;
then A19: len (((1 / 2) * (z6 * x)) + ((1 / 2) * (z6 * (x *')))) = len ((1 / 2) * (z6 * x)) by A1, A17, Th3, Th6;
A20: len (((- ((1 / 2) * <i>)) * z5) * x) = len x by Th3;
then A21: len (((1 / 2) * (z6 * x)) + (((- ((1 / 2) * <i>)) * z5) * x)) = len ((1 / 2) * (z6 * x)) by A17, Th3, Th6;
A22: (Re a) * (Im x) = (z5 * (- ((1 / 2) * <i>))) * (x - (x *')) by Th53
.= (((- ((1 / 2) * <i>)) * z5) * x) - (((- ((1 / 2) * <i>)) * z5) * (x *')) by A1, Th43 ;
A23: len (z6 * x) = len x by Th3;
 ( len ((a * x) *') = len (a * x) & len (- ((a * x) *')) = len ((a * x) *') ) by Def1, Th5;
then  Im (a * x) = ((- ((1 / 2) * <i>)) * (- ((a * x) *'))) + ((- ((1 / 2) * <i>)) * (a * x)) by Th30
.= ((- ((1 / 2) * <i>)) * (- ((a *') * (x *')))) + ((- ((1 / 2) * <i>)) * (a * x)) by Th17
.= ((- ((1 / 2) * <i>)) * (- ((a *') * (x *')))) + ((- ((1 / 2) * <i>)) * ((z5 + (<i> * z6)) * x)) by COMPLEX1:13
.= ((- ((1 / 2) * <i>)) * (- ((z5 - (z6 * <i>)) * (x *')))) + ((- ((1 / 2) * <i>)) * ((z5 + (<i> * z6)) * x)) by COMPLEX1:def_11
.= ((- ((1 / 2) * <i>)) * ((- (z5 - (z6 * <i>))) * (x *'))) + ((- ((1 / 2) * <i>)) * ((z5 + (<i> * z6)) * x)) by Th54
.= ((- ((1 / 2) * <i>)) * (((- z5) + (z6 * <i>)) * (x *'))) + ((- ((1 / 2) * <i>)) * ((z5 + (<i> * z6)) * x))
.= ((- ((1 / 2) * <i>)) * (((- z5) * (x *')) + ((<i> * z6) * (x *')))) + ((- ((1 / 2) * <i>)) * ((z5 + (<i> * z6)) * x)) by Th63
.= ((- ((1 / 2) * <i>)) * (((- z5) * (x *')) + ((<i> * z6) * (x *')))) + ((- ((1 / 2) * <i>)) * ((z5 * x) + ((<i> * z6) * x))) by Th63
.= ((- ((1 / 2) * <i>)) * (((- z5) * (x *')) + ((<i> * z6) * (x *')))) + (((- ((1 / 2) * <i>)) * (z5 * x)) + ((- ((1 / 2) * <i>)) * ((<i> * z6) * x))) by A4, Th30
.= (((- ((1 / 2) * <i>)) * ((- z5) * (x *'))) + ((- ((1 / 2) * <i>)) * ((<i> * z6) * (x *')))) + (((- ((1 / 2) * <i>)) * (z5 * x)) + ((- ((1 / 2) * <i>)) * ((<i> * z6) * x))) by A16, Th30
.= ((((- ((1 / 2) * <i>)) * (- z5)) * (x *')) + ((- ((1 / 2) * <i>)) * ((<i> * z6) * (x *')))) + (((- ((1 / 2) * <i>)) * (z5 * x)) + ((- ((1 / 2) * <i>)) * ((<i> * z6) * x))) by Th53
.= ((((- ((1 / 2) * <i>)) * (- z5)) * (x *')) + ((- ((1 / 2) * <i>)) * (<i> * (z6 * (x *'))))) + (((- ((1 / 2) * <i>)) * (z5 * x)) + ((- ((1 / 2) * <i>)) * ((<i> * z6) * x))) by Th53
.= ((((- ((1 / 2) * <i>)) * (- z5)) * (x *')) + (((- ((1 / 2) * <i>)) * <i>) * (z6 * (x *')))) + (((- ((1 / 2) * <i>)) * (z5 * x)) + ((- ((1 / 2) * <i>)) * ((<i> * z6) * x))) by Th53
.= ((((- ((1 / 2) * <i>)) * (- z5)) * (x *')) + (((- ((1 / 2) * <i>)) * <i>) * (z6 * (x *')))) + ((((- ((1 / 2) * <i>)) * z5) * x) + ((- ((1 / 2) * <i>)) * ((<i> * z6) * x))) by Th53
.= ((((- ((1 / 2) * <i>)) * (- z5)) * (x *')) + (((- ((1 / 2) * <i>)) * <i>) * (z6 * (x *')))) + ((((- ((1 / 2) * <i>)) * z5) * x) + ((- ((1 / 2) * <i>)) * (<i> * (z6 * x)))) by Th53
.= (((1 / 2) * (z6 * x)) + (((- ((1 / 2) * <i>)) * z5) * x)) + (((1 / 2) * (z6 * (x *'))) + ((((1 / 2) * <i>) * z5) * (x *'))) by Th53
.= ((((1 / 2) * (z6 * x)) + (((- ((1 / 2) * <i>)) * z5) * x)) + ((1 / 2) * (z6 * (x *')))) + ((((1 / 2) * <i>) * z5) * (x *')) by A1, A23, A17, A18, A14, A21, Th28
.= ((((1 / 2) * (z6 * x)) + ((1 / 2) * (z6 * (x *')))) + (((- ((1 / 2) * <i>)) * z5) * x)) + ((((1 / 2) * <i>) * z5) * (x *')) by A1, A23, A17, A20, A18, Th28
.= (((1 / 2) * (z6 * x)) + ((1 / 2) * (z6 * (x *')))) + ((((- ((1 / 2) * <i>)) * z5) * x) + ((((1 / 2) * <i>) * z5) * (x *'))) by A1, A23, A17, A20, A14, A19, Th28
.= ((((1 / 2) * z6) * x) + ((1 / 2) * (z6 * (x *')))) + ((((- ((1 / 2) * <i>)) * z5) * x) + ((((1 / 2) * <i>) * z5) * (x *'))) by Th53
.= ((((1 / 2) * z6) * x) + (((1 / 2) * z6) * (x *'))) + ((((- ((1 / 2) * <i>)) * z5) * x) + ((- ((- ((1 / 2) * <i>)) * z5)) * (x *'))) by Th53
.= ((Im a) * (Re x)) + ((Re a) * (Im x)) by A15, A22, Th54 ;
hence  ( Re (a * x) = ((Re a) * (Re x)) - ((Im a) * (Im x)) & Im (a * x) = ((Im a) * (Re x)) + ((Re a) * (Im x)) ) by A13; ::_thesis: verum
end;

begin

theorem Th66: :: COMPLSP2:66
for x1, x2, y being FinSequence of COMPLEX st len x1 = len x2 & len x2 = len y holds
|((x1 + x2),y)| = |(x1,y)| + |(x2,y)|
proof
let x1, x2, y be FinSequence of COMPLEX ; ::_thesis: ( len x1 = len x2 & len x2 = len y implies |((x1 + x2),y)| = |(x1,y)| + |(x2,y)| )
assume that
A1: len x1 = len x2 and
A2: len x2 = len y ; ::_thesis: |((x1 + x2),y)| = |(x1,y)| + |(x2,y)|
A3: ( len (Re x1) = len x1 & len (Re x2) = len x2 ) by Th48;
A4: len (Im y) = len y by Th48;
A5: ( len (Im x1) = len x1 & len (Im x2) = len x2 ) by Th48;
A6: len (Re y) = len y by Th48;
|((x1 + x2),y)| = ((|(((Re x1) + (Re x2)),(Re y))| - (<i> * |((Re (x1 + x2)),(Im y))|)) + (<i> * |((Im (x1 + x2)),(Re y))|)) + |((Im (x1 + x2)),(Im y))| by A1, Th49
.= ((|(((Re x1) + (Re x2)),(Re y))| - (<i> * |(((Re x1) + (Re x2)),(Im y))|)) + (<i> * |((Im (x1 + x2)),(Re y))|)) + |((Im (x1 + x2)),(Im y))| by A1, Th49
.= ((|(((Re x1) + (Re x2)),(Re y))| - (<i> * |(((Re x1) + (Re x2)),(Im y))|)) + (<i> * |(((Im x1) + (Im x2)),(Re y))|)) + |((Im (x1 + x2)),(Im y))| by A1, Th49
.= ((|(((Re x1) + (Re x2)),(Re y))| - (<i> * |(((Re x1) + (Re x2)),(Im y))|)) + (<i> * |(((Im x1) + (Im x2)),(Re y))|)) + |(((Im x1) + (Im x2)),(Im y))| by A1, Th49
.= (((|((Re x1),(Re y))| + |((Re x2),(Re y))|) - (<i> * |(((Re x1) + (Re x2)),(Im y))|)) + (<i> * |(((Im x1) + (Im x2)),(Re y))|)) + |(((Im x1) + (Im x2)),(Im y))| by A1, A2, A3, A6, RVSUM_1:120
.= (((|((Re x1),(Re y))| + |((Re x2),(Re y))|) - (<i> * (|((Re x1),(Im y))| + |((Re x2),(Im y))|))) + (<i> * |(((Im x1) + (Im x2)),(Re y))|)) + |(((Im x1) + (Im x2)),(Im y))| by A1, A2, A3, A4, RVSUM_1:120
.= (((|((Re x1),(Re y))| + |((Re x2),(Re y))|) - (<i> * (|((Re x1),(Im y))| + |((Re x2),(Im y))|))) + (<i> * (|((Im x1),(Re y))| + |((Im x2),(Re y))|))) + |(((Im x1) + (Im x2)),(Im y))| by A1, A2, A6, A5, RVSUM_1:120
.= (((|((Re x1),(Re y))| + |((Re x2),(Re y))|) - (<i> * (|((Re x1),(Im y))| + |((Re x2),(Im y))|))) + (<i> * (|((Im x1),(Re y))| + |((Im x2),(Re y))|))) + (|((Im x1),(Im y))| + |((Im x2),(Im y))|) by A1, A2, A5, A4, RVSUM_1:120
.= |(x1,y)| + |(x2,y)| ;
hence  |((x1 + x2),y)| = |(x1,y)| + |(x2,y)| ; ::_thesis: verum
end;

theorem Th67: :: COMPLSP2:67
for x1, x2 being FinSequence of COMPLEX st len x1 = len x2 holds
|((- x1),x2)| = - |(x1,x2)|
proof
let x1, x2 be FinSequence of COMPLEX ; ::_thesis: ( len x1 = len x2 implies |((- x1),x2)| = - |(x1,x2)| )
assume A1: len x1 = len x2 ; ::_thesis: |((- x1),x2)| = - |(x1,x2)|
A2: len (<i> * x1) = len x1 by Th3;
|((- x1),x2)| = |(((<i> * <i>) * x1),x2)|
.= |((<i> * (<i> * x1)),x2)| by Th53
.= <i> * |((<i> * x1),x2)| by A1, A2, Th59
.= <i> * (<i> * |(x1,x2)|) by A1, Th59
.= (- 1) * |(x1,x2)| ;
hence  |((- x1),x2)| = - |(x1,x2)| ; ::_thesis: verum
end;

theorem Th68: :: COMPLSP2:68
for x1, x2 being FinSequence of COMPLEX st len x1 = len x2 holds
|(x1,(- x2))| = - |(x1,x2)|
proof
let x1, x2 be FinSequence of COMPLEX ; ::_thesis: ( len x1 = len x2 implies |(x1,(- x2))| = - |(x1,x2)| )
assume A1: len x1 = len x2 ; ::_thesis: |(x1,(- x2))| = - |(x1,x2)|
A2: len (<i> * x2) = len x2 by Th3;
|(x1,(- x2))| = |(x1,((<i> * <i>) * x2))|
.= |(x1,(<i> * (<i> * x2)))| by Th53
.= - (<i> * |(x1,(<i> * x2))|) by A1, A2, Th60
.= - (<i> * (- (<i> * |(x1,x2)|))) by A1, Th60
.= - |(x1,x2)| ;
hence  |(x1,(- x2))| = - |(x1,x2)| ; ::_thesis: verum
end;

theorem :: COMPLSP2:69
for x1, x2 being FinSequence of COMPLEX st len x1 = len x2 holds
|((- x1),(- x2))| = |(x1,x2)|
proof
let x1, x2 be FinSequence of COMPLEX ; ::_thesis: ( len x1 = len x2 implies |((- x1),(- x2))| = |(x1,x2)| )
assume A1: len x1 = len x2 ; ::_thesis: |((- x1),(- x2))| = |(x1,x2)|
then  len (- x2) = len x1 by Th5;
then |((- x1),(- x2))| = - |(x1,(- x2))| by Th67
.= - (- |(x1,x2)|) by A1, Th68 ;
hence  |((- x1),(- x2))| = |(x1,x2)| ; ::_thesis: verum
end;

theorem Th70: :: COMPLSP2:70
for x1, x2, x3 being FinSequence of COMPLEX st len x1 = len x2 & len x2 = len x3 holds
|((x1 - x2),x3)| = |(x1,x3)| - |(x2,x3)|
proof
let x1, x2, x3 be FinSequence of COMPLEX ; ::_thesis: ( len x1 = len x2 & len x2 = len x3 implies |((x1 - x2),x3)| = |(x1,x3)| - |(x2,x3)| )
assume that
A1: len x1 = len x2 and
A2: len x2 = len x3 ; ::_thesis: |((x1 - x2),x3)| = |(x1,x3)| - |(x2,x3)|
 len (- x2) = len x2 by Th5;
then |((x1 - x2),x3)| = |(x1,x3)| + |((- x2),x3)| by A1, A2, Th66
.= |(x1,x3)| + (- |(x2,x3)|) by A2, Th67 ;
hence  |((x1 - x2),x3)| = |(x1,x3)| - |(x2,x3)| ; ::_thesis: verum
end;

theorem Th71: :: COMPLSP2:71
for x, y1, y2 being FinSequence of COMPLEX st len x = len y1 & len y1 = len y2 holds
|(x,(y1 + y2))| = |(x,y1)| + |(x,y2)|
proof
let x, y1, y2 be FinSequence of COMPLEX ; ::_thesis: ( len x = len y1 & len y1 = len y2 implies |(x,(y1 + y2))| = |(x,y1)| + |(x,y2)| )
assume that
A1: len x = len y1 and
A2: len y1 = len y2 ; ::_thesis: |(x,(y1 + y2))| = |(x,y1)| + |(x,y2)|
A3: ( len (Re y1) = len y1 & len (Re y2) = len y2 ) by Th48;
A4: len (Im x) = len x by Th48;
A5: ( len (Im y1) = len y1 & len (Im y2) = len y2 ) by Th48;
A6: len (Re x) = len x by Th48;
|(x,(y1 + y2))| = ((|((Re x),((Re y1) + (Re y2)))| - (<i> * |((Re x),(Im (y1 + y2)))|)) + (<i> * |((Im x),(Re (y1 + y2)))|)) + |((Im x),(Im (y1 + y2)))| by A2, Th49
.= ((|((Re x),((Re y1) + (Re y2)))| - (<i> * |((Re x),(Im (y1 + y2)))|)) + (<i> * |((Im x),(Re (y1 + y2)))|)) + |((Im x),((Im y1) + (Im y2)))| by A2, Th49
.= ((|((Re x),((Re y1) + (Re y2)))| - (<i> * |((Re x),((Im y1) + (Im y2)))|)) + (<i> * |((Im x),(Re (y1 + y2)))|)) + |((Im x),((Im y1) + (Im y2)))| by A2, Th49
.= ((|((Re x),((Re y1) + (Re y2)))| - (<i> * |((Re x),((Im y1) + (Im y2)))|)) + (<i> * |((Im x),((Re y1) + (Re y2)))|)) + |((Im x),((Im y1) + (Im y2)))| by A2, Th49
.= (((|((Re x),(Re y1))| + |((Re x),(Re y2))|) - (<i> * |((Re x),((Im y1) + (Im y2)))|)) + (<i> * |((Im x),((Re y1) + (Re y2)))|)) + |((Im x),((Im y1) + (Im y2)))| by A1, A2, A3, A6, RVSUM_1:120
.= (((|((Re x),(Re y1))| + |((Re x),(Re y2))|) - (<i> * |((Re x),((Im y1) + (Im y2)))|)) + (<i> * |((Im x),((Re y1) + (Re y2)))|)) + (|((Im x),(Im y1))| + |((Im x),(Im y2))|) by A1, A2, A5, A4, RVSUM_1:120
.= (((|((Re x),(Re y1))| + |((Re x),(Re y2))|) - (<i> * (|((Re x),(Im y1))| + |((Re x),(Im y2))|))) + (<i> * |((Im x),((Re y1) + (Re y2)))|)) + (|((Im x),(Im y1))| + |((Im x),(Im y2))|) by A1, A2, A6, A5, RVSUM_1:120
.= (((|((Re x),(Re y1))| + |((Re x),(Re y2))|) - (<i> * (|((Re x),(Im y1))| + |((Re x),(Im y2))|))) + (<i> * (|((Im x),(Re y1))| + |((Im x),(Re y2))|))) + (|((Im x),(Im y1))| + |((Im x),(Im y2))|) by A1, A2, A3, A4, RVSUM_1:120
.= |(x,y1)| + |(x,y2)| ;
hence  |(x,(y1 + y2))| = |(x,y1)| + |(x,y2)| ; ::_thesis: verum
end;

theorem Th72: :: COMPLSP2:72
for x, y1, y2 being FinSequence of COMPLEX st len x = len y1 & len y1 = len y2 holds
|(x,(y1 - y2))| = |(x,y1)| - |(x,y2)|
proof
let x, y1, y2 be FinSequence of COMPLEX ; ::_thesis: ( len x = len y1 & len y1 = len y2 implies |(x,(y1 - y2))| = |(x,y1)| - |(x,y2)| )
assume that
A1: len x = len y1 and
A2: len y1 = len y2 ; ::_thesis: |(x,(y1 - y2))| = |(x,y1)| - |(x,y2)|
A3: ( len (Re y1) = len y1 & len (Re y2) = len y2 ) by Th48;
A4: len (Im x) = len x by Th48;
A5: ( len (Im y1) = len y1 & len (Im y2) = len y2 ) by Th48;
A6: len (Re x) = len x by Th48;
|(x,(y1 - y2))| = ((|((Re x),((Re y1) - (Re y2)))| - (<i> * |((Re x),(Im (y1 - y2)))|)) + (<i> * |((Im x),(Re (y1 - y2)))|)) + |((Im x),(Im (y1 - y2)))| by A2, Th52
.= ((|((Re x),((Re y1) - (Re y2)))| - (<i> * |((Re x),(Im (y1 - y2)))|)) + (<i> * |((Im x),(Re (y1 - y2)))|)) + |((Im x),((Im y1) - (Im y2)))| by A2, Th52
.= ((|((Re x),((Re y1) - (Re y2)))| - (<i> * |((Re x),((Im y1) - (Im y2)))|)) + (<i> * |((Im x),(Re (y1 - y2)))|)) + |((Im x),((Im y1) - (Im y2)))| by A2, Th52
.= ((|((Re x),((Re y1) - (Re y2)))| - (<i> * |((Re x),((Im y1) - (Im y2)))|)) + (<i> * |((Im x),((Re y1) - (Re y2)))|)) + |((Im x),((Im y1) - (Im y2)))| by A2, Th52
.= (((|((Re x),(Re y1))| - |((Re x),(Re y2))|) - (<i> * |((Re x),((Im y1) - (Im y2)))|)) + (<i> * |((Im x),((Re y1) - (Re y2)))|)) + |((Im x),((Im y1) - (Im y2)))| by A1, A2, A3, A6, RVSUM_1:124
.= (((|((Re x),(Re y1))| - |((Re x),(Re y2))|) - (<i> * |((Re x),((Im y1) - (Im y2)))|)) + (<i> * |((Im x),((Re y1) - (Re y2)))|)) + (|((Im x),(Im y1))| - |((Im x),(Im y2))|) by A1, A2, A5, A4, RVSUM_1:124
.= (((|((Re x),(Re y1))| - |((Re x),(Re y2))|) - (<i> * (|((Re x),(Im y1))| - |((Re x),(Im y2))|))) + (<i> * |((Im x),((Re y1) - (Re y2)))|)) + (|((Im x),(Im y1))| - |((Im x),(Im y2))|) by A1, A2, A6, A5, RVSUM_1:124
.= (((|((Re x),(Re y1))| - |((Re x),(Re y2))|) - (<i> * (|((Re x),(Im y1))| - |((Re x),(Im y2))|))) + (<i> * (|((Im x),(Re y1))| - |((Im x),(Re y2))|))) + (|((Im x),(Im y1))| - |((Im x),(Im y2))|) by A1, A2, A3, A4, RVSUM_1:124
.= |(x,y1)| - |(x,y2)| ;
hence  |(x,(y1 - y2))| = |(x,y1)| - |(x,y2)| ; ::_thesis: verum
end;

theorem Th73: :: COMPLSP2:73
for x1, x2, y1, y2 being FinSequence of COMPLEX st len x1 = len x2 & len x2 = len y1 & len y1 = len y2 holds
|((x1 + x2),(y1 + y2))| = ((|(x1,y1)| + |(x1,y2)|) + |(x2,y1)|) + |(x2,y2)|
proof
let x1, x2, y1, y2 be FinSequence of COMPLEX ; ::_thesis: ( len x1 = len x2 & len x2 = len y1 & len y1 = len y2 implies |((x1 + x2),(y1 + y2))| = ((|(x1,y1)| + |(x1,y2)|) + |(x2,y1)|) + |(x2,y2)| )
assume that
A1: len x1 = len x2 and
A2: len x2 = len y1 and
A3: len y1 = len y2 ; ::_thesis: |((x1 + x2),(y1 + y2))| = ((|(x1,y1)| + |(x1,y2)|) + |(x2,y1)|) + |(x2,y2)|
 |((x1 + x2),y2)| = |(x1,y2)| + |(x2,y2)| by A1, A2, A3, Th66;
then A4: |((x1 + x2),y1)| + |((x1 + x2),y2)| = (|(x1,y1)| + |(x2,y1)|) + (|(x1,y2)| + |(x2,y2)|) by A1, A2, Th66;
 len (x1 + x2) = len x1 by A1, Th6;
hence  |((x1 + x2),(y1 + y2))| = ((|(x1,y1)| + |(x1,y2)|) + |(x2,y1)|) + |(x2,y2)| by A1, A2, A3, A4, Th71; ::_thesis: verum
end;

theorem Th74: :: COMPLSP2:74
for x1, x2, y1, y2 being FinSequence of COMPLEX st len x1 = len x2 & len x2 = len y1 & len y1 = len y2 holds
|((x1 - x2),(y1 - y2))| = ((|(x1,y1)| - |(x1,y2)|) - |(x2,y1)|) + |(x2,y2)|
proof
let x1, x2, y1, y2 be FinSequence of COMPLEX ; ::_thesis: ( len x1 = len x2 & len x2 = len y1 & len y1 = len y2 implies |((x1 - x2),(y1 - y2))| = ((|(x1,y1)| - |(x1,y2)|) - |(x2,y1)|) + |(x2,y2)| )
assume that
A1: len x1 = len x2 and
A2: len x2 = len y1 and
A3: len y1 = len y2 ; ::_thesis: |((x1 - x2),(y1 - y2))| = ((|(x1,y1)| - |(x1,y2)|) - |(x2,y1)|) + |(x2,y2)|
 |(x1,(y1 - y2))| = |(x1,y1)| - |(x1,y2)| by A1, A2, A3, Th72;
then A4: |(x1,(y1 - y2))| - |(x2,(y1 - y2))| = (|(x1,y1)| - |(x1,y2)|) - (|(x2,y1)| - |(x2,y2)|) by A2, A3, Th72;
 len (y1 - y2) = len y1 by A3, Th7;
hence  |((x1 - x2),(y1 - y2))| = ((|(x1,y1)| - |(x1,y2)|) - |(x2,y1)|) + |(x2,y2)| by A1, A2, A4, Th70; ::_thesis: verum
end;

theorem Th75: :: COMPLSP2:75
for x, y being FinSequence of COMPLEX holds |(x,y)| = |(y,x)| *'
proof
let x, y be FinSequence of COMPLEX ; ::_thesis: |(x,y)| = |(y,x)| *'
set x1 = |((Re y),(Re x))|;
set x2 = |((Re y),(Im x))|;
set y1 = |((Im y),(Re x))|;
set y2 = |((Im y),(Im x))|;
reconsider x19 = |((Re y),(Re x))|, x29 = |((Re y),(Im x))|, y19 = |((Im y),(Re x))|, y29 = |((Im y),(Im x))| as Element of REAL ;
A1: Im x19 = 0 by COMPLEX1:def_2;
A2: Im x29 = 0 by COMPLEX1:def_2;
A3: Im y29 = 0 by COMPLEX1:def_2;
A4: Im y19 = 0 by COMPLEX1:def_2;
reconsider x19 = |((Re y),(Re x))|, x29 = |((Re y),(Im x))|, y19 = |((Im y),(Re x))|, y29 = |((Im y),(Im x))| as Element of COMPLEX by XCMPLX_0:def_2;
|(y,x)| *' = ((x19 + y29) + (<i> * (y19 - x29))) *'
.= ((x19 + y29) *') + ((<i> * (y19 - x29)) *') by COMPLEX1:32
.= ((x19 *') + (y29 *')) + ((<i> * (y19 - x29)) *') by COMPLEX1:32
.= (x19 + (y29 *')) + ((<i> * (y19 - x29)) *') by A1, COMPLEX1:38
.= (x19 + y29) + ((<i> * (y19 - x29)) *') by A3, COMPLEX1:38
.= (x19 + y29) + ((- <i>) * ((y19 - x29) *')) by COMPLEX1:31, COMPLEX1:35
.= (x19 + y29) + ((- <i>) * ((y19 *') - (x29 *'))) by COMPLEX1:34
.= (x19 + y29) + ((- <i>) * (y19 - (x29 *'))) by A4, COMPLEX1:38
.= (x19 + y29) + ((- <i>) * (y19 - x29)) by A2, COMPLEX1:38
.= |(x,y)| ;
hence  |(x,y)| = |(y,x)| *' ; ::_thesis: verum
end;

theorem :: COMPLSP2:76
for x, y being FinSequence of COMPLEX st len x = len y holds
|((x + y),(x + y))| = (|(x,x)| + (2 * (Re |(x,y)|))) + |(y,y)|
proof
let x, y be FinSequence of COMPLEX ; ::_thesis: ( len x = len y implies |((x + y),(x + y))| = (|(x,x)| + (2 * (Re |(x,y)|))) + |(y,y)| )
set z = |(x,y)|;
assume  len x = len y ; ::_thesis: |((x + y),(x + y))| = (|(x,x)| + (2 * (Re |(x,y)|))) + |(y,y)|
then |((x + y),(x + y))| = ((|(x,x)| + |(x,y)|) + |(y,x)|) + |(y,y)| by Th73
.= ((|(x,x)| + |(x,y)|) + (|(x,y)| *')) + |(y,y)| by Th75
.= (|(x,x)| + (|(x,y)| + (|(x,y)| *'))) + |(y,y)|
.= (|(x,x)| + (2 * (Re |(x,y)|))) + |(y,y)| by Th24 ;
hence  |((x + y),(x + y))| = (|(x,x)| + (2 * (Re |(x,y)|))) + |(y,y)| ; ::_thesis: verum
end;

theorem :: COMPLSP2:77
for x, y being FinSequence of COMPLEX st len x = len y holds
|((x - y),(x - y))| = (|(x,x)| - (2 * (Re |(x,y)|))) + |(y,y)|
proof
let x, y be FinSequence of COMPLEX ; ::_thesis: ( len x = len y implies |((x - y),(x - y))| = (|(x,x)| - (2 * (Re |(x,y)|))) + |(y,y)| )
set z = |(x,y)|;
assume  len x = len y ; ::_thesis: |((x - y),(x - y))| = (|(x,x)| - (2 * (Re |(x,y)|))) + |(y,y)|
then |((x - y),(x - y))| = ((|(x,x)| - |(x,y)|) - |(y,x)|) + |(y,y)| by Th74
.= ((|(x,x)| - |(x,y)|) - (|(x,y)| *')) + |(y,y)| by Th75
.= (|(x,x)| - (|(x,y)| + (|(x,y)| *'))) + |(y,y)|
.= (|(x,x)| - (2 * (Re |(x,y)|))) + |(y,y)| by Th24 ;
hence  |((x - y),(x - y))| = (|(x,x)| - (2 * (Re |(x,y)|))) + |(y,y)| ; ::_thesis: verum
end;

theorem Th78: :: COMPLSP2:78
for a being Element of COMPLEX
for x, y being FinSequence of COMPLEX st len x = len y holds
|((a * x),y)| = a * |(x,y)|
proof
let a be Element of COMPLEX ; ::_thesis: for x, y being FinSequence of COMPLEX st len x = len y holds
|((a * x),y)| = a * |(x,y)|
let x, y be FinSequence of COMPLEX ; ::_thesis: ( len x = len y implies |((a * x),y)| = a * |(x,y)| )
assume A1: len x = len y ; ::_thesis: |((a * x),y)| = a * |(x,y)|
A2: ( len ((Re a) * (Im x)) = len (Im x) & len ((Im a) * (Re x)) = len (Re x) ) by RVSUM_1:117;
A3: ( len ((Re a) * (Re x)) = len (Re x) & len ((Im a) * (Im x)) = len (Im x) ) by RVSUM_1:117;
A4: len (Re x) = len x by Th48;
A5: len (Im y) = len y by Th48;
A6: len (Re y) = len y by Th48;
A7: len (Im x) = len x by Th48;
|((a * x),y)| = ((|((((Re a) * (Re x)) - ((Im a) * (Im x))),(Re y))| - (<i> * |((Re (a * x)),(Im y))|)) + (<i> * |((Im (a * x)),(Re y))|)) + |((Im (a * x)),(Im y))| by Th65
.= ((|((((Re a) * (Re x)) - ((Im a) * (Im x))),(Re y))| - (<i> * |((((Re a) * (Re x)) - ((Im a) * (Im x))),(Im y))|)) + (<i> * |((Im (a * x)),(Re y))|)) + |((Im (a * x)),(Im y))| by Th65
.= ((|((((Re a) * (Re x)) - ((Im a) * (Im x))),(Re y))| - (<i> * |((((Re a) * (Re x)) - ((Im a) * (Im x))),(Im y))|)) + (<i> * |((((Im a) * (Re x)) + ((Re a) * (Im x))),(Re y))|)) + |((Im (a * x)),(Im y))| by Th65
.= ((|((((Re a) * (Re x)) - ((Im a) * (Im x))),(Re y))| - (<i> * |((((Re a) * (Re x)) - ((Im a) * (Im x))),(Im y))|)) + (<i> * |((((Im a) * (Re x)) + ((Re a) * (Im x))),(Re y))|)) + |((((Im a) * (Re x)) + ((Re a) * (Im x))),(Im y))| by Th65
.= (((|(((Re a) * (Re x)),(Re y))| - |(((Im a) * (Im x)),(Re y))|) - (<i> * |((((Re a) * (Re x)) - ((Im a) * (Im x))),(Im y))|)) + (<i> * |((((Im a) * (Re x)) + ((Re a) * (Im x))),(Re y))|)) + |((((Im a) * (Re x)) + ((Re a) * (Im x))),(Im y))| by A1, A4, A6, A7, A3, RVSUM_1:124
.= (((|(((Re a) * (Re x)),(Re y))| - |(((Im a) * (Im x)),(Re y))|) - (<i> * (|(((Re a) * (Re x)),(Im y))| - |(((Im a) * (Im x)),(Im y))|))) + (<i> * |((((Im a) * (Re x)) + ((Re a) * (Im x))),(Re y))|)) + |((((Im a) * (Re x)) + ((Re a) * (Im x))),(Im y))| by A1, A4, A7, A5, A3, RVSUM_1:124
.= (((|(((Re a) * (Re x)),(Re y))| - |(((Im a) * (Im x)),(Re y))|) - (<i> * (|(((Re a) * (Re x)),(Im y))| - |(((Im a) * (Im x)),(Im y))|))) + (<i> * (|(((Im a) * (Re x)),(Re y))| + |(((Re a) * (Im x)),(Re y))|))) + |((((Im a) * (Re x)) + ((Re a) * (Im x))),(Im y))| by A1, A4, A6, A7, A2, RVSUM_1:120
.= (((|(((Re a) * (Re x)),(Re y))| - |(((Im a) * (Im x)),(Re y))|) - (<i> * (|(((Re a) * (Re x)),(Im y))| - |(((Im a) * (Im x)),(Im y))|))) + (<i> * (|(((Im a) * (Re x)),(Re y))| + |(((Re a) * (Im x)),(Re y))|))) + (|(((Im a) * (Re x)),(Im y))| + |(((Re a) * (Im x)),(Im y))|) by A1, A4, A7, A5, A2, RVSUM_1:120
.= (((|(((Re a) * (Re x)),(Re y))| - |(((Im a) * (Im x)),(Re y))|) - (<i> * (((Re a) * |((Re x),(Im y))|) - |(((Im a) * (Im x)),(Im y))|))) + (<i> * (|(((Im a) * (Re x)),(Re y))| + |(((Re a) * (Im x)),(Re y))|))) + (|(((Im a) * (Re x)),(Im y))| + |(((Re a) * (Im x)),(Im y))|) by A1, A4, A5, RVSUM_1:121
.= (((|(((Re a) * (Re x)),(Re y))| - |(((Im a) * (Im x)),(Re y))|) - (<i> * (((Re a) * |((Re x),(Im y))|) - ((Im a) * |((Im x),(Im y))|)))) + (<i> * (|(((Im a) * (Re x)),(Re y))| + |(((Re a) * (Im x)),(Re y))|))) + (|(((Im a) * (Re x)),(Im y))| + |(((Re a) * (Im x)),(Im y))|) by A1, A7, A5, RVSUM_1:121
.= (((((Re a) * |((Re x),(Re y))|) - |(((Im a) * (Im x)),(Re y))|) - (<i> * (((Re a) * |((Re x),(Im y))|) - ((Im a) * |((Im x),(Im y))|)))) + (<i> * (|(((Im a) * (Re x)),(Re y))| + |(((Re a) * (Im x)),(Re y))|))) + (|(((Im a) * (Re x)),(Im y))| + |(((Re a) * (Im x)),(Im y))|) by A1, A4, A6, RVSUM_1:121
.= (((((Re a) * |((Re x),(Re y))|) - ((Im a) * |((Im x),(Re y))|)) - (<i> * (((Re a) * |((Re x),(Im y))|) - ((Im a) * |((Im x),(Im y))|)))) + (<i> * (|(((Im a) * (Re x)),(Re y))| + |(((Re a) * (Im x)),(Re y))|))) + (|(((Im a) * (Re x)),(Im y))| + |(((Re a) * (Im x)),(Im y))|) by A1, A6, A7, RVSUM_1:121
.= (((((Re a) * |((Re x),(Re y))|) - ((Im a) * |((Im x),(Re y))|)) - (<i> * (((Re a) * |((Re x),(Im y))|) - ((Im a) * |((Im x),(Im y))|)))) + (<i> * (((Im a) * |((Re x),(Re y))|) + |(((Re a) * (Im x)),(Re y))|))) + (|(((Im a) * (Re x)),(Im y))| + |(((Re a) * (Im x)),(Im y))|) by A1, A4, A6, RVSUM_1:121
.= (((((Re a) * |((Re x),(Re y))|) - ((Im a) * |((Im x),(Re y))|)) - (<i> * (((Re a) * |((Re x),(Im y))|) - ((Im a) * |((Im x),(Im y))|)))) + (<i> * (((Im a) * |((Re x),(Re y))|) + ((Re a) * |((Im x),(Re y))|)))) + (|(((Im a) * (Re x)),(Im y))| + |(((Re a) * (Im x)),(Im y))|) by A1, A6, A7, RVSUM_1:121
.= (((((Re a) * |((Re x),(Re y))|) - ((Im a) * |((Im x),(Re y))|)) - (<i> * (((Re a) * |((Re x),(Im y))|) - ((Im a) * |((Im x),(Im y))|)))) + (<i> * (((Im a) * |((Re x),(Re y))|) + ((Re a) * |((Im x),(Re y))|)))) + (((Im a) * |((Re x),(Im y))|) + |(((Re a) * (Im x)),(Im y))|) by A1, A4, A5, RVSUM_1:121
.= (((((Re a) * |((Re x),(Re y))|) - ((Im a) * |((Im x),(Re y))|)) - (<i> * (((Re a) * |((Re x),(Im y))|) - ((Im a) * |((Im x),(Im y))|)))) + (<i> * (((Im a) * |((Re x),(Re y))|) + ((Re a) * |((Im x),(Re y))|)))) + (((Im a) * |((Re x),(Im y))|) + ((Re a) * |((Im x),(Im y))|)) by A1, A7, A5, RVSUM_1:121
.= ((((((Re a) * |((Re x),(Re y))|) + ((<i> * (Im a)) * |((Re x),(Re y))|)) - (((Re a) * <i>) * |((Re x),(Im y))|)) + ((Im a) * |((Re x),(Im y))|)) + (((Re a) * (<i> * |((Im x),(Re y))|)) - ((Im a) * |((Im x),(Re y))|))) + (((Re a) + (<i> * (Im a))) * |((Im x),(Im y))|)
.= ((((((Re a) * |((Re x),(Re y))|) + ((<i> * (Im a)) * |((Re x),(Re y))|)) - (((Re a) * <i>) * |((Re x),(Im y))|)) + ((Im a) * |((Re x),(Im y))|)) + (((Re a) + (<i> * (Im a))) * (<i> * |((Im x),(Re y))|))) + (a * |((Im x),(Im y))|) by COMPLEX1:13
.= (((((Re a) * |((Re x),(Re y))|) + ((<i> * (Im a)) * |((Re x),(Re y))|)) - (((Re a) + (<i> * (Im a))) * (<i> * |((Re x),(Im y))|))) + (a * (<i> * |((Im x),(Re y))|))) + (a * |((Im x),(Im y))|) by COMPLEX1:13
.= (((((Re a) + (<i> * (Im a))) * |((Re x),(Re y))|) - (a * (<i> * |((Re x),(Im y))|))) + (a * (<i> * |((Im x),(Re y))|))) + (a * |((Im x),(Im y))|) by COMPLEX1:13
.= (((a * |((Re x),(Re y))|) - (a * (<i> * |((Re x),(Im y))|))) + (a * (<i> * |((Im x),(Re y))|))) + (a * |((Im x),(Im y))|) by COMPLEX1:13
.= a * |(x,y)| ;
hence  |((a * x),y)| = a * |(x,y)| ; ::_thesis: verum
end;

theorem Th79: :: COMPLSP2:79
for a being Element of COMPLEX
for x, y being FinSequence of COMPLEX st len x = len y holds
|(x,(a * y))| = (a *') * |(x,y)|
proof
let a be Element of COMPLEX ; ::_thesis: for x, y being FinSequence of COMPLEX st len x = len y holds
|(x,(a * y))| = (a *') * |(x,y)|
let x, y be FinSequence of COMPLEX ; ::_thesis: ( len x = len y implies |(x,(a * y))| = (a *') * |(x,y)| )
assume A1: len x = len y ; ::_thesis: |(x,(a * y))| = (a *') * |(x,y)|
|(x,(a * y))| = |((a * y),x)| *' by Th75
.= (a * |(y,x)|) *' by A1, Th78
.= (a *') * (|(y,x)| *') by COMPLEX1:35
.= (a *') * |(x,y)| by Th75 ;
hence  |(x,(a * y))| = (a *') * |(x,y)| ; ::_thesis: verum
end;

theorem :: COMPLSP2:80
for a, b being Element of COMPLEX
for x, y, z being FinSequence of COMPLEX st len x = len y & len y = len z holds
|(((a * x) + (b * y)),z)| = (a * |(x,z)|) + (b * |(y,z)|)
proof
let a, b be Element of COMPLEX ; ::_thesis: for x, y, z being FinSequence of COMPLEX st len x = len y & len y = len z holds
|(((a * x) + (b * y)),z)| = (a * |(x,z)|) + (b * |(y,z)|)
let x, y, z be FinSequence of COMPLEX ; ::_thesis: ( len x = len y & len y = len z implies |(((a * x) + (b * y)),z)| = (a * |(x,z)|) + (b * |(y,z)|) )
assume that
A1: len x = len y and
A2: len y = len z ; ::_thesis: |(((a * x) + (b * y)),z)| = (a * |(x,z)|) + (b * |(y,z)|)
 ( len (a * x) = len x & len (b * y) = len y ) by Th3;
then |(((a * x) + (b * y)),z)| = |((a * x),z)| + |((b * y),z)| by A1, A2, Th66
.= (a * |(x,z)|) + |((b * y),z)| by A1, A2, Th78
.= (a * |(x,z)|) + (b * |(y,z)|) by A2, Th78 ;
hence  |(((a * x) + (b * y)),z)| = (a * |(x,z)|) + (b * |(y,z)|) ; ::_thesis: verum
end;

theorem :: COMPLSP2:81
for a, b being Element of COMPLEX
for x, y, z being FinSequence of COMPLEX st len x = len y & len y = len z holds
|(x,((a * y) + (b * z)))| = ((a *') * |(x,y)|) + ((b *') * |(x,z)|)
proof
let a, b be Element of COMPLEX ; ::_thesis: for x, y, z being FinSequence of COMPLEX st len x = len y & len y = len z holds
|(x,((a * y) + (b * z)))| = ((a *') * |(x,y)|) + ((b *') * |(x,z)|)
let x, y, z be FinSequence of COMPLEX ; ::_thesis: ( len x = len y & len y = len z implies |(x,((a * y) + (b * z)))| = ((a *') * |(x,y)|) + ((b *') * |(x,z)|) )
assume that
A1: len x = len y and
A2: len y = len z ; ::_thesis: |(x,((a * y) + (b * z)))| = ((a *') * |(x,y)|) + ((b *') * |(x,z)|)
 ( len (a * y) = len y & len (b * z) = len z ) by Th3;
then |(x,((a * y) + (b * z)))| = |(x,(a * y))| + |(x,(b * z))| by A1, A2, Th71
.= ((a *') * |(x,y)|) + |(x,(b * z))| by A1, Th79
.= ((a *') * |(x,y)|) + ((b *') * |(x,z)|) by A1, A2, Th79 ;
hence  |(x,((a * y) + (b * z)))| = ((a *') * |(x,y)|) + ((b *') * |(x,z)|) ; ::_thesis: verum
end;