:: by Rafa{\l} Ziobro

::

:: Received September 29, 2018

:: Copyright (c) 2018-2021 Association of Mizar Users

:: empty Relations are full of adjectives

registration

coherence

for b_{1} being Relation st b_{1} is empty holds

b_{1} is positive-yielding

for b_{1} being Relation st b_{1} is empty holds

b_{1} is negative-yielding

end;
for b

b

proof end;

coherence for b

b

proof end;

registration
end;

registration
end;

registration

let f be complex-valued Function;

reducibility

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

reducibility

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

0 (#) f is empty-yielding

f - f is empty-yielding

end;
reducibility

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

reducibility

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

proof end;

coherence 0 (#) f is empty-yielding

proof end;

coherence f - f is empty-yielding

proof end;

registration

let D be set ;

ex b_{1} being D -valued FinSequence st b_{1} is empty-yielding

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

existence ex b

proof end;

registration

coherence

for b_{1} being FinSequence st b_{1} is empty-yielding holds

b_{1} is NAT -valued

not for b_{1} being empty-yielding FinSequence holds b_{1} is empty

end;
for b

b

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

proof end;

registration

let n be Nat;

ex b_{1} being empty-yielding NAT -valued FinSequence st b_{1} is n -element

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

reducibility

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

end;
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

proof end;

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

reducibility

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

registration

let a be non zero Nat;

reducibility

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

reducibility

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

end;
reducibility

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

reducibility

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

registration

let a be non trivial Nat;

reducibility

min (a,2) = 2

max (a,2) = a

end;
reducibility

min (a,2) = 2

proof end;

reducibility max (a,2) = a

proof end;

registration

coherence

for b_{1} being Relation st b_{1} is empty-yielding holds

b_{1} is Function-like

for b_{1} being Function st b_{1} is empty-yielding holds

b_{1} is natural-valued

for b_{1} being real-valued Function st b_{1} is empty-yielding holds

b_{1} is nonpositive-yielding

for b_{1} being real-valued Function st b_{1} is empty-yielding holds

b_{1} is nonnegative-yielding

for b_{1} being non empty real-valued Function st b_{1} is empty-yielding holds

not b_{1} is positive-yielding

for b_{1} being non empty real-valued Function st b_{1} is empty-yielding holds

not b_{1} is negative-yielding

for b_{1} being non empty real-valued Function st b_{1} is positive-yielding holds

not b_{1} is nonpositive-yielding

for b_{1} being non empty real-valued Function st b_{1} is negative-yielding holds

not b_{1} is nonnegative-yielding

end;
for b

b

proof end;

coherence for b

b

proof end;

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

coherence for b

b

proof end;

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

coherence for b

b

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

not b

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

not b

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

not b

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

not b

proof end;

registration
end;

registration

let f be empty-yielding Function;

let g be complex-valued Function;

coherence

f (#) g is empty-yielding

end;
let g be complex-valued Function;

coherence

f (#) g is empty-yielding

proof end;

:: length of FinSequences

registration

let f be complex-valued FinSequence;

let x be Complex;

coherence

f + x is len f -element

f - x is len f -element

end;
let x be Complex;

coherence

f + x is len f -element

proof end;

coherence f - x is len f -element

proof end;

registration

let f be complex-valued FinSequence;

coherence

abs f is len f -element

- f is len f -element

f " is len f -element

end;
coherence

abs f is len f -element

proof end;

coherence - f is len f -element

proof end;

coherence f " is len f -element

proof end;

registration

let n, m be Nat;

let f be n -element complex-valued FinSequence;

let g be m -element complex-valued FinSequence;

coherence

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

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

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

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

end;
let f be n -element complex-valued FinSequence;

let g be m -element complex-valued FinSequence;

coherence

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

proof end;

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

proof end;

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

proof end;

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

proof 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;

reducibility

f + g = f

end;
let f be n -element complex-valued FinSequence;

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

reducibility

f + g = f

proof end;

registration

let n be Nat;

let f be n -element complex-valued FinSequence;

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

reducibility

f + g = f

end;
let f be n -element complex-valued FinSequence;

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

reducibility

f + g = f

proof end;

registration

let X be non empty set ;

ex b_{1} being empty-yielding X -defined Function st b_{1} is total

end;
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

proof 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;

reducibility

f + g = f

end;
let f be X -defined total complex-valued Function;

let g be empty-yielding X -defined total Function;

reducibility

f + g = f

proof end;

registration

let f be Relation;

existence

ex b_{1} being Relation st b_{1} is dom f -defined
by RELAT_1:def 18;

coherence

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

existence

ex b_{1} being dom f -defined Relation st b_{1} is total

end;
existence

ex b

coherence

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

existence

ex b

proof end;

registration

let f be complex-valued Function;

ex b_{1} being empty-yielding dom f -defined Function st b_{1} is total

- f is dom f -defined

- f is total

f " is dom f -defined

f " is total

abs f is dom f -defined

abs f is total

end;
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

proof end;

coherence - f is dom f -defined

proof end;

coherence - f is total

proof end;

coherence f " is dom f -defined

proof end;

coherence f " is total

proof end;

coherence abs f is dom f -defined

proof end;

coherence abs f is total

proof end;

registration

let f be complex-valued Function;

let c be Complex;

coherence

c + f is dom f -defined

c + f is total

f - c is dom f -defined

f - c is total

c (#) f is dom f -defined

c (#) f is total

end;
let c be Complex;

coherence

c + f is dom f -defined

proof end;

coherence c + f is total

proof end;

coherence f - c is dom f -defined

proof end;

coherence f - c is total

proof end;

coherence c (#) f is dom f -defined

proof end;

coherence c (#) f is total

proof end;

registration

let f be FinSequence;

coherence

for b_{1} being FinSequence st b_{1} is len f -element holds

b_{1} is dom f -defined

end;
coherence

for b

b

proof end;

registration

let n be Nat;

coherence

for b_{1} being FinSequence st b_{1} is n -element holds

b_{1} is Seg n -defined

for b_{1} being FinSequence st b_{1} is total & b_{1} is Seg n -defined holds

b_{1} is n -element

end;
coherence

for b

b

proof end;

coherence for b

b

proof end;

registration
end;

registration

let n be Nat;

let D be non empty set ;

let X be non empty Subset of D;

ex b_{1} being X -valued FinSequence st b_{1} is n -element

ex b_{1} being FinSequence of X st b_{1} is n -element

end;
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

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

proof end;

registration

let f be real-valued Function;

coherence

f + (abs f) is nonnegative-yielding

(abs f) - f is nonnegative-yielding

end;
coherence

f + (abs f) is nonnegative-yielding

proof end;

coherence (abs f) - f is nonnegative-yielding

proof end;

registration

let f be real-valued nonnegative-yielding Function;

let x be object ;

coherence

not f . x is negative

end;
let x be object ;

coherence

not f . x is negative

proof end;

registration

let f be real-valued nonpositive-yielding Function;

let x be object ;

coherence

not f . x is positive

end;
let x be object ;

coherence

not f . x is positive

proof end;

registration

let f be real-valued nonnegative-yielding Function;

let r be non negative Real;

coherence

r (#) f is nonnegative-yielding

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

end;
let r be non negative Real;

coherence

r (#) f is nonnegative-yielding

proof end;

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

proof end;

registration

let f be real-valued nonnegative-yielding Function;

coherence

- f is nonpositive-yielding

end;
coherence

- f is nonpositive-yielding

proof end;

registration

let f be real-valued nonpositive-yielding Function;

let r be non negative Real;

coherence

r (#) f is nonpositive-yielding

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

end;
let r be non negative Real;

coherence

r (#) f is nonpositive-yielding

proof end;

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

proof end;

registration

let f be real-valued nonpositive-yielding Function;

coherence

- f is nonnegative-yielding

end;
coherence

- f is nonnegative-yielding

proof end;

registration

for b_{1} being INT -valued Function st b_{1} is nonnegative-yielding holds

b_{1} is natural-valued
end;

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

coherence for b

b

proof end;

registration

let f be INT -valued Function;

coherence

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

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

end;
coherence

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

proof end;

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

proof end;

:: Values are members of the range

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

theorem :: FINSEQ_9:17

for C, D being set

for f being b_{1} -defined total Function holds

( f is Function of C,D iff f is D -valued )

for f being b

( f is Function of C,D iff f is D -valued )

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

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;

reducibility

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

end;
let k be non zero Nat;

let l be Nat;

let f be k + l -element FinSequence;

reducibility

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

proof end;

definition

let f be complex-valued Function;

correctness

coherence

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

;

correctness

coherence

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

;

correctness

coherence

0 (#) f is complex-valued Function;

;

end;
correctness

coherence

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

;

correctness

coherence

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

;

correctness

coherence

0 (#) f is complex-valued Function;

;

:: deftheorem defines delneg FINSEQ_9:def 1 :

for f being complex-valued Function holds delneg f = (1 / 2) (#) (f + (abs f));

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);

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;

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) )

( 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)

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

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) )

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 )

for x being object holds

( (delneg f) . x = 0 or (delpos f) . x = 0 )

proof end;

registration
end;

registration

let f be complex-valued Function;

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

reducibility

f + f1 = f

f - f1 = f

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

reducibility

f + f1 = f

proof end;

reducibility f - f1 = f

proof 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;

reducibility

f1 + f2 = f1

f1 - f2 = f1

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

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

reducibility

f1 + f2 = f1

proof end;

reducibility f1 - f2 = f1

proof end;

registration

let f be complex-valued Function;

coherence

f - f is dom f -defined

f - f is total

end;
coherence

f - f is dom f -defined

proof end;

coherence f - f is total

proof end;

registration

let f be empty FinSequence;

coherence

Product f is natural by RVSUM_1:94;

coherence

not Product f is zero by RVSUM_1:94;

end;
coherence

Product f is natural by RVSUM_1:94;

coherence

not Product f is zero by RVSUM_1:94;

registration
end;

registration

let f be complex-valued FinSequence;

coherence

delneg f is len f -element

delpos f is len f -element

end;
coherence

delneg f is len f -element

proof end;

coherence delpos f is len f -element

proof end;

registration

let f be real-valued nonnegative-yielding Function;

reducibility

abs f = f

delneg f = f

compatibility

delpos f = delall f;

compatibility

delall f = delpos f;

;

end;
reducibility

abs f = f

proof end;

reducibility delneg f = f

proof end;

correctness compatibility

delpos f = delall f;

proof end;

correctness compatibility

delall f = delpos f;

;

registration

let f be real-valued nonpositive-yielding Function;

reducibility

- (delpos f) = f

delneg f is empty-yielding

compatibility

delneg f = delall f;

compatibility

delall f = delneg f;

;

end;
reducibility

- (delpos f) = f

proof end;

coherence delneg f is empty-yielding

proof end;

correctness compatibility

delneg f = delall f;

proof end;

correctness compatibility

delall f = delneg f;

;

registration
end;

registration
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

( 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)

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)

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

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

( 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)

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;

reducibility

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

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

end;
reducibility

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

proof end;

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

proof end;

registration

let n be Nat;

let f be n -element FinSequence;

let a be Complex;

reducibility

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

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

end;
let f be n -element FinSequence;

let a be Complex;

reducibility

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

proof end;

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

proof end;

registration

let a, b be Complex;

reducibility

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

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

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

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

end;
reducibility

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

proof end;

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

proof end;

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

proof end;

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

proof end;

registration

let a, b, c be Complex;

reducibility

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

reducibility

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

reducibility

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

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

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

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

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

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

end;
reducibility

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

reducibility

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

reducibility

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

theorem FPA: :: FINSEQ_9:40

for a, b being Complex

for n being Nat

for f, g being b_{3} -element complex-valued FinSequence holds (f ^ <*a*>) + (g ^ <*b*>) = (f + g) ^ <*(a + b)*>

for n being Nat

for f, g being b

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_{3} -element complex-valued FinSequence holds (f ^ <*a*>) (#) (g ^ <*b*>) = (f (#) g) ^ <*(a * b)*>

for n being Nat

for f, g being b

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_{2} -element complex-valued FinSequence holds <*a*> + f = <*(a + (f . 1))*>

for n being non zero Nat

for f being b

proof end;

theorem :: FINSEQ_9:49

for a, b being Complex

for n being non trivial Nat

for f being b_{3} -element complex-valued FinSequence holds <*a,b*> + f = <*(a + (f . 1)),(b + (f . 2))*>

for n being non trivial Nat

for f being b

proof end;

theorem :: FINSEQ_9:50

for a being Complex

for n being non zero Nat

for f being b_{2} -element complex-valued FinSequence holds <*a*> (#) f = <*(a * (f . 1))*>

for n being non zero Nat

for f being b

proof end;

theorem :: FINSEQ_9:51

for a, b being Complex

for n being non trivial Nat

for f being b_{3} -element complex-valued FinSequence holds <*a,b*> (#) f = <*(a * (f . 1)),(b * (f . 2))*>

for n being non trivial Nat

for f being b

proof end;