begin
definition
let A be
set ;
existence
ex b1 being BinOp of (Funcs (A,REAL)) st
for f, g being Element of Funcs (A,REAL) holds b1 . (f,g) = addreal .: (f,g)
uniqueness
for b1, b2 being BinOp of (Funcs (A,REAL)) st ( for f, g being Element of Funcs (A,REAL) holds b1 . (f,g) = addreal .: (f,g) ) & ( for f, g being Element of Funcs (A,REAL) holds b2 . (f,g) = addreal .: (f,g) ) holds
b1 = b2
end;
definition
let A be
set ;
existence
ex b1 being BinOp of (Funcs (A,REAL)) st
for f, g being Element of Funcs (A,REAL) holds b1 . (f,g) = multreal .: (f,g)
uniqueness
for b1, b2 being BinOp of (Funcs (A,REAL)) st ( for f, g being Element of Funcs (A,REAL) holds b1 . (f,g) = multreal .: (f,g) ) & ( for f, g being Element of Funcs (A,REAL) holds b2 . (f,g) = multreal .: (f,g) ) holds
b1 = b2
end;
definition
let A be
set ;
existence
ex b1 being Function of [:REAL,(Funcs (A,REAL)):],(Funcs (A,REAL)) st
for a being Real
for f being Element of Funcs (A,REAL) holds b1 . (a,f) = multreal [;] (a,f)
uniqueness
for b1, b2 being Function of [:REAL,(Funcs (A,REAL)):],(Funcs (A,REAL)) st ( for a being Real
for f being Element of Funcs (A,REAL) holds b1 . (a,f) = multreal [;] (a,f) ) & ( for a being Real
for f being Element of Funcs (A,REAL) holds b2 . (a,f) = multreal [;] (a,f) ) holds
b1 = b2
end;
Lm1:
for A, B being non empty set
for x being Element of A
for f being Function of A,B holds x in dom f
Lm2:
for a being Real
for A being set
for f, g being Element of Funcs (A,REAL) holds (RealFuncAdd A) . (((RealFuncExtMult A) . (a,f)),((RealFuncExtMult A) . (a,g))) = (RealFuncExtMult A) . (a,((RealFuncAdd A) . (f,g)))
theorem Th17:
for
x1 being
set for
A being non
empty set ex
f,
g being
Element of
Funcs (
A,
REAL) st
( ( for
z being
set st
z in A holds
( (
z = x1 implies
f . z = 1 ) & (
z <> x1 implies
f . z = 0 ) ) ) & ( for
z being
set st
z in A holds
( (
z = x1 implies
g . z = 0 ) & (
z <> x1 implies
g . z = 1 ) ) ) )
theorem Th22:
for
x1,
x2 being
set for
A being non
empty set st
A = {x1,x2} &
x1 <> x2 holds
ex
f,
g being
Element of
Funcs (
A,
REAL) st
( ( for
a,
b being
Real st
(RealFuncAdd A) . (
((RealFuncExtMult A) . [a,f]),
((RealFuncExtMult A) . [b,g]))
= RealFuncZero A holds
(
a = 0 &
b = 0 ) ) & ( for
h being
Element of
Funcs (
A,
REAL) ex
a,
b being
Real st
h = (RealFuncAdd A) . (
((RealFuncExtMult A) . [a,f]),
((RealFuncExtMult A) . [b,g])) ) )