:: VALUED_1 semantic presentation

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 complex-valued 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
f1 + f2 is total PartFunc of C, COMPLEX
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
f1 + f2 is total PartFunc of C, REAL
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
f1 + f2 is total PartFunc of C, RAT
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
f1 + f2 is total PartFunc of C, INT
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
f1 + f2 is total PartFunc of C, NAT
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 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
r + f is total PartFunc of C, COMPLEX
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
r + f is total PartFunc of C, REAL
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
r + f is total PartFunc of C, RAT
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
r + f is total PartFunc of C, INT
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
r + f is total PartFunc of C, NAT
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;

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
f - r is total PartFunc of C, COMPLEX
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 f - r -> total PartFunc of C, REAL ;
coherence
f - r is total PartFunc of C, REAL
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 f - r -> total PartFunc of C, RAT ;
coherence
f - r is total PartFunc of C, RAT
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 f - r -> total PartFunc of C, INT ;
coherence
f - r is total PartFunc of C, INT
proof end;
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;

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 ;