environ
vocabularies HIDDEN, XBOOLE_0, BINOP_1, FUNCT_2, SUBSET_1, FUNCT_1, ZFMISC_1, NUMBERS, RELAT_1, FUNCOP_1, BINOP_2, REAL_1, CARD_1, ARYTM_3, RLVECT_1, ARYTM_1, STRUCT_0, ALGSTR_0, SUPINF_2, GROUP_1, MESFUNC1, VECTSP_1, LATTICES, TARSKI, FUNCSDOM, VALUED_1, VALUED_2, VALUED_0, FUNCT_7, FUNCT_4;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1, MEMBERED, FUNCT_1, FUNCT_2, BINOP_1, FUNCT_4, DOMAIN_1, FUNCOP_1, BINOP_2, XCMPLX_0, XREAL_0, VALUED_0, VALUED_1, VALUED_2, STRUCT_0, ALGSTR_0, RLVECT_1, REAL_1, GROUP_1, VECTSP_1, PARTFUN3;
definitions RLVECT_1, STRUCT_0, GROUP_1, VECTSP_1, ALGSTR_0, FUNCT_2, VALUED_2;
theorems FUNCT_2, FUNCOP_1, TARSKI, BINOP_2, STRUCT_0, XREAL_0, PARTFUN1, FUNCT_1, VALUED_1, ZFMISC_1, FUNCT_4, XBOOLE_1, RELAT_1;
schemes BINOP_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, NUMBERS, RLVECT_1, VECTSP_1, ALGSTR_0, BINOP_2, FUNCOP_1, FUNCT_3, XREAL_0, ORDINAL1, RELAT_1, VALUED_0, VALUED_1, STRUCT_0, PARTFUN3, MEMBERED;
constructors HIDDEN, BINOP_1, DOMAIN_1, FUNCOP_1, REAL_1, BINOP_2, VECTSP_1, RLVECT_1, FUNCT_3, RELSET_1, VALUED_2, VALUED_0, VALUED_1, NUMBERS, GROUP_1, PARTFUN3, FUNCT_4;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities RLVECT_1, STRUCT_0, BINOP_1, ALGSTR_0, FUNCOP_1;
expansions RLVECT_1, GROUP_1, BINOP_1, VECTSP_1, FUNCT_2;
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;
reconsider jj = 1 as Element of REAL by XREAL_0:def 1;
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 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])) ) )