:: Arithmetic Operations on Short Finite Sequences
:: by Rafa{\l} Ziobro
::
:: Received September 29, 2018
:: Copyright (c) 2018-2021 Association of Mizar Users

:: empty Relations are full of adjectives

registration

cluster Relation-like empty -> positive-yielding for set ;

coherence
for b₁ being Relation st b₁ is empty holds
b₁ is positive-yielding

proof end;

cluster Relation-like empty -> negative-yielding for set ;

coherence
for b₁ being Relation st b₁ is empty holds
b₁ is negative-yielding

proof end;

end;

registration

cluster Relation-like natural-valued -> NAT -valued for set ;

coherence
for b₁ being Relation st b₁ is natural-valued holds
b₁ is NAT -valued

proof end;

end;

registration

let f be complex-valued Function;
let k be object ;

reduce (0 (#) f) . k to 0 ;

reducibility
(0 (#) f) . k = 0

proof end;

end;

registration

let f be complex-valued Function;

reduce 1 (#) f to f;

reducibility
1 (#) f = f by RFUNCT_1:21;

reduce (- 1) (#) (- f) to f;

reducibility
(- 1) (#) (- f) = f

proof end;

cluster 0 * f -> empty-yielding ;

coherence
0 (#) f is empty-yielding

proof end;

cluster f - f -> empty-yielding ;

coherence
f - f is empty-yielding

proof end;

end;

registration

let D be set ;

cluster Relation-like empty-yielding omega -defined D -valued Function-like V32() FinSequence-like FinSubsequence-like for set ;

existence
ex b₁ being D -valued FinSequence st b₁ is empty-yielding

proof end;

end;

registration

cluster Relation-like empty-yielding Function-like FinSequence-like -> NAT -valued for set ;

coherence
for b₁ being FinSequence st b₁ is empty-yielding holds
b₁ is NAT -valued

proof end;

cluster Relation-like empty-yielding omega -defined {{}} -valued Function-like constant non empty V32() FinSequence-like FinSubsequence-like V87() V88() constanT for set ;

existence
not for b₁ being empty-yielding FinSequence holds b₁ is empty

proof end;

end;

registration

let n be Nat;

cluster Relation-like empty-yielding omega -defined NAT -valued Function-like V32() n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued for set ;

existence
ex b₁ being empty-yielding NAT -valued FinSequence st b₁ is n -element

proof end;

cluster min (n,0) -> zero ;

coherence
min (n,0) is zero by XXREAL_0:def 9;

reduce max (n,0) to n;

reducibility
max (n,0) = n by XXREAL_0:def 10;

end;

registration

let a be non zero Nat;

reduce min (a,1) to 1;

reducibility
min (a,1) = 1 by NAT_1:14, XXREAL_0:def 9;

reduce max (a,1) to a;

reducibility
max (a,1) = a by NAT_1:14, XXREAL_0:def 10;

end;

registration

let a be non trivial Nat;

reduce min (a,2) to 2;

reducibility
min (a,2) = 2

proof end;

reduce max (a,2) to a;

reducibility
max (a,2) = a

proof end;

end;

registration

let a be positive Real;
let b be positive Nat;

cluster b |-> a -> positive ;

coherence
b |-> a is positive ;

end;

registration

cluster Relation-like empty-yielding -> Function-like for set ;

coherence
for b₁ being Relation st b₁ is empty-yielding holds
b₁ is Function-like

proof end;

cluster Relation-like empty-yielding Function-like -> natural-valued for set ;

coherence
for b₁ being Function st b₁ is empty-yielding holds
b₁ is natural-valued

proof end;

cluster Relation-like empty-yielding Function-like real-valued -> real-valued nonpositive-yielding for set ;

coherence
for b₁ being real-valued Function st b₁ is empty-yielding holds
b₁ is nonpositive-yielding

proof end;

cluster Relation-like empty-yielding Function-like real-valued -> real-valued nonnegative-yielding for set ;

coherence
for b₁ being real-valued Function st b₁ is empty-yielding holds
b₁ is nonnegative-yielding

proof end;

cluster Relation-like empty-yielding Function-like non empty real-valued -> non empty real-valued non positive-yielding for set ;

coherence
for b₁ being non empty real-valued Function st b₁ is empty-yielding holds
not b₁ is positive-yielding

proof end;

cluster Relation-like empty-yielding Function-like non empty real-valued -> non empty real-valued non negative-yielding for set ;

coherence
for b₁ being non empty real-valued Function st b₁ is empty-yielding holds
not b₁ is negative-yielding

proof end;

cluster Relation-like Function-like non empty real-valued positive-yielding -> non empty real-valued non nonpositive-yielding for set ;

coherence
for b₁ being non empty real-valued Function st b₁ is positive-yielding holds
not b₁ is nonpositive-yielding

proof end;

cluster Relation-like Function-like non empty real-valued negative-yielding -> non empty real-valued non nonnegative-yielding for set ;

coherence
for b₁ being non empty real-valued Function st b₁ is negative-yielding holds
not b₁ is nonnegative-yielding

proof end;

end;

registration

let f be empty-yielding Function;
let c be Complex;

cluster c * f -> empty-yielding ;

coherence
c (#) f is empty-yielding

proof end;

end;

registration

let f be empty-yielding Function;
let g be complex-valued Function;

cluster f (#) g -> empty-yielding ;

coherence
f (#) g is empty-yielding

proof end;

end;

:: length of FinSequences

registration

let f be complex-valued FinSequence;
let x be Complex;

cluster x + f -> len f -element ;

coherence
f + x is len f -element

proof end;

cluster f - x -> len f -element ;

coherence
f - x is len f -element

proof end;

end;

registration

let f be complex-valued FinSequence;

cluster |.f.| -> len f -element ;

coherence
abs f is len f -element

proof end;

cluster - f -> len f -element ;

coherence
- f is len f -element

proof end;

cluster f " -> len f -element ;

coherence
f " is len f -element

proof end;

end;

registration

let n, m be Nat;
let f be n -element complex-valued FinSequence;
let g be m -element complex-valued FinSequence;

cluster f + g -> min (n,m) -element ;

coherence
f + g is min (n,m) -element

proof end;

cluster f (#) g -> min (n,m) -element ;

coherence
f (#) g is min (n,m) -element

proof end;

cluster f - g -> min (n,m) -element ;

coherence
f - g is min (n,m) -element

proof end;

cluster f /" g -> min (n,m) -element ;

coherence
f /" g is min (n,m) -element

proof end;

end;

registration

let n, m be Nat;
let f be n -element complex-valued FinSequence;
let g be empty-yielding n + m -element complex-valued FinSequence;

reduce f + g to f;

reducibility
f + g = f

proof end;

end;

registration

let n be Nat;
let f be n -element complex-valued FinSequence;
let g be empty-yielding n -element complex-valued FinSequence;

reduce f + g to f;

reducibility
f + g = f

proof end;

end;

registration

let X be non empty set ;

cluster Relation-like empty-yielding X -defined NAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued nonpositive-yielding nonnegative-yielding for set ;

existence
ex b₁ being empty-yielding X -defined Function st b₁ is total

proof end;

end;

registration

let X be non empty set ;
let f be X -defined total complex-valued Function;
let g be empty-yielding X -defined total Function;

reduce f + g to f;

reducibility
f + g = f

proof end;

end;

registration

let f be Relation;

cluster Relation-like dom f -defined for set ;

existence
ex b₁ being Relation st b₁ is dom f -defined by RELAT_1:def 18;

cluster f null f -> dom f -defined ;

coherence
f null f is dom f -defined by RELAT_1:def 18;

cluster Relation-like dom f -defined total for set ;

existence
ex b₁ being dom f -defined Relation st b₁ is total

proof end;

end;

registration

let f be complex-valued Function;

cluster Relation-like empty-yielding dom f -defined NAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued nonpositive-yielding nonnegative-yielding for set ;

existence
ex b₁ being empty-yielding dom f -defined Function st b₁ is total

proof end;

cluster - f -> dom f -defined ;

coherence
- f is dom f -defined

proof end;

cluster - f -> total ;

coherence
- f is total

proof end;

cluster f " -> dom f -defined ;

coherence
f " is dom f -defined

proof end;

cluster f " -> total ;

coherence
f " is total

proof end;

cluster |.f.| -> dom f -defined ;

coherence
abs f is dom f -defined

proof end;

cluster |.f.| -> total ;

coherence
abs f is total

proof end;

end;

registration

let f be complex-valued Function;
let c be Complex;

cluster c + f -> dom f -defined ;

coherence
c + f is dom f -defined

proof end;

cluster c + f -> total ;

coherence
c + f is total

proof end;

cluster f - c -> dom f -defined ;

coherence
f - c is dom f -defined

proof end;

cluster f - c -> total ;

coherence
f - c is total

proof end;

cluster c * f -> dom f -defined ;

coherence
c (#) f is dom f -defined

proof end;

cluster c * f -> total ;

coherence
c (#) f is total

proof end;

end;

registration

let f be FinSequence;

cluster Relation-like Function-like len f -element FinSequence-like -> dom f -defined for set ;

coherence
for b₁ being FinSequence st b₁ is len f -element holds
b₁ is dom f -defined

proof end;

end;

registration

let n be Nat;

cluster Relation-like Function-like n -element FinSequence-like -> Seg n -defined for set ;

coherence
for b₁ being FinSequence st b₁ is n -element holds
b₁ is Seg n -defined

proof end;

cluster Relation-like Seg n -defined Function-like FinSequence-like total -> n -element for set ;

coherence
for b₁ being FinSequence st b₁ is total & b₁ is Seg n -defined holds
b₁ is n -element

proof end;

end;

theorem EMP: :: FINSEQ_9:1

for f being complex-valued FinSequence holds 0 (#) f = (len f) |-> 0

proof end;

registration

let f be complex-valued FinSequence;

reduce f + ((len f) |-> 0) to f;

reducibility
f + ((len f) |-> 0) = f

proof end;

end;

registration

let n be Nat;
let D be non empty set ;
let X be non empty Subset of D;

cluster Relation-like omega -defined X -valued Function-like V32() n -element FinSequence-like FinSubsequence-like for set ;

existence
ex b₁ being X -valued FinSequence st b₁ is n -element

proof end;

cluster Relation-like omega -defined X -valued Function-like V32() n -element FinSequence-like FinSubsequence-like for FinSequence of X;

existence
ex b₁ being FinSequence of X st b₁ is n -element

proof end;

end;

registration

let f be real-valued Function;

cluster f + (abs f) -> nonnegative-yielding ;

coherence
f + (abs f) is nonnegative-yielding

proof end;

cluster (abs f) - f -> nonnegative-yielding ;

coherence
(abs f) - f is nonnegative-yielding

proof end;

end;

registration

let f be real-valued nonnegative-yielding Function;
let x be object ;

cluster f . x -> non negative ;

coherence
not f . x is negative

proof end;

end;

registration

let f be real-valued nonpositive-yielding Function;
let x be object ;

cluster f . x -> non positive ;

coherence
not f . x is positive

proof end;

end;

registration

let f be real-valued nonnegative-yielding Function;
let r be non negative Real;

cluster r * f -> nonnegative-yielding ;

coherence
r (#) f is nonnegative-yielding

proof end;

cluster (- r) * f -> nonpositive-yielding ;

coherence
(- r) (#) f is nonpositive-yielding

proof end;

end;

registration

let f be real-valued nonnegative-yielding Function;

cluster - f -> nonpositive-yielding ;

coherence
- f is nonpositive-yielding

proof end;

end;

registration

let f be real-valued nonpositive-yielding Function;
let r be non negative Real;

cluster r * f -> nonpositive-yielding ;

coherence
r (#) f is nonpositive-yielding

proof end;

cluster (- r) * f -> nonnegative-yielding ;

coherence
(- r) (#) f is nonnegative-yielding

proof end;

end;

registration

let f be real-valued nonpositive-yielding Function;

cluster - f -> nonnegative-yielding ;

coherence
- f is nonnegative-yielding

proof end;

end;

registration

cluster Relation-like INT -valued Function-like nonnegative-yielding -> INT -valued natural-valued for set ;

coherence
for b₁ being INT -valued Function st b₁ is nonnegative-yielding holds
b₁ is natural-valued

proof end;

end;

registration

let f be INT -valued Function;

cluster (1 / 2) * (f + (abs f)) -> natural-valued ;

coherence
(1 / 2) (#) (f + (abs f)) is natural-valued

proof end;

cluster (1 / 2) * ((abs f) - f) -> natural-valued ;

coherence
(1 / 2) (#) ((abs f) - f) is natural-valued

proof end;

end;

:: Values are members of the range

theorem NV: :: FINSEQ_9:2

for f being Relation holds
( rng f is natural-membered iff f is natural-valued )

proof end;

theorem :: FINSEQ_9:3

for f being Relation holds
( f is NAT -valued iff rng f is natural-membered )

proof end;

theorem :: FINSEQ_9:4

for f being Relation holds
( rng f is integer-membered iff f is INT -valued )

proof end;

theorem :: FINSEQ_9:5

for f being Relation holds
( rng f is rational-membered iff f is RAT -valued )

proof end;

theorem RV: :: FINSEQ_9:6

for f being Relation holds
( rng f is real-membered iff f is real-valued )

proof end;

theorem :: FINSEQ_9:7

for f being Relation holds
( f is REAL -valued iff rng f is real-membered )

proof end;

theorem CV: :: FINSEQ_9:8

for f being Relation holds
( rng f is complex-membered iff f is complex-valued )

proof end;

theorem :: FINSEQ_9:9

for f being Relation holds
( f is COMPLEX -valued iff rng f is complex-membered )

proof end;

:: similarly: Relations are defined over members of their domain

theorem :: FINSEQ_9:10

for f being Relation holds
( dom f is natural-membered iff f is NAT -defined )

proof end;

registration

let f be INT -defined Relation;

cluster dom f -> integer-membered ;

coherence
dom f is integer-membered ;

end;

theorem :: FINSEQ_9:11

for f being Relation holds
( dom f is integer-membered iff f is INT -defined )

proof end;

registration

let f be RAT -defined Relation;

cluster dom f -> rational-membered ;

coherence
dom f is rational-membered ;

end;

theorem :: FINSEQ_9:12

for f being Relation holds
( dom f is rational-membered iff f is RAT -defined )

proof end;

registration

let f be REAL -defined Relation;

cluster dom f -> real-membered ;

coherence
dom f is real-membered ;

end;

theorem :: FINSEQ_9:13

for f being Relation holds
( dom f is real-membered iff f is REAL -defined )

proof end;

registration

let f be COMPLEX -defined Relation;

cluster dom f -> complex-membered ;

coherence
dom f is complex-membered ;

end;

theorem :: FINSEQ_9:14

for f being Relation holds
( dom f is complex-membered iff f is COMPLEX -defined )

proof end;

theorem N2103: :: FINSEQ_9:15

for D being set
for f being Function holds
( f is D -valued iff f is Function of (dom f),D )

proof end;

theorem T2103: :: FINSEQ_9:16

for C being set
for f being b₁ -defined total Function holds f is Function of C,(rng f)

proof end;

theorem :: FINSEQ_9:17

for C, D being set
for f being b₁ -defined total Function holds
( f is Function of C,D iff f is D -valued )

proof end;

theorem :: FINSEQ_9:18

for f being real-valued Function holds f is Function of (dom f),REAL

proof end;

theorem :: FINSEQ_9:19

for f being complex-valued FinSequence holds
( f - f = 0 (#) f & f - f = (len f) |-> 0 )

proof end;

theorem Lmkdf: :: FINSEQ_9:20

for a being Complex
for f being FinSequence
for k being Nat st k in dom f holds
((len f) |-> a) . k = a

proof end;

registration

let a be Real;
let k be non zero Nat;
let l be Nat;
let f be k + l -element FinSequence;

reduce ((len f) |-> a) . k to a;

reducibility
((len f) |-> a) . k = a

proof end;

end;

definition

let f be complex-valued Function;

func delneg f -> complex-valued Function equals :: FINSEQ_9:def 1
(1 / 2) (#) (f + (abs f));

correctness
coherence
(1 / 2) (#) (f + (abs f)) is complex-valued Function;
;

func delpos f -> complex-valued Function equals :: FINSEQ_9:def 2
(1 / 2) (#) ((abs f) - f);

correctness
coherence
(1 / 2) (#) ((abs f) - f) is complex-valued Function;
;

func delall f -> complex-valued Function equals :: FINSEQ_9:def 3
0 (#) f;

correctness
coherence
0 (#) f is complex-valued Function;
;

end;

:: deftheorem defines delneg FINSEQ_9:def 1 :
for f being complex-valued Function holds delneg f = (1 / 2) (#) (f + (abs f));

:: deftheorem defines delpos FINSEQ_9:def 2 :
for f being complex-valued Function holds delpos f = (1 / 2) (#) ((abs f) - f);

:: deftheorem defines delall FINSEQ_9:def 3 :
for f being complex-valued Function holds delall f = 0 (#) f;

theorem DMN: :: FINSEQ_9:21

for f being complex-valued Function holds
( dom f = dom (delpos f) & dom f = dom (delneg f) & dom f = dom (delall f) )

proof end;

theorem VAL: :: FINSEQ_9:22

for f being complex-valued Function
for x being object holds f . x = ((delneg f) . x) - ((delpos f) . x)

proof end;

theorem DNP: :: FINSEQ_9:23

for f being complex-valued Function holds f = (delneg f) - (delpos f)

proof end;

theorem VOR: :: FINSEQ_9:24

for f being real-valued Function
for x being object holds
( f . x = (delneg f) . x or f . x = - ((delpos f) . x) )

proof end;

theorem ZOR: :: FINSEQ_9:25

for f being real-valued Function
for x being object holds
( (delneg f) . x = 0 or (delpos f) . x = 0 )

proof end;

registration

let f be real-valued Function;

cluster (delneg f) (#) (delpos f) -> empty-yielding ;

coherence
(delneg f) (#) (delpos f) is empty-yielding

proof end;

end;

theorem :: FINSEQ_9:26

for f being real-valued Function holds delall f = (delneg f) (#) (delpos f)

proof end;

registration

let f be complex-valued Function;
let f1 be empty-yielding dom f -defined total Function;

reduce f + f1 to f;

reducibility
f + f1 = f

proof end;

reduce f - f1 to f;

reducibility
f - f1 = f

proof end;

end;

registration

let f be complex-valued Function;
let f1 be dom f -defined total complex-valued Function;
let f2 be empty-yielding dom f -defined total Function;

reduce f1 + f2 to f1;

reducibility
f1 + f2 = f1

proof end;

reduce f1 - f2 to f1;

reducibility
f1 - f2 = f1

proof end;

end;

registration

let f be complex-valued Function;

cluster f - f -> dom f -defined ;

coherence
f - f is dom f -defined

proof end;

cluster f - f -> total ;

coherence
f - f is total

proof end;

end;

theorem :: FINSEQ_9:27

for f being complex-valued Function holds abs f = (delneg f) + (delpos f)

proof end;

registration

let f be empty FinSequence;

cluster Product f -> natural ;

coherence
Product f is natural by RVSUM_1:94;

cluster Product f -> non zero ;

coherence
not Product f is zero by RVSUM_1:94;

end;

registration

let f be real-valued positive-yielding FinSequence;

cluster Product f -> positive ;

coherence
Product f is positive

proof end;

end;

registration

let f be complex-valued FinSequence;

cluster delneg f -> len f -element complex-valued ;

coherence
delneg f is len f -element

proof end;

cluster delpos f -> len f -element complex-valued ;

coherence
delpos f is len f -element

proof end;

end;

theorem DNF: :: FINSEQ_9:28

for f being complex-valued Function holds delneg f = delpos (- f)

proof end;

registration

let f be real-valued nonnegative-yielding Function;

reduce abs f to f;

reducibility
abs f = f

proof end;

reduce delneg f to f;

reducibility
delneg f = f

proof end;

identify delpos f with delall f;

correctness
compatibility
delpos f = delall f;

proof end;

identify delall f with delpos f;

correctness
compatibility
delall f = delpos f;
;

end;

registration

let f be real-valued nonpositive-yielding Function;

reduce - (delpos f) to f;

reducibility
- (delpos f) = f

proof end;

cluster delneg f -> empty-yielding complex-valued ;

coherence
delneg f is empty-yielding

proof end;

identify delneg f with delall f;

correctness
compatibility
delneg f = delall f;

proof end;

identify delall f with delneg f;

correctness
compatibility
delall f = delneg f;
;

end;

theorem :: FINSEQ_9:29

for f being FinSequence of INT ex f1, f2 being FinSequence of NAT st f = f1 - f2

proof end;

registration

let a be Integer;
let n be Nat;

cluster n |-> a -> INT -valued ;

coherence
n |-> a is INT -valued ;

end;

registration

let f be empty-yielding non empty FinSequence;

cluster Product f -> zero ;

coherence
Product f is zero

proof end;

end;

theorem :: FINSEQ_9:30

for f1, f2 being FinSequence of REAL st len f1 = len f2 & ( for k being Element of NAT st k in dom f1 holds
( f1 . k >= f2 . k & f2 . k > 0 ) ) holds
Product f1 >= Product f2

proof end;

theorem :: FINSEQ_9:31

for a being Real
for f being FinSequence of REAL st ( for k being Element of NAT st k in dom f holds
( 0 < f . k & f . k <= a ) ) holds
Product f <= Product ((len f) |-> a)

proof end;

theorem :: FINSEQ_9:32

for a being non negative Real
for f being FinSequence of REAL st ( for k being Nat st k in dom f holds
f . k >= a ) holds
Product f >= a |^ (len f)

proof end;

theorem N454: :: FINSEQ_9:33

for f1, f2 being nonnegative-yielding FinSequence of REAL st len f1 = len f2 & ( for k being Element of NAT st k in dom f2 holds
f1 . k >= f2 . k ) holds
Product f1 >= Product f2

proof end;

theorem :: FINSEQ_9:34

for f1, f2 being FinSequence of REAL st len f1 = len f2 & ( for k being Element of NAT st k in dom f2 holds
( f1 . k >= f2 . k & f2 . k >= 0 ) ) holds
Product f1 >= Product f2

proof end;

theorem :: FINSEQ_9:35

for a being positive Real
for f being nonnegative-yielding FinSequence of REAL st ( for k being Element of NAT st k in dom f holds
f . k <= a ) holds
Product f <= a |^ (len f)

proof end;

:: Basic operations on short finsequences

registration

let a be Complex;

reduce (- <*(- a)*>) . 1 to a;

reducibility
(- <*(- a)*>) . 1 = a

proof end;

reduce (<*(a ")*> ") . 1 to a;

reducibility
(<*(a ")*> ") . 1 = a

proof end;

end;

theorem APB: :: FINSEQ_9:36

for a, b being Complex holds <*a*> + <*b*> = <*(a + b)*>

proof end;

theorem :: FINSEQ_9:37

for a, b being Complex holds <*a*> - <*b*> = <*(a - b)*>

proof end;

theorem AMB: :: FINSEQ_9:38

for a, b being Complex holds <*a*> (#) <*b*> = <*(a * b)*>

proof end;

theorem :: FINSEQ_9:39

for a, b being Complex holds <*a*> /" <*b*> = <*(a * (b "))*>

proof end;

registration

let n be Nat;
let f be n -element FinSequence;
let a be Complex;

reduce (f ^ <*a*>) . (n + 1) to a;

reducibility
(f ^ <*a*>) . (n + 1) = a

proof end;

reduce (f ^ <*a*>) | n to f;

reducibility
(f ^ <*a*>) | n = f

proof end;

end;

registration

let a, b, c, d be Complex;

cluster <*a,b,c,d*> -> complex-valued ;

coherence
<*a,b,c,d*> is complex-valued

proof end;

end;

registration

let a, b be Complex;

reduce (- <*(- a),b*>) . 1 to a;

reducibility
(- <*(- a),b*>) . 1 = a

proof end;

reduce (- <*a,(- b)*>) . 2 to b;

reducibility
(- <*a,(- b)*>) . 2 = b

proof end;

reduce (<*(a "),b*> ") . 1 to a;

reducibility
(<*(a "),b*> ") . 1 = a

proof end;

reduce (<*a,(b ")*> ") . 2 to b;

reducibility
(<*a,(b ")*> ") . 2 = b

proof end;

end;

registration

let a, b, c be Complex;

reduce <*a,b,c*> . 1 to a;

reducibility
<*a,b,c*> . 1 = a by FINSEQ_1:45;

reduce <*a,b,c*> . 2 to b;

reducibility
<*a,b,c*> . 2 = b by FINSEQ_1:45;

reduce (- <*(- a),b,c*>) . 1 to a;

reducibility
(- <*(- a),b,c*>) . 1 = a

proof end;

reduce (- <*a,(- b),c*>) . 2 to b;

reducibility
(- <*a,(- b),c*>) . 2 = b

proof end;

reduce (- <*a,b,(- c)*>) . 3 to c;

reducibility
(- <*a,b,(- c)*>) . 3 = c

proof end;

reduce (<*(a "),b,c*> ") . 1 to a;

reducibility
(<*(a "),b,c*> ") . 1 = a

proof end;

reduce (<*a,(b "),c*> ") . 2 to b;

reducibility
(<*a,(b "),c*> ") . 2 = b

proof end;

reduce (<*a,b,(c ")*> ") . 3 to c;

reducibility
(<*a,b,(c ")*> ") . 3 = c

proof end;

end;

theorem FPA: :: FINSEQ_9:40

for a, b being Complex
for n being Nat
for f, g being b₃ -element complex-valued FinSequence holds (f ^ <*a*>) + (g ^ <*b*>) = (f + g) ^ <*(a + b)*>

proof end;

theorem AP2: :: FINSEQ_9:41

for a, b, x, y being Complex holds <*a,b*> + <*x,y*> = <*(a + x),(b + y)*>

proof end;

theorem AP3: :: FINSEQ_9:42

for a, b, c, x, y, z being Complex holds <*a,b,c*> + <*x,y,z*> = <*(a + x),(b + y),(c + z)*>

proof end;

theorem :: FINSEQ_9:43

for a, b, c, d, x, y, z, v being Complex holds <*a,b,c,d*> + <*x,y,z,v*> = <*(a + x),(b + y),(c + z),(d + v)*>

proof end;

theorem FMA: :: FINSEQ_9:44

for a, b being Complex
for n being Nat
for f, g being b₃ -element complex-valued FinSequence holds (f ^ <*a*>) (#) (g ^ <*b*>) = (f (#) g) ^ <*(a * b)*>

proof end;

theorem AM2: :: FINSEQ_9:45

for a, b, x, y being Complex holds <*a,b*> (#) <*x,y*> = <*(a * x),(b * y)*>

proof end;

theorem AM3: :: FINSEQ_9:46

for a, b, c, x, y, z being Complex holds <*a,b,c*> (#) <*x,y,z*> = <*(a * x),(b * y),(c * z)*>

proof end;

theorem :: FINSEQ_9:47

for a, b, c, d, x, y, z, v being Complex holds <*a,b,c,d*> (#) <*x,y,z,v*> = <*(a * x),(b * y),(c * z),(d * v)*>

proof end;

theorem :: FINSEQ_9:48

for a being Complex
for n being non zero Nat
for f being b₂ -element complex-valued FinSequence holds <*a*> + f = <*(a + (f . 1))*>

proof end;

theorem :: FINSEQ_9:49

for a, b being Complex
for n being non trivial Nat
for f being b₃ -element complex-valued FinSequence holds <*a,b*> + f = <*(a + (f . 1)),(b + (f . 2))*>

proof end;

theorem :: FINSEQ_9:50

for a being Complex
for n being non zero Nat
for f being b₂ -element complex-valued FinSequence holds <*a*> (#) f = <*(a * (f . 1))*>

proof end;

theorem :: FINSEQ_9:51

for a, b being Complex
for n being non trivial Nat
for f being b₃ -element complex-valued FinSequence holds <*a,b*> (#) f = <*(a * (f . 1)),(b * (f . 2))*>

proof end;