:: Properties of Number-Valued Functions
:: by Library Committee
::
:: Received December 18, 2007
:: Copyright (c) 2007-2011 Association of Mizar Users


begin

Lm1: for f being FinSequence
for h being Function st dom h = dom f holds
h is FinSequence
proof end;

Lm2: for f, g being FinSequence
for h being Function st dom h = (dom f) /\ (dom g) holds
h is FinSequence
proof end;

registration
cluster Relation-like Function-like complex-valued FinSequence-like set ;
existence
ex b1 being FinSequence st b1 is complex-valued
proof end;
end;

registration
let r be rational number ;
cluster |.r.| -> rational ;
coherence
|.r.| is rational
proof end;
end;

definition
let f1, f2 be complex-valued Function;
deffunc H1( set ) -> set = (f1 . $1) + (f2 . $1);
set X = (dom f1) /\ (dom f2);
func f1 + f2 -> Function means :Def1: :: VALUED_1:def 1
( dom it = (dom f1) /\ (dom f2) & ( for c being set st c in dom it holds
it . c = (f1 . c) + (f2 . c) ) );
existence
ex b1 being Function st
( dom b1 = (dom f1) /\ (dom f2) & ( for c being set st c in dom b1 holds
b1 . c = (f1 . c) + (f2 . c) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = (dom f1) /\ (dom f2) & ( for c being set st c in dom b1 holds
b1 . c = (f1 . c) + (f2 . c) ) & dom b2 = (dom f1) /\ (dom f2) & ( for c being set st c in dom b2 holds
b2 . c = (f1 . c) + (f2 . c) ) holds
b1 = b2
proof end;
commutativity
for b1 being Function
for f1, f2 being complex-valued Function st dom b1 = (dom f1) /\ (dom f2) & ( for c being set st c in dom b1 holds
b1 . c = (f1 . c) + (f2 . c) ) holds
( dom b1 = (dom f2) /\ (dom f1) & ( for c being set st c in dom b1 holds
b1 . c = (f2 . c) + (f1 . c) ) )
;
end;

:: deftheorem Def1 defines + VALUED_1:def 1 :
for f1, f2 being complex-valued Function
for b3 being Function holds
( b3 = f1 + f2 iff ( dom b3 = (dom f1) /\ (dom f2) & ( for c being set st c in dom b3 holds
b3 . c = (f1 . c) + (f2 . c) ) ) );

registration
let f1, f2 be complex-valued Function;
cluster f1 + f2 -> complex-valued ;
coherence
f1 + f2 is complex-valued
proof end;
end;

registration
let f1, f2 be real-valued Function;
cluster f1 + f2 -> real-valued ;
coherence
f1 + f2 is real-valued
proof end;
end;

registration
let f1, f2 be rational-valued Function;
cluster f1 + f2 -> rational-valued ;
coherence
f1 + f2 is rational-valued
proof end;
end;

registration
let f1, f2 be integer-valued Function;
cluster f1 + f2 -> integer-valued ;
coherence
f1 + f2 is integer-valued
proof end;
end;

registration
let f1, f2 be natural-valued Function;
cluster f1 + f2 -> natural-valued ;
coherence
f1 + f2 is natural-valued
proof end;
end;

definition
let C be set ;
let D1, D2 be complex-membered set ;
let f1 be PartFunc of C,D1;
let f2 be PartFunc of C,D2;
:: original: +
redefine func f1 + f2 -> PartFunc of C,COMPLEX;
coherence
f1 + f2 is PartFunc of C,COMPLEX
proof end;
end;

definition
let C be set ;
let D1, D2 be real-membered set ;
let f1 be PartFunc of C,D1;
let f2 be PartFunc of C,D2;
:: original: +
redefine func f1 + f2 -> PartFunc of C,REAL;
coherence
f1 + f2 is PartFunc of C,REAL
proof end;
end;

definition
let C be set ;
let D1, D2 be rational-membered set ;
let f1 be PartFunc of C,D1;
let f2 be PartFunc of C,D2;
:: original: +
redefine func f1 + f2 -> PartFunc of C,RAT;
coherence
f1 + f2 is PartFunc of C,RAT
proof end;
end;

definition
let C be set ;
let D1, D2 be integer-membered set ;
let f1 be PartFunc of C,D1;
let f2 be PartFunc of C,D2;
:: original: +
redefine func f1 + f2 -> PartFunc of C,INT;
coherence
f1 + f2 is PartFunc of C,INT
proof end;
end;

definition
let C be set ;
let D1, D2 be natural-membered set ;
let f1 be PartFunc of C,D1;
let f2 be PartFunc of C,D2;
:: original: +
redefine func f1 + f2 -> PartFunc of C,NAT;
coherence
f1 + f2 is PartFunc of C,NAT
proof end;
end;

registration
let C be set ;
let D1, D2 be non empty complex-membered set ;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
cluster f1 + f2 -> total PartFunc of C,COMPLEX;
coherence
for b1 being PartFunc of C,COMPLEX st b1 = f1 + f2 holds
b1 is total
proof end;
end;

registration
let C be set ;
let D1, D2 be non empty real-membered set ;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
cluster f1 + f2 -> total PartFunc of C,REAL;
coherence
for b1 being PartFunc of C,REAL st b1 = f1 + f2 holds
b1 is total
proof end;
end;

registration
let C be set ;
let D1, D2 be non empty rational-membered set ;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
cluster f1 + f2 -> total PartFunc of C,RAT;
coherence
for b1 being PartFunc of C,RAT st b1 = f1 + f2 holds
b1 is total
proof end;
end;

registration
let C be set ;
let D1, D2 be non empty integer-membered set ;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
cluster f1 + f2 -> total PartFunc of C,INT;
coherence
for b1 being PartFunc of C,INT st b1 = f1 + f2 holds
b1 is total
proof end;
end;

registration
let C be set ;
let D1, D2 be non empty natural-membered set ;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
cluster f1 + f2 -> total PartFunc of C,NAT;
coherence
for b1 being PartFunc of C,NAT st b1 = f1 + f2 holds
b1 is total
proof end;
end;

theorem :: VALUED_1:1
for C being set
for D1, D2 being non empty complex-membered set
for f1 being Function of C,D1
for f2 being Function of C,D2
for c being Element of C holds (f1 + f2) . c = (f1 . c) + (f2 . c)
proof end;

registration
let f1, f2 be complex-valued FinSequence;
cluster f1 + f2 -> FinSequence-like ;
coherence
f1 + f2 is FinSequence-like
proof end;
end;

begin

definition
let f be complex-valued Function;
let r be complex number ;
deffunc H1( set ) -> set = r + (f . $1);
func r + f -> Function means :Def2: :: VALUED_1:def 2
( dom it = dom f & ( for c being set st c in dom it holds
it . c = r + (f . c) ) );
existence
ex b1 being Function st
( dom b1 = dom f & ( for c being set st c in dom b1 holds
b1 . c = r + (f . c) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = dom f & ( for c being set st c in dom b1 holds
b1 . c = r + (f . c) ) & dom b2 = dom f & ( for c being set st c in dom b2 holds
b2 . c = r + (f . c) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines + VALUED_1:def 2 :
for f being complex-valued Function
for r being complex number
for b3 being Function holds
( b3 = r + f iff ( dom b3 = dom f & ( for c being set st c in dom b3 holds
b3 . c = r + (f . c) ) ) );

notation
let f be complex-valued Function;
let r be complex number ;
synonym f + r for r + f;
end;

registration
let f be complex-valued Function;
let r be complex number ;
cluster r + f -> complex-valued ;
coherence
r + f is complex-valued
proof end;
end;

registration
let f be real-valued Function;
let r be real number ;
cluster r + f -> real-valued ;
coherence
r + f is real-valued
proof end;
end;

registration
let f be rational-valued Function;
let r be rational number ;
cluster r + f -> rational-valued ;
coherence
r + f is rational-valued
proof end;
end;

registration
let f be integer-valued Function;
let r be integer number ;
cluster r + f -> integer-valued ;
coherence
r + f is integer-valued
proof end;
end;

registration
let f be natural-valued Function;
let r be natural number ;
cluster r + f -> natural-valued ;
coherence
r + f is natural-valued
proof end;
end;

definition
let C be set ;
let D be complex-membered set ;
let f be PartFunc of C,D;
let r be complex number ;
:: original: +
redefine func r + f -> PartFunc of C,COMPLEX;
coherence
r + f is PartFunc of C,COMPLEX
proof end;
end;

definition
let C be set ;
let D be real-membered set ;
let f be PartFunc of C,D;
let r be real number ;
:: original: +
redefine func r + f -> PartFunc of C,REAL;
coherence
r + f is PartFunc of C,REAL
proof end;
end;

definition
let C be set ;
let D be rational-membered set ;
let f be PartFunc of C,D;
let r be rational number ;
:: original: +
redefine func r + f -> PartFunc of C,RAT;
coherence
r + f is PartFunc of C,RAT
proof end;
end;

definition
let C be set ;
let D be integer-membered set ;
let f be PartFunc of C,D;
let r be integer number ;
:: original: +
redefine func r + f -> PartFunc of C,INT;
coherence
r + f is PartFunc of C,INT
proof end;
end;

definition
let C be set ;
let D be natural-membered set ;
let f be PartFunc of C,D;
let r be natural number ;
:: original: +
redefine func r + f -> PartFunc of C,NAT;
coherence
r + f is PartFunc of C,NAT
proof end;
end;

registration
let C be set ;
let D be non empty complex-membered set ;
let f be Function of C,D;
let r be complex number ;
cluster r + f -> total PartFunc of C,COMPLEX;
coherence
for b1 being PartFunc of C,COMPLEX st b1 = r + f holds
b1 is total
proof end;
end;

registration
let C be set ;
let D be non empty real-membered set ;
let f be Function of C,D;
let r be real number ;
cluster r + f -> total PartFunc of C,REAL;
coherence
for b1 being PartFunc of C,REAL st b1 = r + f holds
b1 is total
proof end;
end;

registration
let C be set ;
let D be non empty rational-membered set ;
let f be Function of C,D;
let r be rational number ;
cluster r + f -> total PartFunc of C,RAT;
coherence
for b1 being PartFunc of C,RAT st b1 = r + f holds
b1 is total
proof end;
end;

registration
let C be set ;
let D be non empty integer-membered set ;
let f be Function of C,D;
let r be integer number ;
cluster r + f -> total PartFunc of C,INT;
coherence
for b1 being PartFunc of C,INT st b1 = r + f holds
b1 is total
proof end;
end;

registration
let C be set ;
let D be non empty natural-membered set ;
let f be Function of C,D;
let r be natural number ;
cluster r + f -> total PartFunc of C,NAT;
coherence
for b1 being PartFunc of C,NAT st b1 = r + f holds
b1 is total
proof end;
end;

theorem :: VALUED_1:2
for C being non empty set
for D being non empty complex-membered set
for f being Function of C,D
for r being complex number
for c being Element of C holds (r + f) . c = r + (f . c)
proof end;

registration
let f be complex-valued FinSequence;
let r be complex number ;
cluster r + f -> FinSequence-like ;
coherence
r + f is FinSequence-like
proof end;
end;

begin

definition
let f be complex-valued Function;
let r be complex number ;
func f - r -> Function equals :: VALUED_1:def 3
(- r) + f;
coherence
(- r) + f is Function
;
end;

:: deftheorem defines - VALUED_1:def 3 :
for f being complex-valued Function
for r being complex number holds f - r = (- r) + f;

theorem :: VALUED_1:3
for f being complex-valued Function
for r being complex number holds
( dom (f - r) = dom f & ( for c being set st c in dom f holds
(f - r) . c = (f . c) - r ) )
proof end;

registration
let f be complex-valued Function;
let r be complex number ;
cluster f - r -> complex-valued ;
coherence
f - r is complex-valued
;
end;

registration
let f be real-valued Function;
let r be real number ;
cluster f - r -> real-valued ;
coherence
f - r is real-valued
;
end;

registration
let f be rational-valued Function;
let r be rational number ;
cluster f - r -> rational-valued ;
coherence
f - r is rational-valued
;
end;

registration
let f be integer-valued Function;
let r be integer number ;
cluster f - r -> integer-valued ;
coherence
f - r is integer-valued
;
end;

definition
let C be set ;
let D be complex-membered set ;
let f be PartFunc of C,D;
let r be complex number ;
:: original: -
redefine func f - r -> PartFunc of C,COMPLEX;
coherence
f - r is PartFunc of C,COMPLEX
proof end;
end;

definition
let C be set ;
let D be real-membered set ;
let f be PartFunc of C,D;
let r be real number ;
:: original: -
redefine func f - r -> PartFunc of C,REAL;
coherence
f - r is PartFunc of C,REAL
proof end;
end;

definition
let C be set ;
let D be rational-membered set ;
let f be PartFunc of C,D;
let r be rational number ;
:: original: -
redefine func f - r -> PartFunc of C,RAT;
coherence
f - r is PartFunc of C,RAT
proof end;
end;

definition
let C be set ;
let D be integer-membered set ;
let f be PartFunc of C,D;
let r be integer number ;
:: original: -
redefine func f - r -> PartFunc of C,INT;
coherence
f - r is PartFunc of C,INT
proof end;
end;

registration
let C be set ;
let D be non empty complex-membered set ;
let f be Function of C,D;
let r be complex number ;
cluster f - r -> total PartFunc of C,COMPLEX;
coherence
for b1 being PartFunc of C,COMPLEX st b1 = f - r holds
b1 is total
;
end;

registration
let C be set ;
let D be non empty real-membered set ;
let f be Function of C,D;
let r be real number ;
cluster f - r -> total PartFunc of C,REAL;
coherence
for b1 being PartFunc of C,REAL st b1 = f - r holds
b1 is total
;
end;

registration
let C be set ;
let D be non empty rational-membered set ;
let f be Function of C,D;
let r be rational number ;
cluster f - r -> total PartFunc of C,RAT;
coherence
for b1 being PartFunc of C,RAT st b1 = f - r holds
b1 is total
;
end;

registration
let C be set ;
let D be non empty integer-membered set ;
let f be Function of C,D;
let r be integer number ;
cluster f - r -> total PartFunc of C,INT;
coherence
for b1 being PartFunc of C,INT st b1 = f - r holds
b1 is total
;
end;

theorem :: VALUED_1:4
for C being non empty set
for D being non empty complex-membered set
for f being Function of C,D
for r being complex number
for c being Element of C holds (f - r) . c = (f . c) - r
proof end;

registration
let f be complex-valued FinSequence;
let r be complex number ;
cluster f - r -> FinSequence-like ;
coherence
f - r is FinSequence-like
;
end;

begin

definition
let f1, f2 be complex-valued Function;
deffunc H1( set ) -> set = (f1 . $1) * (f2 . $1);
set X = (dom f1) /\ (dom f2);
func f1 (#) f2 -> Function means :Def4: :: VALUED_1:def 4
( dom it = (dom f1) /\ (dom f2) & ( for c being set st c in dom it holds
it . c = (f1 . c) * (f2 . c) ) );
existence
ex b1 being Function st
( dom b1 = (dom f1) /\ (dom f2) & ( for c being set st c in dom b1 holds
b1 . c = (f1 . c) * (f2 . c) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = (dom f1) /\ (dom f2) & ( for c being set st c in dom b1 holds
b1 . c = (f1 . c) * (f2 . c) ) & dom b2 = (dom f1) /\ (dom f2) & ( for c being set st c in dom b2 holds
b2 . c = (f1 . c) * (f2 . c) ) holds
b1 = b2
proof end;
commutativity
for b1 being Function
for f1, f2 being complex-valued Function st dom b1 = (dom f1) /\ (dom f2) & ( for c being set st c in dom b1 holds
b1 . c = (f1 . c) * (f2 . c) ) holds
( dom b1 = (dom f2) /\ (dom f1) & ( for c being set st c in dom b1 holds
b1 . c = (f2 . c) * (f1 . c) ) )
;
end;

:: deftheorem Def4 defines (#) VALUED_1:def 4 :
for f1, f2 being complex-valued Function
for b3 being Function holds
( b3 = f1 (#) f2 iff ( dom b3 = (dom f1) /\ (dom f2) & ( for c being set st c in dom b3 holds
b3 . c = (f1 . c) * (f2 . c) ) ) );

theorem :: VALUED_1:5
for f1, f2 being complex-valued Function
for c being set holds (f1 (#) f2) . c = (f1 . c) * (f2 . c)
proof end;

registration
let f1, f2 be complex-valued Function;
cluster f1 (#) f2 -> complex-valued ;
coherence
f1 (#) f2 is complex-valued
proof end;
end;

registration
let f1, f2 be real-valued Function;
cluster f1 (#) f2 -> real-valued ;
coherence
f1 (#) f2 is real-valued
proof end;
end;

registration
let f1, f2 be rational-valued Function;
cluster f1 (#) f2 -> rational-valued ;
coherence
f1 (#) f2 is rational-valued
proof end;
end;

registration
let f1, f2 be integer-valued Function;
cluster f1 (#) f2 -> integer-valued ;
coherence
f1 (#) f2 is integer-valued
proof end;
end;

registration
let f1, f2 be natural-valued Function;
cluster f1 (#) f2 -> natural-valued ;
coherence
f1 (#) f2 is natural-valued
proof end;
end;

definition
let C be set ;
let D1, D2 be complex-membered set ;
let f1 be PartFunc of C,D1;
let f2 be PartFunc of C,D2;
:: original: (#)
redefine func f1 (#) f2 -> PartFunc of C,COMPLEX;
coherence
f1 (#) f2 is PartFunc of C,COMPLEX
proof end;
end;

definition
let C be set ;
let D1, D2 be real-membered set ;
let f1 be PartFunc of C,D1;
let f2 be PartFunc of C,D2;
:: original: (#)
redefine func f1 (#) f2 -> PartFunc of C,REAL;
coherence
f1 (#) f2 is PartFunc of C,REAL
proof end;
end;

definition
let C be set ;
let D1, D2 be rational-membered set ;
let f1 be PartFunc of C,D1;
let f2 be PartFunc of C,D2;
:: original: (#)
redefine func f1 (#) f2 -> PartFunc of C,RAT;
coherence
f1 (#) f2 is PartFunc of C,RAT
proof end;
end;

definition
let C be set ;
let D1, D2 be integer-membered set ;
let f1 be PartFunc of C,D1;
let f2 be PartFunc of C,D2;
:: original: (#)
redefine func f1 (#) f2 -> PartFunc of C,INT;
coherence
f1 (#) f2 is PartFunc of C,INT
proof end;
end;

definition
let C be set ;
let D1, D2 be natural-membered set ;
let f1 be PartFunc of C,D1;
let f2 be PartFunc of C,D2;
:: original: (#)
redefine func f1 (#) f2 -> PartFunc of C,NAT;
coherence
f1 (#) f2 is PartFunc of C,NAT
proof end;
end;

registration
let C be set ;
let D1, D2 be non empty complex-membered set ;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
cluster f1 (#) f2 -> total PartFunc of C,COMPLEX;
coherence
for b1 being PartFunc of C,COMPLEX st b1 = f1 (#) f2 holds
b1 is total
proof end;
end;

registration
let C be set ;
let D1, D2 be non empty real-membered set ;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
cluster f1 (#) f2 -> total PartFunc of C,REAL;
coherence
for b1 being PartFunc of C,REAL st b1 = f1 (#) f2 holds
b1 is total
proof end;
end;

registration
let C be set ;
let D1, D2 be non empty rational-membered set ;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
cluster f1 (#) f2 -> total PartFunc of C,RAT;
coherence
for b1 being PartFunc of C,RAT st b1 = f1 (#) f2 holds
b1 is total
proof end;
end;

registration
let C be set ;
let D1, D2 be non empty integer-membered set ;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
cluster f1 (#) f2 -> total PartFunc of C,INT;
coherence
for b1 being PartFunc of C,INT st b1 = f1 (#) f2 holds
b1 is total
proof end;
end;

registration
let C be set ;
let D1, D2 be non empty natural-membered set ;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
cluster f1 (#) f2 -> total PartFunc of C,NAT;
coherence
for b1 being PartFunc of C,NAT st b1 = f1 (#) f2 holds
b1 is total
proof end;
end;

registration
let f1, f2 be complex-valued FinSequence;
cluster f1 (#) f2 -> FinSequence-like ;
coherence
f1 (#) f2 is FinSequence-like
proof end;
end;

begin

definition
let f be complex-valued Function;
let r be complex number ;
deffunc H1( set ) -> set = r * (f . $1);
func r (#) f -> Function means :Def5: :: VALUED_1:def 5
( dom it = dom f & ( for c being set st c in dom it holds
it . c = r * (f . c) ) );
existence
ex b1 being Function st
( dom b1 = dom f & ( for c being set st c in dom b1 holds
b1 . c = r * (f . c) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = dom f & ( for c being set st c in dom b1 holds
b1 . c = r * (f . c) ) & dom b2 = dom f & ( for c being set st c in dom b2 holds
b2 . c = r * (f . c) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines (#) VALUED_1:def 5 :
for f being complex-valued Function
for r being complex number
for b3 being Function holds
( b3 = r (#) f iff ( dom b3 = dom f & ( for c being set st c in dom b3 holds
b3 . c = r * (f . c) ) ) );

notation
let f be complex-valued Function;
let r be complex number ;
synonym f (#) r for r (#) f;
end;

theorem Th6: :: VALUED_1:6
for f being complex-valued Function
for r being complex number
for c being set holds (r (#) f) . c = r * (f . c)
proof end;

registration
let f be complex-valued Function;
let r be complex number ;
cluster r (#) f -> complex-valued ;
coherence
r (#) f is complex-valued
proof end;
end;

registration
let f be real-valued Function;
let r be real number ;
cluster r (#) f -> real-valued ;
coherence
r (#) f is real-valued
proof end;
end;

registration
let f be rational-valued Function;
let r be rational number ;
cluster r (#) f -> rational-valued ;
coherence
r (#) f is rational-valued
proof end;
end;

registration
let f be integer-valued Function;
let r be integer number ;
cluster r (#) f -> integer-valued ;
coherence
r (#) f is integer-valued
proof end;
end;

registration
let f be natural-valued Function;
let r be natural number ;
cluster r (#) f -> natural-valued ;
coherence
r (#) f is natural-valued
proof end;
end;

definition
let C be set ;
let D be complex-membered set ;
let f be PartFunc of C,D;
let r be complex number ;
:: original: (#)
redefine func r (#) f -> PartFunc of C,COMPLEX;
coherence
r (#) f is PartFunc of C,COMPLEX
proof end;
end;

definition
let C be set ;
let D be real-membered set ;
let f be PartFunc of C,D;
let r be real number ;
:: original: (#)
redefine func r (#) f -> PartFunc of C,REAL;
coherence
r (#) f is PartFunc of C,REAL
proof end;
end;

definition
let C be set ;
let D be rational-membered set ;
let f be PartFunc of C,D;
let r be rational number ;
:: original: (#)
redefine func r (#) f -> PartFunc of C,RAT;
coherence
r (#) f is PartFunc of C,RAT
proof end;
end;

definition
let C be set ;
let D be integer-membered set ;
let f be PartFunc of C,D;
let r be integer number ;
:: original: (#)
redefine func r (#) f -> PartFunc of C,INT;
coherence
r (#) f is PartFunc of C,INT
proof end;
end;

definition
let C be set ;
let D be natural-membered set ;
let f be PartFunc of C,D;
let r be natural number ;
:: original: (#)
redefine func r (#) f -> PartFunc of C,NAT;
coherence
r (#) f is PartFunc of C,NAT
proof end;
end;

registration
let C be set ;
let D be non empty complex-membered set ;
let f be Function of C,D;
let r be complex number ;
cluster r (#) f -> total PartFunc of C,COMPLEX;
coherence
for b1 being PartFunc of C,COMPLEX st b1 = r (#) f holds
b1 is total
proof end;
end;

registration
let C be set ;
let D be non empty real-membered set ;
let f be Function of C,D;
let r be real number ;
cluster r (#) f -> total PartFunc of C,REAL;
coherence
for b1 being PartFunc of C,REAL st b1 = r (#) f holds
b1 is total
proof end;
end;

registration
let C be set ;
let D be non empty rational-membered set ;
let f be Function of C,D;
let r be rational number ;
cluster r (#) f -> total PartFunc of C,RAT;
coherence
for b1 being PartFunc of C,RAT st b1 = r (#) f holds
b1 is total
proof end;
end;

registration
let C be set ;
let D be non empty integer-membered set ;
let f be Function of C,D;
let r be integer number ;
cluster r (#) f -> total PartFunc of C,INT;
coherence
for b1 being PartFunc of C,INT st b1 = r (#) f holds
b1 is total
proof end;
end;

registration
let C be set ;
let D be non empty natural-membered set ;
let f be Function of C,D;
let r be natural number ;
cluster r (#) f -> total PartFunc of C,NAT;
coherence
for b1 being PartFunc of C,NAT st b1 = r (#) f holds
b1 is total
proof end;
end;

theorem :: VALUED_1:7
for C being non empty set
for D being non empty complex-membered set
for f being Function of C,D
for r being complex number
for g being Function of C,COMPLEX st ( for c being Element of C holds g . c = r * (f . c) ) holds
g = r (#) f
proof end;

registration
let f be complex-valued FinSequence;
let r be complex number ;
cluster r (#) f -> FinSequence-like ;
coherence
r (#) f is FinSequence-like
proof end;
end;

begin

definition
let f be complex-valued Function;
func - f -> complex-valued Function equals :: VALUED_1:def 6
(- 1) (#) f;
coherence
(- 1) (#) f is complex-valued Function
;
involutiveness
for b1, b2 being complex-valued Function st b1 = (- 1) (#) b2 holds
b2 = (- 1) (#) b1
proof end;
end;

:: deftheorem defines - VALUED_1:def 6 :
for f being complex-valued Function holds - f = (- 1) (#) f;

theorem Th8: :: VALUED_1:8
for f being complex-valued Function holds
( dom (- f) = dom f & ( for c being set holds (- f) . c = - (f . c) ) )
proof end;

theorem :: VALUED_1:9
for f being complex-valued Function
for g being Function st dom f = dom g & ( for c being set st c in dom f holds
g . c = - (f . c) ) holds
g = - f
proof end;

registration
let f be complex-valued Function;
cluster - f -> complex-valued ;
coherence
- f is complex-valued
;
end;

registration
let f be real-valued Function;
cluster - f -> complex-valued real-valued ;
coherence
- f is real-valued
;
end;

registration
let f be rational-valued Function;
cluster - f -> complex-valued rational-valued ;
coherence
- f is rational-valued
;
end;

registration
let f be integer-valued Function;
cluster - f -> complex-valued integer-valued ;
coherence
- f is integer-valued
;
end;

definition
let C be set ;
let D be complex-membered set ;
let f be PartFunc of C,D;
:: original: -
redefine func - f -> PartFunc of C,COMPLEX;
coherence
- f is PartFunc of C,COMPLEX
proof end;
end;

definition
let C be set ;
let D be real-membered set ;
let f be PartFunc of C,D;
:: original: -
redefine func - f -> PartFunc of C,REAL;
coherence
- f is PartFunc of C,REAL
proof end;
end;

definition
let C be set ;
let D be rational-membered set ;
let f be PartFunc of C,D;
:: original: -
redefine func - f -> PartFunc of C,RAT;
coherence
- f is PartFunc of C,RAT
proof end;
end;

definition
let C be set ;
let D be integer-membered set ;
let f be PartFunc of C,D;
:: original: -
redefine func - f -> PartFunc of C,INT;
coherence
- f is PartFunc of C,INT
proof end;
end;

registration
let C be set ;
let D be non empty complex-membered set ;
let f be Function of C,D;
cluster - f -> total PartFunc of C,COMPLEX;
coherence
for b1 being PartFunc of C,COMPLEX st b1 = - f holds
b1 is total
;
end;

registration
let C be set ;
let D be non empty real-membered set ;
let f be Function of C,D;
cluster - f -> total PartFunc of C,REAL;
coherence
for b1 being PartFunc of C,REAL st b1 = - f holds
b1 is total
;
end;

registration
let C be set ;
let D be non empty rational-membered set ;
let f be Function of C,D;
cluster - f -> total PartFunc of C,RAT;
coherence
for b1 being PartFunc of C,RAT st b1 = - f holds
b1 is total
;
end;

registration
let C be set ;
let D be non empty integer-membered set ;
let f be Function of C,D;
cluster - f -> total PartFunc of C,INT;
coherence
for b1 being PartFunc of C,INT st b1 = - f holds
b1 is total
;
end;

registration
let f be complex-valued FinSequence;
cluster - f -> complex-valued FinSequence-like ;
coherence
- f is FinSequence-like
;
end;

begin

definition
let f be complex-valued Function;
deffunc H1( set ) -> set = (f . $1) " ;
func f " -> complex-valued Function means :Def7: :: VALUED_1:def 7
( dom it = dom f & ( for c being set st c in dom it holds
it . c = (f . c) " ) );
existence
ex b1 being complex-valued Function st
( dom b1 = dom f & ( for c being set st c in dom b1 holds
b1 . c = (f . c) " ) )
proof end;
uniqueness
for b1, b2 being complex-valued Function st dom b1 = dom f & ( for c being set st c in dom b1 holds
b1 . c = (f . c) " ) & dom b2 = dom f & ( for c being set st c in dom b2 holds
b2 . c = (f . c) " ) holds
b1 = b2
proof end;
involutiveness
for b1, b2 being complex-valued Function st dom b1 = dom b2 & ( for c being set st c in dom b1 holds
b1 . c = (b2 . c) " ) holds
( dom b2 = dom b1 & ( for c being set st c in dom b2 holds
b2 . c = (b1 . c) " ) )
proof end;
end;

:: deftheorem Def7 defines " VALUED_1:def 7 :
for f, b2 being complex-valued Function holds
( b2 = f " iff ( dom b2 = dom f & ( for c being set st c in dom b2 holds
b2 . c = (f . c) " ) ) );

theorem Th10: :: VALUED_1:10
for f being complex-valued Function
for c being set holds (f ") . c = (f . c) "
proof end;

registration
let f be real-valued Function;
cluster f " -> complex-valued real-valued ;
coherence
f " is real-valued
proof end;
end;

registration
let f be rational-valued Function;
cluster f " -> complex-valued rational-valued ;
coherence
f " is rational-valued
proof end;
end;

definition
let C be set ;
let D be complex-membered set ;
let f be PartFunc of C,D;
:: original: "
redefine func f " -> PartFunc of C,COMPLEX;
coherence
f " is PartFunc of C,COMPLEX
proof end;
end;

definition
let C be set ;
let D be real-membered set ;
let f be PartFunc of C,D;
:: original: "
redefine func f " -> PartFunc of C,REAL;
coherence
f " is PartFunc of C,REAL
proof end;
end;

definition
let C be set ;
let D be rational-membered set ;
let f be PartFunc of C,D;
:: original: "
redefine func f " -> PartFunc of C,RAT;
coherence
f " is PartFunc of C,RAT
proof end;
end;

registration
let C be set ;
let D be non empty complex-membered set ;
let f be Function of C,D;
cluster f " -> total PartFunc of C,COMPLEX;
coherence
for b1 being PartFunc of C,COMPLEX st b1 = f " holds
b1 is total
proof end;
end;

registration
let C be set ;
let D be non empty real-membered set ;
let f be Function of C,D;
cluster f " -> total PartFunc of C,REAL;
coherence
for b1 being PartFunc of C,REAL st b1 = f " holds
b1 is total
proof end;
end;

registration
let C be set ;
let D be non empty rational-membered set ;
let f be Function of C,D;
cluster f " -> total PartFunc of C,RAT;
coherence
for b1 being PartFunc of C,RAT st b1 = f " holds
b1 is total
proof end;
end;

registration
let f be complex-valued FinSequence;
cluster f " -> complex-valued FinSequence-like ;
coherence
f " is FinSequence-like
proof end;
end;

begin

definition
let f be complex-valued Function;
func f ^2 -> Function equals :: VALUED_1:def 8
f (#) f;
coherence
f (#) f is Function
;
end;

:: deftheorem defines ^2 VALUED_1:def 8 :
for f being complex-valued Function holds f ^2 = f (#) f;

theorem Th11: :: VALUED_1:11
for f being complex-valued Function holds
( dom (f ^2) = dom f & ( for c being set holds (f ^2) . c = (f . c) ^2 ) )
proof end;

registration
let f be complex-valued Function;
cluster f ^2 -> complex-valued ;
coherence
f ^2 is complex-valued
;
end;

registration
let f be real-valued Function;
cluster f ^2 -> real-valued ;
coherence
f ^2 is real-valued
;
end;

registration
let f be rational-valued Function;
cluster f ^2 -> rational-valued ;
coherence
f ^2 is rational-valued
;
end;

registration
let f be integer-valued Function;
cluster f ^2 -> integer-valued ;
coherence
f ^2 is integer-valued
;
end;

registration
let f be natural-valued Function;
cluster f ^2 -> natural-valued ;
coherence
f ^2 is natural-valued
;
end;

definition
let C be set ;
let D be complex-membered set ;
let f be PartFunc of C,D;
:: original: ^2
redefine func f ^2 -> PartFunc of C,COMPLEX;
coherence
f ^2 is PartFunc of C,COMPLEX
proof end;
end;

definition
let C be set ;
let D be real-membered set ;
let f be PartFunc of C,D;
:: original: ^2
redefine func f ^2 -> PartFunc of C,REAL;
coherence
f ^2 is PartFunc of C,REAL
proof end;
end;

definition
let C be set ;
let D be rational-membered set ;
let f be PartFunc of C,D;
:: original: ^2
redefine func f ^2 -> PartFunc of C,RAT;
coherence
f ^2 is PartFunc of C,RAT
proof end;
end;

definition
let C be set ;
let D be integer-membered set ;
let f be PartFunc of C,D;
:: original: ^2
redefine func f ^2 -> PartFunc of C,INT;
coherence
f ^2 is PartFunc of C,INT
proof end;
end;

definition
let C be set ;
let D be natural-membered set ;
let f be PartFunc of C,D;
:: original: ^2
redefine func f ^2 -> PartFunc of C,NAT;
coherence
f ^2 is PartFunc of C,NAT
proof end;
end;

registration
let C be set ;
let D be non empty complex-membered set ;
let f be Function of C,D;
cluster f ^2 -> total PartFunc of C,COMPLEX;
coherence
for b1 being PartFunc of C,COMPLEX st b1 = f ^2 holds
b1 is total
;
end;

registration
let C be set ;
let D be non empty real-membered set ;
let f be Function of C,D;
cluster f ^2 -> total PartFunc of C,REAL;
coherence
for b1 being PartFunc of C,REAL st b1 = f ^2 holds
b1 is total
;
end;

registration
let C be set ;
let D be non empty rational-membered set ;
let f be Function of C,D;
cluster f ^2 -> total PartFunc of C,RAT;
coherence
for b1 being PartFunc of C,RAT st b1 = f ^2 holds
b1 is total
;
end;

registration
let C be set ;
let D be non empty integer-membered set ;
let f be Function of C,D;
cluster f ^2 -> total PartFunc of C,INT;
coherence
for b1 being PartFunc of C,INT st b1 = f ^2 holds
b1 is total
;
end;

registration
let C be set ;
let D be non empty natural-membered set ;
let f be Function of C,D;
cluster f ^2 -> total PartFunc of C,NAT;
coherence
for b1 being PartFunc of C,NAT st b1 = f ^2 holds
b1 is total
;
end;

registration
let f be complex-valued FinSequence;
cluster f ^2 -> FinSequence-like ;
coherence
f ^2 is FinSequence-like
;
end;

begin

definition
let f1, f2 be complex-valued Function;
func f1 - f2 -> Function equals :: VALUED_1:def 9
f1 + (- f2);
coherence
f1 + (- f2) is Function
;
end;

:: deftheorem defines - VALUED_1:def 9 :
for f1, f2 being complex-valued Function holds f1 - f2 = f1 + (- f2);

registration
let f1, f2 be complex-valued Function;
cluster f1 - f2 -> complex-valued ;
coherence
f1 - f2 is complex-valued
;
end;

registration
let f1, f2 be real-valued Function;
cluster f1 - f2 -> real-valued ;
coherence
f1 - f2 is real-valued
;
end;

registration
let f1, f2 be rational-valued Function;
cluster f1 - f2 -> rational-valued ;
coherence
f1 - f2 is rational-valued
;
end;

registration
let f1, f2 be integer-valued Function;
cluster f1 - f2 -> integer-valued ;
coherence
f1 - f2 is integer-valued
;
end;

theorem Th12: :: VALUED_1:12
for f1, f2 being complex-valued Function holds dom (f1 - f2) = (dom f1) /\ (dom f2)
proof end;

theorem :: VALUED_1:13
for f1, f2 being complex-valued Function
for c being set st c in dom (f1 - f2) holds
(f1 - f2) . c = (f1 . c) - (f2 . c)
proof end;

theorem :: VALUED_1:14
for f1, f2 being complex-valued Function
for f being Function st dom f = dom (f1 - f2) & ( for c being set st c in dom f holds
f . c = (f1 . c) - (f2 . c) ) holds
f = f1 - f2
proof end;

definition
let C be set ;
let D1, D2 be complex-membered set ;
let f1 be PartFunc of C,D1;
let f2 be PartFunc of C,D2;
:: original: -
redefine func f1 - f2 -> PartFunc of C,COMPLEX;
coherence
f1 - f2 is PartFunc of C,COMPLEX
proof end;
end;

definition
let C be set ;
let D1, D2 be real-membered set ;
let f1 be PartFunc of C,D1;
let f2 be PartFunc of C,D2;
:: original: -
redefine func f1 - f2 -> PartFunc of C,REAL;
coherence
f1 - f2 is PartFunc of C,REAL
proof end;
end;

definition
let C be set ;
let D1, D2 be rational-membered set ;
let f1 be PartFunc of C,D1;
let f2 be PartFunc of C,D2;
:: original: -
redefine func f1 - f2 -> PartFunc of C,RAT;
coherence
f1 - f2 is PartFunc of C,RAT
proof end;
end;

definition
let C be set ;
let D1, D2 be integer-membered set ;
let f1 be PartFunc of C,D1;
let f2 be PartFunc of C,D2;
:: original: -
redefine func f1 - f2 -> PartFunc of C,INT;
coherence
f1 - f2 is PartFunc of C,INT
proof end;
end;

Lm3: for C being set
for D1, D2 being non empty complex-membered set
for f1 being Function of C,D1
for f2 being Function of C,D2 holds dom (f1 - f2) = C
proof end;

registration
let C be set ;
let D1, D2 be non empty complex-membered set ;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
cluster f1 - f2 -> total PartFunc of C,COMPLEX;
coherence
for b1 being PartFunc of C,COMPLEX st b1 = f1 - f2 holds
b1 is total
proof end;
end;

registration
let C be set ;
let D1, D2 be non empty real-membered set ;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
cluster f1 - f2 -> total PartFunc of C,REAL;
coherence
for b1 being PartFunc of C,REAL st b1 = f1 - f2 holds
b1 is total
proof end;
end;

registration
let C be set ;
let D1, D2 be non empty rational-membered set ;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
cluster f1 - f2 -> total PartFunc of C,RAT;
coherence
for b1 being PartFunc of C,RAT st b1 = f1 - f2 holds
b1 is total
proof end;
end;

registration
let C be set ;
let D1, D2 be non empty integer-membered set ;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
cluster f1 - f2 -> total PartFunc of C,INT;
coherence
for b1 being PartFunc of C,INT st b1 = f1 - f2 holds
b1 is total
proof end;
end;

theorem :: VALUED_1:15
for C being set
for D1, D2 being non empty complex-membered set
for f1 being Function of C,D1
for f2 being Function of C,D2
for c being Element of C holds (f1 - f2) . c = (f1 . c) - (f2 . c)
proof end;

registration
let f1, f2 be complex-valued FinSequence;
cluster f1 - f2 -> FinSequence-like ;
coherence
f1 - f2 is FinSequence-like
;
end;

begin

definition
let f1, f2 be complex-valued Function;
func f1 /" f2 -> Function equals :: VALUED_1:def 10
f1 (#) (f2 ");
coherence
f1 (#) (f2 ") is Function
;
end;

:: deftheorem defines /" VALUED_1:def 10 :
for f1, f2 being complex-valued Function holds f1 /" f2 = f1 (#) (f2 ");

theorem Th16: :: VALUED_1:16
for f1, f2 being complex-valued Function holds dom (f1 /" f2) = (dom f1) /\ (dom f2)
proof end;

theorem :: VALUED_1:17
for f1, f2 being complex-valued Function
for c being set holds (f1 /" f2) . c = (f1 . c) / (f2 . c)
proof end;

registration
let f1, f2 be complex-valued Function;
cluster f1 /" f2 -> complex-valued ;
coherence
f1 /" f2 is complex-valued
;
end;

registration
let f1, f2 be real-valued Function;
cluster f1 /" f2 -> real-valued ;
coherence
f1 /" f2 is real-valued
;
end;

registration
let f1, f2 be rational-valued Function;
cluster f1 /" f2 -> rational-valued ;
coherence
f1 /" f2 is rational-valued
;
end;

definition
let C be set ;
let D1, D2 be complex-membered set ;
let f1 be PartFunc of C,D1;
let f2 be PartFunc of C,D2;
:: original: /"
redefine func f1 /" f2 -> PartFunc of C,COMPLEX;
coherence
f1 /" f2 is PartFunc of C,COMPLEX
proof end;
end;

definition
let C be set ;
let D1, D2 be real-membered set ;
let f1 be PartFunc of C,D1;
let f2 be PartFunc of C,D2;
:: original: /"
redefine func f1 /" f2 -> PartFunc of C,REAL;
coherence
f1 /" f2 is PartFunc of C,REAL
proof end;
end;

definition
let C be set ;
let D1, D2 be rational-membered set ;
let f1 be PartFunc of C,D1;
let f2 be PartFunc of C,D2;
:: original: /"
redefine func f1 /" f2 -> PartFunc of C,RAT;
coherence
f1 /" f2 is PartFunc of C,RAT
proof end;
end;

Lm4: for C being set
for D1, D2 being non empty complex-membered set
for f1 being Function of C,D1
for f2 being Function of C,D2 holds dom (f1 /" f2) = C
proof end;

registration
let C be set ;
let D1, D2 be non empty complex-membered set ;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
cluster f1 /" f2 -> total PartFunc of C,COMPLEX;
coherence
for b1 being PartFunc of C,COMPLEX st b1 = f1 /" f2 holds
b1 is total
proof end;
end;

registration
let C be set ;
let D1, D2 be non empty real-membered set ;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
cluster f1 /" f2 -> total PartFunc of C,REAL;
coherence
for b1 being PartFunc of C,REAL st b1 = f1 /" f2 holds
b1 is total
proof end;
end;

registration
let C be set ;
let D1, D2 be non empty rational-membered set ;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
cluster f1 /" f2 -> total PartFunc of C,RAT;
coherence
for b1 being PartFunc of C,RAT st b1 = f1 /" f2 holds
b1 is total
proof end;
end;

registration
let f1, f2 be complex-valued FinSequence;
cluster f1 /" f2 -> FinSequence-like ;
coherence
f1 /" f2 is FinSequence-like
;
end;

begin

definition
let f be complex-valued Function;
deffunc H1( set ) -> Element of REAL = |.(f . $1).|;
func |.f.| -> real-valued Function means :Def11: :: VALUED_1:def 11
( dom it = dom f & ( for c being set st c in dom it holds
it . c = |.(f . c).| ) );
existence
ex b1 being real-valued Function st
( dom b1 = dom f & ( for c being set st c in dom b1 holds
b1 . c = |.(f . c).| ) )
proof end;
uniqueness
for b1, b2 being real-valued Function st dom b1 = dom f & ( for c being set st c in dom b1 holds
b1 . c = |.(f . c).| ) & dom b2 = dom f & ( for c being set st c in dom b2 holds
b2 . c = |.(f . c).| ) holds
b1 = b2
proof end;
projectivity
for b1, b2 being real-valued Function st dom b1 = dom b2 & ( for c being set st c in dom b1 holds
b1 . c = |.(b2 . c).| ) holds
( dom b1 = dom b1 & ( for c being set st c in dom b1 holds
b1 . c = |.(b1 . c).| ) )
proof end;
end;

:: deftheorem Def11 defines |. VALUED_1:def 11 :
for f being complex-valued Function
for b2 being real-valued Function holds
( b2 = |.f.| iff ( dom b2 = dom f & ( for c being set st c in dom b2 holds
b2 . c = |.(f . c).| ) ) );

notation
let f be complex-valued Function;
synonym abs f for |.f.|;
end;

theorem :: VALUED_1:18
for f being complex-valued Function
for c being set holds |.f.| . c = |.(f . c).|
proof end;

registration
let f be rational-valued Function;
cluster |.f.| -> real-valued rational-valued ;
coherence
|.f.| is rational-valued
proof end;
end;

registration
let f be integer-valued Function;
cluster |.f.| -> real-valued natural-valued ;
coherence
|.f.| is natural-valued
proof end;
end;

definition
let C be set ;
let D be complex-membered set ;
let f be PartFunc of C,D;
:: original: |.
redefine func |.f.| -> PartFunc of C,REAL;
coherence
|.f.| is PartFunc of C,REAL
proof end;
end;

definition
let C be set ;
let D be complex-membered set ;
let f be PartFunc of C,D;
:: original: |.
redefine func abs f -> PartFunc of C,REAL;
coherence
|.f.| is PartFunc of C,REAL
proof end;
end;

definition
let C be set ;
let D be rational-membered set ;
let f be PartFunc of C,D;
:: original: |.
redefine func |.f.| -> PartFunc of C,RAT;
coherence
|.f.| is PartFunc of C,RAT
proof end;
end;

definition
let C be set ;
let D be rational-membered set ;
let f be PartFunc of C,D;
:: original: |.
redefine func abs f -> PartFunc of C,RAT;
coherence
|.f.| is PartFunc of C,RAT
proof end;
end;

definition
let C be set ;
let D be integer-membered set ;
let f be PartFunc of C,D;
:: original: |.
redefine func |.f.| -> PartFunc of C,NAT;
coherence
|.f.| is PartFunc of C,NAT
proof end;
end;

definition
let C be set ;
let D be integer-membered set ;
let f be PartFunc of C,D;
:: original: |.
redefine func abs f -> PartFunc of C,NAT;
coherence
|.f.| is PartFunc of C,NAT
proof end;
end;

registration
let C be set ;
let D be non empty complex-membered set ;
let f be Function of C,D;
cluster |.f.| -> total PartFunc of C,REAL;
coherence
for b1 being PartFunc of C,REAL st b1 = |.f.| holds
b1 is total
proof end;
end;

registration
let C be set ;
let D be non empty rational-membered set ;
let f be Function of C,D;
cluster |.f.| -> total PartFunc of C,RAT;
coherence
for b1 being PartFunc of C,RAT st b1 = |.f.| holds
b1 is total
proof end;
end;

registration
let C be set ;
let D be non empty integer-membered set ;
let f be Function of C,D;
cluster |.f.| -> total PartFunc of C,NAT;
coherence
for b1 being PartFunc of C,NAT st b1 = |.f.| holds
b1 is total
proof end;
end;

registration
let f be complex-valued FinSequence;
cluster |.f.| -> real-valued FinSequence-like ;
coherence
|.f.| is FinSequence-like
proof end;
end;

theorem :: VALUED_1:19
for f, g being FinSequence
for h being Function st dom h = (dom f) /\ (dom g) holds
h is FinSequence by Lm2;

begin

definition
let p be Function;
let k be Element of NAT ;
func Shift (p,k) -> Function means :Def12: :: VALUED_1:def 12
( dom it = { (m + k) where m is Element of NAT : m in dom p } & ( for m being Element of NAT st m in dom p holds
it . (m + k) = p . m ) );
existence
ex b1 being Function st
( dom b1 = { (m + k) where m is Element of NAT : m in dom p } & ( for m being Element of NAT st m in dom p holds
b1 . (m + k) = p . m ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = { (m + k) where m is Element of NAT : m in dom p } & ( for m being Element of NAT st m in dom p holds
b1 . (m + k) = p . m ) & dom b2 = { (m + k) where m is Element of NAT : m in dom p } & ( for m being Element of NAT st m in dom p holds
b2 . (m + k) = p . m ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines Shift VALUED_1:def 12 :
for p being Function
for k being Element of NAT
for b3 being Function holds
( b3 = Shift (p,k) iff ( dom b3 = { (m + k) where m is Element of NAT : m in dom p } & ( for m being Element of NAT st m in dom p holds
b3 . (m + k) = p . m ) ) );

registration
let p be Function;
let k be Element of NAT ;
cluster Shift (p,k) -> NAT -defined ;
coherence
Shift (p,k) is NAT -defined
proof end;
end;

theorem :: VALUED_1:20
canceled;

theorem :: VALUED_1:21
for P, Q being Function
for k being Element of NAT st P c= Q holds
Shift (P,k) c= Shift (Q,k)
proof end;

theorem :: VALUED_1:22
for m, n being Element of NAT
for I being Function holds Shift ((Shift (I,m)),n) = Shift (I,(m + n))
proof end;

theorem :: VALUED_1:23
for s, f being Function
for n being Element of NAT holds Shift ((f * s),n) = f * (Shift (s,n))
proof end;

theorem :: VALUED_1:24
for n being Element of NAT
for I, J being Function holds Shift ((I +* J),n) = (Shift (I,n)) +* (Shift (J,n))
proof end;

theorem Th25: :: VALUED_1:25
for p being Function
for k, il being Element of NAT st il in dom p holds
il + k in dom (Shift (p,k))
proof end;

theorem Th26: :: VALUED_1:26
for p being Function
for k being Element of NAT holds rng (Shift (p,k)) c= rng p
proof end;

theorem :: VALUED_1:27
for p being Function st dom p c= NAT holds
for k being Element of NAT holds rng (Shift (p,k)) = rng p
proof end;

registration
let p be finite Function;
let k be Element of NAT ;
cluster Shift (p,k) -> finite ;
coherence
Shift (p,k) is finite
proof end;
end;

definition
let X be non empty ext-real-membered set ;
let s be sequence of X;
:: original: increasing
redefine attr s is increasing means :: VALUED_1:def 13
for n being Nat holds s . n < s . (n + 1);
compatibility
( s is increasing iff for n being Nat holds s . n < s . (n + 1) )
proof end;
:: original: decreasing
redefine attr s is decreasing means :: VALUED_1:def 14
for n being Nat holds s . n > s . (n + 1);
compatibility
( s is decreasing iff for n being Nat holds s . n > s . (n + 1) )
proof end;
:: original: non-decreasing
redefine attr s is non-decreasing means :: VALUED_1:def 15
for n being Nat holds s . n <= s . (n + 1);
compatibility
( s is non-decreasing iff for n being Nat holds s . n <= s . (n + 1) )
proof end;
:: original: non-increasing
redefine attr s is non-increasing means :: VALUED_1:def 16
for n being Nat holds s . n >= s . (n + 1);
compatibility
( s is non-increasing iff for n being Nat holds s . n >= s . (n + 1) )
proof end;
end;

:: deftheorem defines increasing VALUED_1:def 13 :
for X being non empty ext-real-membered set
for s being sequence of X holds
( s is increasing iff for n being Nat holds s . n < s . (n + 1) );

:: deftheorem defines decreasing VALUED_1:def 14 :
for X being non empty ext-real-membered set
for s being sequence of X holds
( s is decreasing iff for n being Nat holds s . n > s . (n + 1) );

:: deftheorem defines non-decreasing VALUED_1:def 15 :
for X being non empty ext-real-membered set
for s being sequence of X holds
( s is non-decreasing iff for n being Nat holds s . n <= s . (n + 1) );

:: deftheorem defines non-increasing VALUED_1:def 16 :
for X being non empty ext-real-membered set
for s being sequence of X holds
( s is non-increasing iff for n being Nat holds s . n >= s . (n + 1) );

scheme :: VALUED_1:sch 1
SubSeqChoice{ F1() -> non empty set , F2() -> sequence of F1(), P1[ set ] } :
ex S1 being subsequence of F2() st
for n being Element of NAT holds P1[S1 . n]
provided
A1: for n being Element of NAT ex m being Element of NAT st
( n <= m & P1[F2() . m] )
proof end;

theorem :: VALUED_1:28
for k being Element of NAT
for F being NAT -defined Function holds dom F, dom (Shift (F,k)) are_equipotent
proof end;

theorem :: VALUED_1:29
for F being NAT -defined Function holds Shift (F,0) = F
proof end;

registration
let X be non empty set ;
let F be X -valued Function;
let k be Element of NAT ;
cluster Shift (F,k) -> X -valued ;
coherence
Shift (F,k) is X -valued
proof end;
end;

registration
cluster Relation-like NAT -defined Function-like non empty set ;
existence
ex b1 being Function st
( not b1 is empty & b1 is NAT -defined )
proof end;
end;

registration
let F be empty Function;
let k be Element of NAT ;
cluster Shift (F,k) -> empty ;
coherence
Shift (F,k) is empty
proof end;
end;

registration
let F be NAT -defined non empty Function;
let k be Element of NAT ;
cluster Shift (F,k) -> non empty ;
coherence
not Shift (F,k) is empty
proof end;
end;

theorem :: VALUED_1:30
for F being Function
for k being Element of NAT st k > 0 holds
not 0 in dom (Shift (F,k))
proof end;

registration
cluster Relation-like NAT -defined Function-like non empty finite set ;
existence
ex b1 being Function st
( b1 is NAT -defined & b1 is finite & not b1 is empty )
proof end;
end;

registration
let F be NAT -defined Relation;
cluster proj1 F -> natural-membered ;
coherence
dom F is natural-membered
proof end;
end;

definition
let F be NAT -defined non empty finite Function;
func LastLoc F -> Element of NAT equals :: VALUED_1:def 17
max (dom F);
coherence
max (dom F) is Element of NAT
by ORDINAL1:def 13;
end;

:: deftheorem defines LastLoc VALUED_1:def 17 :
for F being NAT -defined non empty finite Function holds LastLoc F = max (dom F);

definition
let F be NAT -defined non empty finite Function;
func CutLastLoc F -> Function equals :: VALUED_1:def 18
F \ ((LastLoc F) .--> (F . (LastLoc F)));
coherence
F \ ((LastLoc F) .--> (F . (LastLoc F))) is Function
;
end;

:: deftheorem defines CutLastLoc VALUED_1:def 18 :
for F being NAT -defined non empty finite Function holds CutLastLoc F = F \ ((LastLoc F) .--> (F . (LastLoc F)));

registration
let F be NAT -defined non empty finite Function;
cluster CutLastLoc F -> NAT -defined finite ;
coherence
( CutLastLoc F is NAT -defined & CutLastLoc F is finite )
;
end;

theorem Th31: :: VALUED_1:31
for F being NAT -defined non empty finite Function holds LastLoc F in dom F by XXREAL_2:def 8;

theorem :: VALUED_1:32
for F, G being NAT -defined non empty finite Function st F c= G holds
LastLoc F <= LastLoc G by RELAT_1:25, XXREAL_2:59;

theorem :: VALUED_1:33
for F being NAT -defined non empty finite Function
for l being Element of NAT st l in dom F holds
l <= LastLoc F by XXREAL_2:def 8;

definition
let F be NAT -defined non empty Function;
func FirstLoc F -> Element of NAT equals :: VALUED_1:def 19
min (dom F);
coherence
min (dom F) is Element of NAT
by ORDINAL1:def 13;
end;

:: deftheorem defines FirstLoc VALUED_1:def 19 :
for F being NAT -defined non empty Function holds FirstLoc F = min (dom F);

theorem :: VALUED_1:34
for F being NAT -defined non empty finite Function holds FirstLoc F in dom F
proof end;

theorem :: VALUED_1:35
for F, G being NAT -defined non empty finite Function st F c= G holds
FirstLoc G <= FirstLoc F
proof end;

theorem :: VALUED_1:36
for l1 being Element of NAT
for F being NAT -defined non empty finite Function st l1 in dom F holds
FirstLoc F <= l1
proof end;

theorem Th37: :: VALUED_1:37
for F being NAT -defined non empty finite Function holds dom (CutLastLoc F) = (dom F) \ {(LastLoc F)}
proof end;

theorem :: VALUED_1:38
for F being NAT -defined non empty finite Function holds dom F = (dom (CutLastLoc F)) \/ {(LastLoc F)}
proof end;

registration
cluster Relation-like NAT -defined Function-like non empty trivial finite set ;
existence
ex b1 being Function st
( not b1 is empty & b1 is trivial & b1 is NAT -defined & b1 is finite )
proof end;
end;

registration
let F be NAT -defined non empty trivial finite Function;
cluster CutLastLoc F -> empty ;
coherence
CutLastLoc F is empty
proof end;
end;

theorem :: VALUED_1:39
for F being NAT -defined non empty finite Function holds card (CutLastLoc F) = (card F) - 1
proof end;