begin
:: deftheorem FUNCSDOM:def 1 :
canceled;
definition
let A be
set ;
func RealFuncAdd A -> BinOp of
Funcs A,
REAL means :
Def2:
for
f,
g being
Element of
Funcs A,
REAL holds
it . f,
g = addreal .: f,
g;
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;
:: deftheorem Def2 defines RealFuncAdd FUNCSDOM:def 2 :
definition
let A be non
empty set ;
func RealFuncMult A -> BinOp of
Funcs A,
REAL means :
Def3:
for
f,
g being
Element of
Funcs A,
REAL holds
it . f,
g = multreal .: f,
g;
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;
:: deftheorem Def3 defines RealFuncMult FUNCSDOM:def 3 :
definition
let A be
set ;
func RealFuncExtMult A -> Function of
[:REAL ,(Funcs A,REAL ):],
Funcs A,
REAL means :
Def4:
for
a being
Real for
f being
Element of
Funcs A,
REAL holds
it . a,
f = multreal [;] a,
f;
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;
:: deftheorem Def4 defines RealFuncExtMult FUNCSDOM:def 4 :
:: deftheorem defines RealFuncZero FUNCSDOM:def 5 :
:: deftheorem defines RealFuncUnit FUNCSDOM:def 6 :
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
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th10:
theorem Th11:
theorem
canceled;
theorem
canceled;
theorem
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
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 Th26:
theorem Th27:
theorem Th28:
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 Th29:
theorem
theorem Th31:
theorem
theorem Th33:
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]) ) )
:: deftheorem defines RealVectSpace FUNCSDOM:def 7 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
definition
let A be non
empty set ;
canceled;canceled;canceled;canceled;func RRing A -> strict doubleLoopStr equals
doubleLoopStr(#
(Funcs A,REAL ),
(RealFuncAdd A),
(RealFuncMult A),
(RealFuncUnit A),
(RealFuncZero A) #);
correctness
coherence
doubleLoopStr(# (Funcs A,REAL ),(RealFuncAdd A),(RealFuncMult A),(RealFuncUnit A),(RealFuncZero A) #) is strict doubleLoopStr ;
;
end;
:: deftheorem FUNCSDOM:def 8 :
canceled;
:: deftheorem FUNCSDOM:def 9 :
canceled;
:: deftheorem FUNCSDOM:def 10 :
canceled;
:: deftheorem FUNCSDOM:def 11 :
canceled;
:: deftheorem defines RRing FUNCSDOM:def 12 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th42:
theorem
definition
let A be non
empty set ;
canceled;canceled;canceled;canceled;canceled;canceled;func RAlgebra A -> strict AlgebraStr equals
AlgebraStr(#
(Funcs A,REAL ),
(RealFuncMult A),
(RealFuncAdd A),
(RealFuncExtMult A),
(RealFuncUnit A),
(RealFuncZero A) #);
correctness
coherence
AlgebraStr(# (Funcs A,REAL ),(RealFuncMult A),(RealFuncAdd A),(RealFuncExtMult A),(RealFuncUnit A),(RealFuncZero A) #) is strict AlgebraStr ;
;
end;
:: deftheorem FUNCSDOM:def 13 :
canceled;
:: deftheorem FUNCSDOM:def 14 :
canceled;
:: deftheorem FUNCSDOM:def 15 :
canceled;
:: deftheorem FUNCSDOM:def 16 :
canceled;
:: deftheorem FUNCSDOM:def 17 :
canceled;
:: deftheorem FUNCSDOM:def 18 :
canceled;
:: deftheorem defines RAlgebra FUNCSDOM:def 19 :
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th49:
:: deftheorem Def20 defines Algebra-like FUNCSDOM:def 20 :
Lm5:
for A being non empty set holds RAlgebra A is right_complementable
theorem