:: 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 b1 being Relation st b1 is empty holds
b1 is positive-yielding
proof end;
cluster Relation-like empty -> negative-yielding for set ;
coherence
for b1 being Relation st b1 is empty holds
b1 is negative-yielding
proof end;
end;

registration
cluster Relation-like natural-valued -> NAT -valued for set ;
coherence
for b1 being Relation st b1 is natural-valued holds
b1 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 b1 being D -valued FinSequence st b1 is empty-yielding
proof end;
end;

registration
cluster Relation-like empty-yielding Function-like FinSequence-like -> NAT -valued for set ;
coherence
for b1 being FinSequence st b1 is empty-yielding holds
b1 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 b1 being empty-yielding FinSequence holds b1 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 b1 being empty-yielding NAT -valued FinSequence st b1 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 b1 being Relation st b1 is empty-yielding holds
b1 is Function-like
proof end;
cluster Relation-like empty-yielding Function-like -> natural-valued for set ;
coherence
for b1 being Function st b1 is empty-yielding holds
b1 is natural-valued
proof end;
cluster Relation-like empty-yielding Function-like real-valued -> real-valued nonpositive-yielding for set ;
coherence
for b1 being real-valued Function st b1 is empty-yielding holds
b1 is nonpositive-yielding
proof end;
cluster Relation-like empty-yielding Function-like real-valued -> real-valued nonnegative-yielding for set ;
coherence
for b1 being real-valued Function st b1 is empty-yielding holds
b1 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 b1 being non empty real-valued Function st b1 is empty-yielding holds
not b1 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 b1 being non empty real-valued Function st b1 is empty-yielding holds
not b1 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 b1 being non empty real-valued Function st b1 is positive-yielding holds
not b1 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 b1 being non empty real-valued Function st b1 is negative-yielding holds
not b1 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 b1 being empty-yielding X -defined Function st b1 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 b1 being Relation st b1 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 b1 being dom f -defined Relation st b1 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 b1 being empty-yielding dom f -defined Function st b1 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 b1 being FinSequence st b1 is len f -element holds
b1 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 b1 being FinSequence st b1 is n -element holds
b1 is Seg n -defined
proof end;
cluster Relation-like Seg n -defined Function-like FinSequence-like total -> n -element for set ;
coherence
for b1 being FinSequence st b1 is total & b1 is Seg n -defined holds
b1 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 b1 being X -valued FinSequence st b1 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 b1 being FinSequence of X st b1 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 b1 being INT -valued Function st b1 is nonnegative-yielding holds
b1 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 b1 -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 b1 -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 b3 -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 b3 -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 b2 -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 b3 -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 b2 -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 b3 -element complex-valued FinSequence holds <*a,b*> (#) f = <*(a * (f . 1)),(b * (f . 2))*>
proof end;