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

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 omega -defined Function-like complex-valued finite FinSequence-like FinSubsequence-like for set ;

existence
ex b₁ being FinSequence st b₁ is complex-valued

proof end;

end;

:: move somewhere

registration

let r be Rational;

cluster |.r.| -> rational ;

coherence
|.r.| is rational

proof end;

end;

definition

let f1, f2 be complex-valued Function;
deffunc H₁( object ) -> 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 object st c in dom it holds
it . c = (f1 . c) + (f2 . c) ) );

existence
ex b₁ being Function st
( dom b₁ = (dom f1) /\ (dom f2) & ( for c being object st c in dom b₁ holds
b₁ . c = (f1 . c) + (f2 . c) ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = (dom f1) /\ (dom f2) & ( for c being object st c in dom b₁ holds
b₁ . c = (f1 . c) + (f2 . c) ) & dom b₂ = (dom f1) /\ (dom f2) & ( for c being object st c in dom b₂ holds
b₂ . c = (f1 . c) + (f2 . c) ) holds
b₁ = b₂

proof end;

commutativity
for b₁ being Function
for f1, f2 being complex-valued Function st dom b₁ = (dom f1) /\ (dom f2) & ( for c being object st c in dom b₁ holds
b₁ . c = (f1 . c) + (f2 . c) ) holds
( dom b₁ = (dom f2) /\ (dom f1) & ( for c being object st c in dom b₁ holds
b₁ . c = (f2 . c) + (f1 . c) ) ) ;

end;

:: deftheorem Def1 defines + VALUED_1:def 1 :
for f1, f2 being complex-valued Function
for b₃ being Function holds
( b₃ = f1 + f2 iff ( dom b₃ = (dom f1) /\ (dom f2) & ( for c being object st c in dom b₃ holds
b₃ . 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 RAT -valued Function;

cluster f1 + f2 -> RAT -valued ;

coherence
f1 + f2 is RAT -valued

proof end;

end;

registration

let f1, f2 be INT -valued Function;

cluster f1 + f2 -> INT -valued ;

coherence
f1 + f2 is INT -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 for PartFunc of C,COMPLEX;

coherence
for b₁ being PartFunc of C,COMPLEX st b₁ = f1 + f2 holds
b₁ 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 for PartFunc of C,REAL;

coherence
for b₁ being PartFunc of C,REAL st b₁ = f1 + f2 holds
b₁ 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 for PartFunc of C,RAT;

coherence
for b₁ being PartFunc of C,RAT st b₁ = f1 + f2 holds
b₁ 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 for PartFunc of C,INT;

coherence
for b₁ being PartFunc of C,INT st b₁ = f1 + f2 holds
b₁ 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 for PartFunc of C,NAT;

coherence
for b₁ being PartFunc of C,NAT st b₁ = f1 + f2 holds
b₁ 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;

definition

let f be complex-valued Function;
let r be Complex;
deffunc H₁( object ) -> set = r + (f . $1);

func r + f -> Function means :Def2: :: VALUED_1:def 2
( dom it = dom f & ( for c being object st c in dom it holds
it . c = r + (f . c) ) );

existence
ex b₁ being Function st
( dom b₁ = dom f & ( for c being object st c in dom b₁ holds
b₁ . c = r + (f . c) ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = dom f & ( for c being object st c in dom b₁ holds
b₁ . c = r + (f . c) ) & dom b₂ = dom f & ( for c being object st c in dom b₂ holds
b₂ . c = r + (f . c) ) holds
b₁ = b₂

proof end;

end;

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

notation

let f be complex-valued Function;
let r be Complex;
synonym f + r for r + f;

end;

registration

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

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;

cluster r + f -> real-valued ;

coherence
r + f is real-valued

proof end;

end;

registration

let f be RAT -valued Function;
let r be Rational;

cluster r + f -> RAT -valued ;

coherence
r + f is RAT -valued

proof end;

end;

registration

let f be INT -valued Function;
let r be Integer;

cluster r + f -> INT -valued ;

coherence
r + f is INT -valued

proof end;

end;

registration

let f be natural-valued Function;
let r be Nat;

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;
:: 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;
:: 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;
:: 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;
:: 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 Nat;
:: 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;

cluster r + f -> total for PartFunc of C,COMPLEX;

coherence
for b₁ being PartFunc of C,COMPLEX st b₁ = r + f holds
b₁ 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;

cluster r + f -> total for PartFunc of C,REAL;

coherence
for b₁ being PartFunc of C,REAL st b₁ = r + f holds
b₁ 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;

cluster r + f -> total for PartFunc of C,RAT;

coherence
for b₁ being PartFunc of C,RAT st b₁ = r + f holds
b₁ 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;

cluster r + f -> total for PartFunc of C,INT;

coherence
for b₁ being PartFunc of C,INT st b₁ = r + f holds
b₁ 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 Nat;

cluster r + f -> total for PartFunc of C,NAT;

coherence
for b₁ being PartFunc of C,NAT st b₁ = r + f holds
b₁ 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
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;

cluster r + f -> FinSequence-like ;

coherence
r + f is FinSequence-like

proof end;

end;

definition

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

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 holds f - r = (- r) + f;

theorem :: VALUED_1:3

for f being complex-valued Function
for r being Complex holds
( dom (f - r) = dom f & ( for c being object 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;

cluster f - r -> complex-valued ;

coherence
f - r is complex-valued ;

end;

registration

let f be real-valued Function;
let r be Real;

cluster f - r -> real-valued ;

coherence
f - r is real-valued ;

end;

registration

let f be RAT -valued Function;
let r be Rational;

cluster f - r -> RAT -valued ;

coherence
f - r is RAT -valued ;

end;

registration

let f be INT -valued Function;
let r be Integer;

cluster f - r -> INT -valued ;

coherence
f - r is INT -valued ;

end;

definition

let C be set ;
let D be complex-membered set ;
let f be PartFunc of C,D;
let r be Complex;
:: 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;
:: 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;
:: 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;
:: 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;

cluster f - r -> total for PartFunc of C,COMPLEX;

coherence
for b₁ being PartFunc of C,COMPLEX st b₁ = f - r holds
b₁ 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;

cluster f - r -> total for PartFunc of C,REAL;

coherence
for b₁ being PartFunc of C,REAL st b₁ = f - r holds
b₁ 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;

cluster f - r -> total for PartFunc of C,RAT;

coherence
for b₁ being PartFunc of C,RAT st b₁ = f - r holds
b₁ 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;

cluster f - r -> total for PartFunc of C,INT;

coherence
for b₁ being PartFunc of C,INT st b₁ = f - r holds
b₁ 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
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;

cluster f - r -> FinSequence-like ;

coherence
f - r is FinSequence-like ;

end;

definition

let f1, f2 be complex-valued Function;
deffunc H₁( object ) -> 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 object st c in dom it holds
it . c = (f1 . c) * (f2 . c) ) );

existence
ex b₁ being Function st
( dom b₁ = (dom f1) /\ (dom f2) & ( for c being object st c in dom b₁ holds
b₁ . c = (f1 . c) * (f2 . c) ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = (dom f1) /\ (dom f2) & ( for c being object st c in dom b₁ holds
b₁ . c = (f1 . c) * (f2 . c) ) & dom b₂ = (dom f1) /\ (dom f2) & ( for c being object st c in dom b₂ holds
b₂ . c = (f1 . c) * (f2 . c) ) holds
b₁ = b₂

proof end;

commutativity
for b₁ being Function
for f1, f2 being complex-valued Function st dom b₁ = (dom f1) /\ (dom f2) & ( for c being object st c in dom b₁ holds
b₁ . c = (f1 . c) * (f2 . c) ) holds
( dom b₁ = (dom f2) /\ (dom f1) & ( for c being object st c in dom b₁ holds
b₁ . c = (f2 . c) * (f1 . c) ) ) ;

end;

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

theorem :: VALUED_1:5

for f1, f2 being complex-valued Function
for c being object 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 RAT -valued Function;

cluster f1 (#) f2 -> RAT -valued ;

coherence
f1 (#) f2 is RAT -valued

proof end;

end;

registration

let f1, f2 be INT -valued Function;

cluster f1 (#) f2 -> INT -valued ;

coherence
f1 (#) f2 is INT -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 for PartFunc of C,COMPLEX;

coherence
for b₁ being PartFunc of C,COMPLEX st b₁ = f1 (#) f2 holds
b₁ 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 for PartFunc of C,REAL;

coherence
for b₁ being PartFunc of C,REAL st b₁ = f1 (#) f2 holds
b₁ 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 for PartFunc of C,RAT;

coherence
for b₁ being PartFunc of C,RAT st b₁ = f1 (#) f2 holds
b₁ 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 for PartFunc of C,INT;

coherence
for b₁ being PartFunc of C,INT st b₁ = f1 (#) f2 holds
b₁ 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 for PartFunc of C,NAT;

coherence
for b₁ being PartFunc of C,NAT st b₁ = f1 (#) f2 holds
b₁ 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;

definition

let f be complex-valued Function;
let r be Complex;
deffunc H₁( object ) -> set = r * (f . $1);

func r (#) f -> Function means :Def5: :: VALUED_1:def 5
( dom it = dom f & ( for c being object st c in dom it holds
it . c = r * (f . c) ) );

existence
ex b₁ being Function st
( dom b₁ = dom f & ( for c being object st c in dom b₁ holds
b₁ . c = r * (f . c) ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = dom f & ( for c being object st c in dom b₁ holds
b₁ . c = r * (f . c) ) & dom b₂ = dom f & ( for c being object st c in dom b₂ holds
b₂ . c = r * (f . c) ) holds
b₁ = b₂

proof end;

end;

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

notation

let f be complex-valued Function;
let r be Complex;
synonym f (#) r for r (#) f;

end;

theorem Th6: :: VALUED_1:6

for f being complex-valued Function
for r being Complex
for c being object holds (r (#) f) . c = r * (f . c)

proof end;

registration

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

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;

cluster r (#) f -> real-valued ;

coherence
r (#) f is real-valued

proof end;

end;

registration

let f be RAT -valued Function;
let r be Rational;

cluster r (#) f -> RAT -valued ;

coherence
r (#) f is RAT -valued

proof end;

end;

registration

let f be INT -valued Function;
let r be Integer;

cluster r (#) f -> INT -valued ;

coherence
r (#) f is INT -valued

proof end;

end;

registration

let f be natural-valued Function;
let r be Nat;

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;
:: 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;
:: 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;
:: 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;
:: 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 Nat;
:: 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;

cluster r (#) f -> total for PartFunc of C,COMPLEX;

coherence
for b₁ being PartFunc of C,COMPLEX st b₁ = r (#) f holds
b₁ 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;

cluster r (#) f -> total for PartFunc of C,REAL;

coherence
for b₁ being PartFunc of C,REAL st b₁ = r (#) f holds
b₁ 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;

cluster r (#) f -> total for PartFunc of C,RAT;

coherence
for b₁ being PartFunc of C,RAT st b₁ = r (#) f holds
b₁ 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;

cluster r (#) f -> total for PartFunc of C,INT;

coherence
for b₁ being PartFunc of C,INT st b₁ = r (#) f holds
b₁ 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 Nat;

cluster r (#) f -> total for PartFunc of C,NAT;

coherence
for b₁ being PartFunc of C,NAT st b₁ = r (#) f holds
b₁ 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
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;

cluster r (#) f -> FinSequence-like ;

coherence
r (#) f is FinSequence-like

proof end;

end;

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 b₁, b₂ being complex-valued Function st b₁ = (- 1) (#) b₂ holds
b₂ = (- 1) (#) b₁

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 object 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 object 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 RAT -valued Function;

cluster - f -> RAT -valued complex-valued ;

coherence
- f is RAT -valued ;

end;

registration

let f be INT -valued Function;

cluster - f -> INT -valued complex-valued ;

coherence
- f is INT -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 for PartFunc of C,COMPLEX;

coherence
for b₁ being PartFunc of C,COMPLEX st b₁ = - f holds
b₁ 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 for PartFunc of C,REAL;

coherence
for b₁ being PartFunc of C,REAL st b₁ = - f holds
b₁ 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 for PartFunc of C,RAT;

coherence
for b₁ being PartFunc of C,RAT st b₁ = - f holds
b₁ 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 for PartFunc of C,INT;

coherence
for b₁ being PartFunc of C,INT st b₁ = - f holds
b₁ is total ;

end;

registration

let f be complex-valued FinSequence;

cluster - f -> complex-valued FinSequence-like ;

coherence
- f is FinSequence-like ;

end;

definition

let f be complex-valued Function;
deffunc H₁( object ) -> object = (f . $1) " ;

func f " -> complex-valued Function means :Def7: :: VALUED_1:def 7
( dom it = dom f & ( for c being object st c in dom it holds
it . c = (f . c) " ) );

existence
ex b₁ being complex-valued Function st
( dom b₁ = dom f & ( for c being object st c in dom b₁ holds
b₁ . c = (f . c) " ) )

proof end;

uniqueness
for b₁, b₂ being complex-valued Function st dom b₁ = dom f & ( for c being object st c in dom b₁ holds
b₁ . c = (f . c) " ) & dom b₂ = dom f & ( for c being object st c in dom b₂ holds
b₂ . c = (f . c) " ) holds
b₁ = b₂

proof end;

involutiveness
for b₁, b₂ being complex-valued Function st dom b₁ = dom b₂ & ( for c being object st c in dom b₁ holds
b₁ . c = (b₂ . c) " ) holds
( dom b₂ = dom b₁ & ( for c being object st c in dom b₂ holds
b₂ . c = (b₁ . c) " ) )

proof end;

end;

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

::better name

theorem Th10: :: VALUED_1:10

for f being complex-valued Function
for c being object 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 RAT -valued Function;

cluster f " -> RAT -valued complex-valued ;

coherence
f " is RAT -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 for PartFunc of C,COMPLEX;

coherence
for b₁ being PartFunc of C,COMPLEX st b₁ = f " holds
b₁ 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 for PartFunc of C,REAL;

coherence
for b₁ being PartFunc of C,REAL st b₁ = f " holds
b₁ 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 for PartFunc of C,RAT;

coherence
for b₁ being PartFunc of C,RAT st b₁ = f " holds
b₁ 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;

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 object 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 RAT -valued Function;

cluster f ^2 -> RAT -valued ;

coherence
f ^2 is RAT -valued ;

end;

registration

let f be INT -valued Function;

cluster f ^2 -> INT -valued ;

coherence
f ^2 is INT -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 for PartFunc of C,COMPLEX;

coherence
for b₁ being PartFunc of C,COMPLEX st b₁ = f ^2 holds
b₁ 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 for PartFunc of C,REAL;

coherence
for b₁ being PartFunc of C,REAL st b₁ = f ^2 holds
b₁ 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 for PartFunc of C,RAT;

coherence
for b₁ being PartFunc of C,RAT st b₁ = f ^2 holds
b₁ 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 for PartFunc of C,INT;

coherence
for b₁ being PartFunc of C,INT st b₁ = f ^2 holds
b₁ 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 for PartFunc of C,NAT;

coherence
for b₁ being PartFunc of C,NAT st b₁ = f ^2 holds
b₁ is total ;

end;

registration

let f be complex-valued FinSequence;

cluster f ^2 -> FinSequence-like ;

coherence
f ^2 is FinSequence-like ;

end;

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 RAT -valued Function;

cluster f1 - f2 -> RAT -valued ;

coherence
f1 - f2 is RAT -valued ;

end;

registration

let f1, f2 be INT -valued Function;

cluster f1 - f2 -> INT -valued ;

coherence
f1 - f2 is INT -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 object 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 object 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 for PartFunc of C,COMPLEX;

coherence
for b₁ being PartFunc of C,COMPLEX st b₁ = f1 - f2 holds
b₁ is total by Lm3, PARTFUN1:def 2;

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 for PartFunc of C,REAL;

coherence
for b₁ being PartFunc of C,REAL st b₁ = f1 - f2 holds
b₁ is total by Lm3, PARTFUN1:def 2;

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 for PartFunc of C,RAT;

coherence
for b₁ being PartFunc of C,RAT st b₁ = f1 - f2 holds
b₁ is total by Lm3, PARTFUN1:def 2;

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 for PartFunc of C,INT;

coherence
for b₁ being PartFunc of C,INT st b₁ = f1 - f2 holds
b₁ is total by Lm3, PARTFUN1:def 2;

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;

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 object 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 RAT -valued Function;

cluster f1 /" f2 -> RAT -valued ;

coherence
f1 /" f2 is RAT -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 for PartFunc of C,COMPLEX;

coherence
for b₁ being PartFunc of C,COMPLEX st b₁ = f1 /" f2 holds
b₁ is total by Lm4, PARTFUN1:def 2;

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 for PartFunc of C,REAL;

coherence
for b₁ being PartFunc of C,REAL st b₁ = f1 /" f2 holds
b₁ is total by Lm4, PARTFUN1:def 2;

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 for PartFunc of C,RAT;

coherence
for b₁ being PartFunc of C,RAT st b₁ = f1 /" f2 holds
b₁ is total by Lm4, PARTFUN1:def 2;

end;

registration

let f1, f2 be complex-valued FinSequence;

cluster f1 /" f2 -> FinSequence-like ;

coherence
f1 /" f2 is FinSequence-like ;

end;

definition

let f be complex-valued Function;
deffunc H₁( object ) -> object = |.(f . $1).|;

func |.f.| -> real-valued Function means :Def11: :: VALUED_1:def 11
( dom it = dom f & ( for c being object st c in dom it holds
it . c = |.(f . c).| ) );

existence
ex b₁ being real-valued Function st
( dom b₁ = dom f & ( for c being object st c in dom b₁ holds
b₁ . c = |.(f . c).| ) )

proof end;

uniqueness
for b₁, b₂ being real-valued Function st dom b₁ = dom f & ( for c being object st c in dom b₁ holds
b₁ . c = |.(f . c).| ) & dom b₂ = dom f & ( for c being object st c in dom b₂ holds
b₂ . c = |.(f . c).| ) holds
b₁ = b₂

proof end;

projectivity
for b₁ being real-valued Function
for b₂ being complex-valued Function st dom b₁ = dom b₂ & ( for c being object st c in dom b₁ holds
b₁ . c = |.(b₂ . c).| ) holds
( dom b₁ = dom b₁ & ( for c being object st c in dom b₁ holds
b₁ . c = |.(b₁ . c).| ) )

proof end;

end;

:: deftheorem Def11 defines |. VALUED_1:def 11 :
for f being complex-valued Function
for b₂ being real-valued Function holds
( b₂ = |.f.| iff ( dom b₂ = dom f & ( for c being object st c in dom b₂ holds
b₂ . 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 object holds |.f.| . c = |.(f . c).|

proof end;

registration

let f be RAT -valued Function;

cluster |.f.| -> RAT -valued real-valued ;

coherence
|.f.| is RAT -valued

proof end;

end;

registration

let f be INT -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 for PartFunc of C,REAL;

coherence
for b₁ being PartFunc of C,REAL st b₁ = |.f.| holds
b₁ 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 for PartFunc of C,RAT;

coherence
for b₁ being PartFunc of C,RAT st b₁ = |.f.| holds
b₁ 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 for PartFunc of C,NAT;

coherence
for b₁ being PartFunc of C,NAT st b₁ = |.f.| holds
b₁ 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;

definition

let p be Function;
let k be Nat;

func Shift (p,k) -> Function means :Def12: :: VALUED_1:def 12
( dom it = { (m + k) where m is Nat : m in dom p } & ( for m being Nat st m in dom p holds
it . (m + k) = p . m ) );

existence
ex b₁ being Function st
( dom b₁ = { (m + k) where m is Nat : m in dom p } & ( for m being Nat st m in dom p holds
b₁ . (m + k) = p . m ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = { (m + k) where m is Nat : m in dom p } & ( for m being Nat st m in dom p holds
b₁ . (m + k) = p . m ) & dom b₂ = { (m + k) where m is Nat : m in dom p } & ( for m being Nat st m in dom p holds
b₂ . (m + k) = p . m ) holds
b₁ = b₂

proof end;

end;

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

registration

let p be Function;
let k be Nat;

cluster Shift (p,k) -> NAT -defined ;

coherence
Shift (p,k) is NAT -defined

proof end;

end;

theorem :: VALUED_1:20

for P, Q being Function
for k being Nat st P c= Q holds
Shift (P,k) c= Shift (Q,k)

proof end;

theorem :: VALUED_1:21

for n, m being Nat
for I being Function holds Shift ((Shift (I,m)),n) = Shift (I,(m + n))

proof end;

theorem :: VALUED_1:22

for s, f being Function
for n being Nat holds Shift ((f * s),n) = f * (Shift (s,n))

proof end;

theorem :: VALUED_1:23

for I, J being Function
for n being Nat holds Shift ((I +* J),n) = (Shift (I,n)) +* (Shift (J,n))

proof end;

:: from SCMPDS_4, 2008.03.16, A.T.

theorem Th24: :: VALUED_1:24

for p being Function
for k, il being Nat st il in dom p holds
il + k in dom (Shift (p,k))

proof end;

:: missing, 2008.03.16, A.T.

theorem Th25: :: VALUED_1:25

for p being Function
for k being Nat holds rng (Shift (p,k)) c= rng p

proof end;

theorem :: VALUED_1:26

for p being Function st dom p c= NAT holds
for k being Nat holds rng (Shift (p,k)) = rng p

proof end;

registration

let p be finite Function;
let k be 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) );

:: from KURATO_2, 2008.09.05, A.T.

scheme :: VALUED_1:sch 1
SubSeqChoice{ F₁() -> non empty set , F₂() -> sequence of F₁(), P₁[ set ] } :

ex S1 being subsequence of F₂() st
for n being Element of NAT holds P₁[S1 . n]

provided

A1: for n being Element of NAT ex m being Element of NAT st
( n <= m & P₁[F₂() . m] )

proof end;

:: from AMISTD_2, 2010.02.05, A.T.

theorem :: VALUED_1:27

for k being Nat
for F being NAT -defined Function holds dom F, dom (Shift (F,k)) are_equipotent

proof end;

registration

let F be NAT -defined Function;

reduce Shift (F,0) to F;

reducibility
Shift (F,0) = F

proof end;

end;

registration

let X be non empty set ;
let F be X -valued Function;
let k be 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 for set ;

existence
ex b₁ being Function st
( not b₁ is empty & b₁ is NAT -defined )

proof end;

end;

registration

let F be empty Function;
let k be 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 Nat;

cluster Shift (F,k) -> non empty ;

coherence
not Shift (F,k) is empty

proof end;

end;

theorem :: VALUED_1:28

canceled;

::$CT

theorem :: VALUED_1:29

for F being Function
for k being 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 for set ;

existence
ex b₁ being Function st
( b₁ is NAT -defined & b₁ is finite & not b₁ is empty )

proof end;

end;

registration

let F be NAT -defined Relation;

cluster dom F -> natural-membered ;

coherence
dom F is natural-membered ;

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

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 :: VALUED_1:30

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

theorem :: VALUED_1:31

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

theorem :: VALUED_1:32

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

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:33

for F being NAT -defined non empty finite Function holds FirstLoc F in dom F by XXREAL_2:def 7;

theorem :: VALUED_1:34

for F, G being NAT -defined non empty finite Function st F c= G holds
FirstLoc G <= FirstLoc F by RELAT_1:11, XXREAL_2:60;

theorem :: VALUED_1:35

for l1 being Element of NAT
for F being NAT -defined non empty finite Function st l1 in dom F holds
FirstLoc F <= l1 by XXREAL_2:def 7;

theorem Th35: :: VALUED_1:36

for F being NAT -defined non empty finite Function holds dom (CutLastLoc F) = (dom F) \ {(LastLoc F)}

proof end;

theorem :: VALUED_1:37

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 finite 1 -element for set ;

existence
ex b₁ being Function st
( b₁ is 1 -element & b₁ is NAT -defined & b₁ is finite )

proof end;

end;

registration

let F be NAT -defined finite 1 -element Function;

cluster CutLastLoc F -> empty ;

coherence
CutLastLoc F is empty

proof end;

end;

theorem Th37: :: VALUED_1:38

for F being NAT -defined non empty finite Function holds card (CutLastLoc F) = (card F) - 1

proof end;

registration

let X be set ;
let f be X -defined complex-valued Function;

cluster - f -> X -defined complex-valued ;

coherence
- f is X -defined

proof end;

cluster f " -> X -defined complex-valued ;

coherence
f " is X -defined

proof end;

cluster f ^2 -> X -defined ;

coherence
f ^2 is X -defined

proof end;

cluster |.f.| -> X -defined real-valued ;

coherence
|.f.| is X -defined

proof end;

end;

registration

let X be set ;

cluster Relation-like X -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued for set ;

existence
ex b₁ being X -defined natural-valued Function st b₁ is total

proof end;

end;

registration

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

cluster - f -> total complex-valued ;

coherence
- f is total

proof end;

cluster f " -> total complex-valued ;

coherence
f " is total

proof end;

cluster f ^2 -> total ;

coherence
f ^2 is total

proof end;

cluster |.f.| -> total real-valued ;

coherence
|.f.| is total

proof end;

end;

registration

let X be set ;
let f be X -defined complex-valued Function;
let r be Complex;

cluster r + f -> X -defined ;

coherence
r + f is X -defined

proof end;

cluster f - r -> X -defined ;

coherence
f - r is X -defined ;

cluster r (#) f -> X -defined ;

coherence
r (#) f is X -defined

proof end;

end;

registration

let X be set ;
let f be X -defined total complex-valued Function;
let r be Complex;

cluster r + f -> total ;

coherence
r + f is total

proof end;

cluster f - r -> total ;

coherence
f - r is total ;

cluster r (#) f -> total ;

coherence
r (#) f is total

proof end;

end;

registration

let X be set ;
let f1 be complex-valued Function;
let f2 be X -defined complex-valued Function;

cluster f1 + f2 -> X -defined ;

coherence
f1 + f2 is X -defined

proof end;

cluster f1 - f2 -> X -defined ;

coherence
f1 - f2 is X -defined ;

cluster f1 (#) f2 -> X -defined ;

coherence
f1 (#) f2 is X -defined

proof end;

cluster f1 /" f2 -> X -defined ;

coherence
f1 /" f2 is X -defined ;

end;

registration

let X be set ;
let f1, f2 be X -defined total complex-valued Function;

cluster f1 + f2 -> total ;

coherence
f1 + f2 is total

proof end;

cluster f1 - f2 -> total ;

coherence
f1 - f2 is total ;

cluster f1 (#) f2 -> total ;

coherence
f1 (#) f2 is total

proof end;

cluster f1 /" f2 -> total ;

coherence
f1 /" f2 is total ;

end;

registration

let X be non empty set ;
let F be NAT -defined X -valued non empty finite Function;

cluster CutLastLoc F -> X -valued ;

coherence
CutLastLoc F is X -valued ;

end;

theorem :: VALUED_1:39

for f being Function
for i, n being Nat st i in dom (Shift (f,n)) holds
ex j being Nat st
( j in dom f & i = j + n )

proof end;

:: from PNPROC_1, 2012.02.20, A.T.

registration

let p be FinSubsequence;
let i be Nat;

cluster Shift (p,i) -> FinSubsequence-like ;

coherence
Shift (p,i) is FinSubsequence-like

proof end;

end;

theorem Th39: :: VALUED_1:40

for i being Nat
for p being FinSequence holds dom (Shift (p,i)) = { j1 where j1 is Nat : ( i + 1 <= j1 & j1 <= i + (len p) ) }

proof end;

theorem Th40: :: VALUED_1:41

for i being Nat
for q being FinSubsequence ex ss being FinSubsequence st
( dom ss = dom q & rng ss = dom (Shift (q,i)) & ( for k being Element of NAT st k in dom q holds
ss . k = i + k ) & ss is one-to-one )

proof end;

Lm5: for i being Nat
for p being FinSequence ex fs being FinSequence st
( dom fs = dom p & rng fs = dom (Shift (p,i)) & ( for k being Element of NAT st k in dom p holds
fs . k = i + k ) & fs is one-to-one )

proof end;

theorem Th41: :: VALUED_1:42

for i being Nat
for q being FinSubsequence holds card q = card (Shift (q,i))

proof end;

theorem Th42: :: VALUED_1:43

for i being Nat
for p being FinSequence holds dom p = dom (Seq (Shift (p,i)))

proof end;

theorem Th43: :: VALUED_1:44

for i being Nat
for k being Element of NAT
for p being FinSequence st k in dom p holds
(Sgm (dom (Shift (p,i)))) . k = i + k

proof end;

theorem Th44: :: VALUED_1:45

for i being Nat
for k being Element of NAT
for p being FinSequence st k in dom p holds
(Seq (Shift (p,i))) . k = p . k

proof end;

theorem :: VALUED_1:46

for i being Nat
for p being FinSequence holds Seq (Shift (p,i)) = p

proof end;

Lm6: for j, k, l being Nat st ( ( 1 <= j & j <= l ) or ( l + 1 <= j & j <= l + k ) ) holds
( 1 <= j & j <= l + k )

proof end;

theorem Th46: :: VALUED_1:47

for p1, p2 being FinSequence holds dom (p1 \/ (Shift (p2,(len p1)))) = Seg ((len p1) + (len p2))

proof end;

theorem Th47: :: VALUED_1:48

for i being Nat
for p1 being FinSequence
for p2 being FinSubsequence st len p1 <= i holds
dom p1 misses dom (Shift (p2,i))

proof end;

theorem :: VALUED_1:49

for p1, p2 being FinSequence holds p1 ^ p2 = p1 \/ (Shift (p2,(len p1)))

proof end;

theorem :: VALUED_1:50

for i being Nat
for p1 being FinSequence
for p2 being FinSubsequence st i >= len p1 holds
p1 misses Shift (p2,i)

proof end;

theorem :: VALUED_1:51

for F being NAT -defined total Function
for p being NAT -defined Function
for n being Element of NAT st Shift (p,n) c= F holds
for i being Element of NAT st i in dom p holds
F . (n + i) = p . i

proof end;

theorem Th51: :: VALUED_1:52

for i being Nat
for p, q being FinSubsequence st q c= p holds
Shift (q,i) c= Shift (p,i)

proof end;

theorem :: VALUED_1:53

for p1, p2 being FinSequence holds Shift (p2,(len p1)) c= p1 ^ p2

proof end;

theorem Th53: :: VALUED_1:54

for i being Nat
for q1, q2 being FinSubsequence st dom q1 misses dom q2 holds
dom (Shift (q1,i)) misses dom (Shift (q2,i))

proof end;

theorem :: VALUED_1:55

for i being Nat
for q, q1, q2 being FinSubsequence st q = q1 \/ q2 & q1 misses q2 holds
(Shift (q1,i)) \/ (Shift (q2,i)) = Shift (q,i)

proof end;

theorem Th55: :: VALUED_1:56

for i being Nat
for q being FinSubsequence holds dom (Seq q) = dom (Seq (Shift (q,i)))

proof end;

theorem Th56: :: VALUED_1:57

for i being Nat
for k being Element of NAT
for q being FinSubsequence st k in dom (Seq q) holds
ex j being Element of NAT st
( j = (Sgm (dom q)) . k & (Sgm (dom (Shift (q,i)))) . k = i + j )

proof end;

theorem Th57: :: VALUED_1:58

for i being Nat
for k being Element of NAT
for q being FinSubsequence st k in dom (Seq q) holds
(Seq (Shift (q,i))) . k = (Seq q) . k

proof end;

theorem :: VALUED_1:59

for i being Nat
for q being FinSubsequence holds Seq q = Seq (Shift (q,i))

proof end;

theorem Th59: :: VALUED_1:60

for i being Nat
for k being Element of NAT
for q being FinSubsequence st dom q c= Seg k holds
dom (Shift (q,i)) c= Seg (i + k)

proof end;

theorem Th60: :: VALUED_1:61

for p being FinSequence
for q1, q2 being FinSubsequence st q1 c= p holds
ex ss being FinSubsequence st ss = q1 \/ (Shift (q2,(len p)))

proof end;

Lm7: for i being Nat
for p, q being FinSubsequence st q c= p holds
dom (Shift (q,i)) c= dom (Shift (p,i))

proof end;

Lm8: for p1, p2 being FinSequence
for q1, q2 being FinSubsequence st q1 c= p1 & q2 c= p2 holds
Sgm ((dom q1) \/ (dom (Shift (q2,(len p1))))) = (Sgm (dom q1)) ^ (Sgm (dom (Shift (q2,(len p1)))))

proof end;

theorem Th61: :: VALUED_1:62

for p1, p2 being FinSequence
for q1, q2 being FinSubsequence st q1 c= p1 & q2 c= p2 holds
ex ss being FinSubsequence st
( ss = q1 \/ (Shift (q2,(len p1))) & dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) )

proof end;

theorem Th62: :: VALUED_1:63

for p1, p2 being FinSequence
for q1, q2 being FinSubsequence st q1 c= p1 & q2 c= p2 holds
ex ss being FinSubsequence st
( ss = q1 \/ (Shift (q2,(len p1))) & dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) & Seq ss = (Seq q1) \/ (Shift ((Seq q2),(len (Seq q1)))) )

proof end;

theorem :: VALUED_1:64

for p1, p2 being FinSequence
for q1, q2 being FinSubsequence st q1 c= p1 & q2 c= p2 holds
ex ss being FinSubsequence st
( ss = q1 \/ (Shift (q2,(len p1))) & (Seq q1) ^ (Seq q2) = Seq ss )

proof end;

theorem :: VALUED_1:65

for F being NAT -defined non empty finite Function holds card (CutLastLoc F) = (card F) -' 1

proof end;

theorem :: VALUED_1:66

for F, G being NAT -defined non empty finite Function st dom F = dom G holds
LastLoc F = LastLoc G ;

theorem :: VALUED_1:67

for i being Nat
for x, y being set
for f being NAT -defined non empty finite Function holds Shift ((f +~ (x,y)),i) = (Shift (f,i)) +~ (x,y)

proof end;

theorem :: VALUED_1:68

for F, G being NAT -defined non empty finite Function st dom F c= dom G holds
LastLoc F <= LastLoc G by XXREAL_2:59;