begin
Lm1:
0 = - 0
;
begin
definition
let C be non
empty set ;
let f1,
f2 be
C -defined ExtREAL -valued Function;
deffunc H1(
Element of
C)
-> Element of
ExtREAL =
(f1 . $1) + (f2 . $1);
existence
ex b1 being PartFunc of C,ExtREAL st
( dom b1 = ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom b1 holds
b1 . c = (f1 . c) + (f2 . c) ) )
uniqueness
for b1, b2 being PartFunc of C,ExtREAL st dom b1 = ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom b1 holds
b1 . c = (f1 . c) + (f2 . c) ) & dom b2 = ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom b2 holds
b2 . c = (f1 . c) + (f2 . c) ) holds
b1 = b2
commutativity
for b1 being PartFunc of C,ExtREAL
for f1, f2 being C -defined ExtREAL -valued Function st dom b1 = ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom b1 holds
b1 . c = (f1 . c) + (f2 . c) ) holds
( dom b1 = ((dom f2) /\ (dom f1)) \ (((f2 " {-infty}) /\ (f1 " {+infty})) \/ ((f2 " {+infty}) /\ (f1 " {-infty}))) & ( for c being Element of C st c in dom b1 holds
b1 . c = (f2 . c) + (f1 . c) ) )
;
deffunc H2(
Element of
C)
-> Element of
ExtREAL =
(f1 . $1) - (f2 . $1);
existence
ex b1 being PartFunc of C,ExtREAL st
( dom b1 = ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom b1 holds
b1 . c = (f1 . c) - (f2 . c) ) )
uniqueness
for b1, b2 being PartFunc of C,ExtREAL st dom b1 = ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom b1 holds
b1 . c = (f1 . c) - (f2 . c) ) & dom b2 = ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom b2 holds
b2 . c = (f1 . c) - (f2 . c) ) holds
b1 = b2
deffunc H3(
Element of
C)
-> Element of
ExtREAL =
(f1 . $1) * (f2 . $1);
existence
ex b1 being PartFunc of C,ExtREAL st
( dom b1 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b1 holds
b1 . c = (f1 . c) * (f2 . c) ) )
uniqueness
for b1, b2 being PartFunc of C,ExtREAL st dom b1 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b1 holds
b1 . c = (f1 . c) * (f2 . c) ) & dom b2 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b2 holds
b2 . c = (f1 . c) * (f2 . c) ) holds
b1 = b2
commutativity
for b1 being PartFunc of C,ExtREAL
for f1, f2 being C -defined ExtREAL -valued Function st dom b1 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b1 holds
b1 . c = (f1 . c) * (f2 . c) ) holds
( dom b1 = (dom f2) /\ (dom f1) & ( for c being Element of C st c in dom b1 holds
b1 . c = (f2 . c) * (f1 . c) ) )
;
end;
begin
definition
let X be
set ;
let f be
PartFunc of
X,
ExtREAL;
let a be
ext-real number ;
less_domredefine func less_dom (
f,
a)
-> Subset of
X;
coherence
less_dom (f,a) is Subset of X
less_eq_domredefine func less_eq_dom (
f,
a)
-> Subset of
X;
coherence
less_eq_dom (f,a) is Subset of X
great_domredefine func great_dom (
f,
a)
-> Subset of
X;
coherence
great_dom (f,a) is Subset of X
great_eq_domredefine func great_eq_dom (
f,
a)
-> Subset of
X;
coherence
great_eq_dom (f,a) is Subset of X
eq_domredefine func eq_dom (
f,
a)
-> Subset of
X;
coherence
eq_dom (f,a) is Subset of X
end;
begin