:: FUNCSDOM semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let A, B be non empty set ;
let F be BinOp of Funcs A,B;
let f, g be Element of Funcs A,B;
:: original: .
redefine func F . f,g -> Element of Funcs A,B;
coherence
F . f,g is Element of Funcs A,B
proof end;
end;

definition
let A, B, C, D be non empty set ;
let F be Function of [:C,D:], Funcs A,B;
let cd be Element of [:C,D:];
:: original: .
redefine func F . cd -> Element of Funcs A,B;
coherence
F . cd is Element of Funcs A,B
proof end;
end;

definition
let A, B be non empty set ;
let f be Function of A,B;
func @ f -> Element of Funcs A,B equals :: FUNCSDOM:def 1
f;
coherence
f is Element of Funcs A,B
by FUNCT_2:11;
end;

:: deftheorem defines @ FUNCSDOM:def 1 :
for A, B being non empty set
for f being Function of A,B holds @ f = f;

definition
let X, Z be non empty set ;
let F be BinOp of X;
let f, g be Function of Z,X;
:: original: .:
redefine func F .: f,g -> Element of Funcs Z,X;
coherence
F .: f,g is Element of Funcs Z,X
proof end;
end;

definition
let X, Z be non empty set ;
let F be BinOp of X;
let a be Element of X;
let f be Function of Z,X;
:: original: [;]
redefine func F [;] a,f -> Element of Funcs Z,X;
coherence
F [;] a,f is Element of Funcs Z,X
proof end;
end;

definition
let A be non empty set ;
func RealFuncAdd A -> BinOp of Funcs A,REAL means :Def2: :: FUNCSDOM:def 2
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
proof end;
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
proof end;
end;

:: deftheorem Def2 defines RealFuncAdd FUNCSDOM:def 2 :
for A being non empty set
for b2 being BinOp of Funcs A,REAL holds
( b2 = RealFuncAdd A iff for f, g being Element of Funcs A,REAL holds b2 . f,g = addreal .: f,g );

definition
let A be non empty set ;
func RealFuncMult A -> BinOp of Funcs A,REAL means :Def3: :: FUNCSDOM:def 3
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
proof end;
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
proof end;
end;

:: deftheorem Def3 defines RealFuncMult FUNCSDOM:def 3 :
for A being non empty set
for b2 being BinOp of Funcs A,REAL holds
( b2 = RealFuncMult A iff for f, g being Element of Funcs A,REAL holds b2 . f,g = multreal .: f,g );

definition
let A be non empty set ;
func RealFuncExtMult A -> Function of [:REAL ,(Funcs A,REAL ):], Funcs A,REAL means :Def4: :: FUNCSDOM:def 4
for a being Real
for f being Element of Funcs A,REAL
for x being Element of A holds (it . [a,f]) . x = a * (f . x);
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
for x being Element of A holds (b1 . [a,f]) . x = a * (f . x)
proof end;
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
for x being Element of A holds (b1 . [a,f]) . x = a * (f . x) ) & ( for a being Real
for f being Element of Funcs A,REAL
for x being Element of A holds (b2 . [a,f]) . x = a * (f . x) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines RealFuncExtMult FUNCSDOM:def 4 :
for A being non empty set
for b2 being Function of [:REAL ,(Funcs A,REAL ):], Funcs A,REAL holds
( b2 = RealFuncExtMult A iff for a being Real
for f being Element of Funcs A,REAL
for x being Element of A holds (b2 . [a,f]) . x = a * (f . x) );

definition
let A be non empty set ;
func RealFuncZero A -> Element of Funcs A,REAL equals :: FUNCSDOM:def 5
A --> 0;
coherence
A --> 0 is Element of Funcs A,REAL
proof end;
end;

:: deftheorem defines RealFuncZero FUNCSDOM:def 5 :
for A being non empty set holds RealFuncZero A = A --> 0;

definition
let A be non empty set ;
func RealFuncUnit A -> Element of Funcs A,REAL equals :: FUNCSDOM:def 6
A --> 1;
coherence
A --> 1 is Element of Funcs A,REAL
proof end;
end;

:: deftheorem defines RealFuncUnit FUNCSDOM:def 6 :
for A being non empty set holds RealFuncUnit A = A --> 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
proof end;

theorem :: FUNCSDOM:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FUNCSDOM:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FUNCSDOM:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FUNCSDOM:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FUNCSDOM:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FUNCSDOM:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FUNCSDOM:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FUNCSDOM:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FUNCSDOM:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th10: :: FUNCSDOM:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for h, f, g being Element of Funcs A,REAL holds
( h = (RealFuncAdd A) . f,g iff for x being Element of A holds h . x = (f . x) + (g . x) )
proof end;

theorem Th11: :: FUNCSDOM:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for h, f, g being Element of Funcs A,REAL holds
( h = (RealFuncMult A) . f,g iff for x being Element of A holds h . x = (f . x) * (g . x) )
proof end;

theorem Th12: :: FUNCSDOM:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for x being Element of A holds (RealFuncUnit A) . x = 1 by FUNCOP_1:13;

theorem Th13: :: FUNCSDOM:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for x being Element of A holds (RealFuncZero A) . x = 0 by FUNCOP_1:13;

theorem :: FUNCSDOM:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set holds RealFuncZero A <> RealFuncUnit A
proof end;

theorem Th15: :: FUNCSDOM:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for h, f being Element of Funcs A,REAL
for a being Real holds
( h = (RealFuncExtMult A) . [a,f] iff for x being Element of A holds h . x = a * (f . x) )
proof end;

theorem Th16: :: FUNCSDOM:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for f, g being Element of Funcs A,REAL holds (RealFuncAdd A) . f,g = (RealFuncAdd A) . g,f
proof end;

theorem Th17: :: FUNCSDOM:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for f, g, h being Element of Funcs A,REAL holds (RealFuncAdd A) . f,((RealFuncAdd A) . g,h) = (RealFuncAdd A) . ((RealFuncAdd A) . f,g),h
proof end;

theorem Th18: :: FUNCSDOM:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for f, g being Element of Funcs A,REAL holds (RealFuncMult A) . f,g = (RealFuncMult A) . g,f
proof end;

theorem Th19: :: FUNCSDOM:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for f, g, h being Element of Funcs A,REAL holds (RealFuncMult A) . f,((RealFuncMult A) . g,h) = (RealFuncMult A) . ((RealFuncMult A) . f,g),h
proof end;

theorem Th20: :: FUNCSDOM:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for f being Element of Funcs A,REAL holds (RealFuncMult A) . (RealFuncUnit A),f = f
proof end;

theorem Th21: :: FUNCSDOM:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for f being Element of Funcs A,REAL holds (RealFuncAdd A) . (RealFuncZero A),f = f
proof end;

theorem Th22: :: FUNCSDOM:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for f being Element of Funcs A,REAL holds (RealFuncAdd A) . f,((RealFuncExtMult A) . [(- 1),f]) = RealFuncZero A
proof end;

theorem Th23: :: FUNCSDOM:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for f being Element of Funcs A,REAL holds (RealFuncExtMult A) . [1,f] = f
proof end;

theorem Th24: :: FUNCSDOM:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for f being Element of Funcs A,REAL
for a, b being Real holds (RealFuncExtMult A) . [a,((RealFuncExtMult A) . [b,f])] = (RealFuncExtMult A) . [(a * b),f]
proof end;

theorem Th25: :: FUNCSDOM:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for f being Element of Funcs A,REAL
for a, b being Real holds (RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,f]) = (RealFuncExtMult A) . [(a + b),f]
proof end;

Lm2: for A being non empty set
for f, g being Element of Funcs A,REAL
for a being Real holds (RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [a,g]) = (RealFuncExtMult A) . [a,((RealFuncAdd A) . f,g)]
proof end;

theorem Th26: :: FUNCSDOM:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for f, g, h being Element of Funcs A,REAL holds (RealFuncMult A) . f,((RealFuncAdd A) . g,h) = (RealFuncAdd A) . ((RealFuncMult A) . f,g),((RealFuncMult A) . f,h)
proof end;

theorem Th27: :: FUNCSDOM:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for f, g being Element of Funcs A,REAL
for a being Real holds (RealFuncMult A) . ((RealFuncExtMult A) . [a,f]),g = (RealFuncExtMult A) . [a,((RealFuncMult A) . f,g)]
proof end;

theorem Th28: :: FUNCSDOM:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) ) ) )
proof end;

theorem Th29: :: FUNCSDOM:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2 being set
for A being non empty set
for f, g being Element of Funcs A,REAL st x1 in A & x2 in A & x1 <> x2 & ( 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 ) ) ) holds
for a, b being Real st (RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]) = RealFuncZero A holds
( a = 0 & b = 0 )
proof end;

theorem :: FUNCSDOM:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2 being set
for A being non empty set st x1 in A & x2 in A & 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 )
proof end;

theorem Th31: :: FUNCSDOM:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2 being set
for A being non empty set
for f, g being Element of Funcs A,REAL st A = {x1,x2} & x1 <> x2 & ( 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 ) ) ) holds
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])
proof end;

theorem :: FUNCSDOM:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 h being Element of Funcs A,REAL ex a, b being Real st h = (RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])
proof end;

theorem Th33: :: FUNCSDOM:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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]) ) )
proof end;

theorem Th34: :: FUNCSDOM:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set holds RLSStruct(# (Funcs A,REAL ),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is RealLinearSpace
proof end;

definition
let A be non empty set ;
func RealVectSpace A -> strict RealLinearSpace equals :: FUNCSDOM:def 7
RLSStruct(# (Funcs A,REAL ),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #);
coherence
RLSStruct(# (Funcs A,REAL ),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is strict RealLinearSpace
by Th34;
end;

:: deftheorem defines RealVectSpace FUNCSDOM:def 7 :
for A being non empty set holds RealVectSpace A = RLSStruct(# (Funcs A,REAL ),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #);

Lm3: ex A being non empty set ex x1, x2 being set st
( A = {x1,x2} & x1 <> x2 )
proof end;

theorem :: FUNCSDOM:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FUNCSDOM:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FUNCSDOM:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
ex V being strict RealLinearSpace ex u, v being VECTOR of V st
( ( for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ) & ( for w being VECTOR of V ex a, b being Real st w = (a * u) + (b * v) ) )
proof end;

definition
let A be non empty set ;
canceled;
canceled;
canceled;
canceled;
func RRing A -> strict doubleLoopStr equals :: FUNCSDOM:def 12
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 :
for A being non empty set holds RRing A = doubleLoopStr(# (Funcs A,REAL ),(RealFuncAdd A),(RealFuncMult A),(RealFuncUnit A),(RealFuncZero A) #);

registration
let A be non empty set ;
cluster RRing A -> non empty strict ;
coherence
not RRing A is empty
proof end;
end;

Lm4: now
let A be non empty set ; :: thesis: for h, a being Element of (RRing A) st a = RealFuncUnit A holds
( h * a = h & a * h = h )

set FR = RRing A;
let h, a be Element of (RRing A); :: thesis: ( a = RealFuncUnit A implies ( h * a = h & a * h = h ) )
assume A1: a = RealFuncUnit A ; :: thesis: ( h * a = h & a * h = h )
reconsider g = h as Element of Funcs A,REAL ;
thus h * a = (RealFuncMult A) . h,a
.= (RealFuncMult A) . h,(RealFuncUnit A) by A1
.= (RealFuncMult A) . (RealFuncUnit A),g by Th18
.= g by Th20
.= h ; :: thesis: a * h = h
thus a * h = (RealFuncMult A) . a,h
.= (RealFuncMult A) . (RealFuncUnit A),h by A1
.= g by Th20
.= h ; :: thesis: verum
end;

registration
let A be non empty set ;
cluster RRing A -> non empty unital strict ;
coherence
RRing A is unital
proof end;
end;

theorem :: FUNCSDOM:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FUNCSDOM:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FUNCSDOM:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th41: :: FUNCSDOM:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set holds 1. (RRing A) = RealFuncUnit A
proof end;

theorem Th42: :: FUNCSDOM:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for x, y, z being Element of (RRing A) holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (RRing A)) = x & ex t being Element of (RRing A) st x + t = 0. (RRing A) & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (RRing A)) = x & (1. (RRing A)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
proof end;

registration
cluster non empty Abelian add-associative right_zeroed right_complementable associative commutative strict right-distributive right_unital doubleLoopStr ;
existence
ex b1 being non empty doubleLoopStr st
( b1 is strict & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is associative & b1 is commutative & b1 is right_unital & b1 is right-distributive )
proof end;
end;

definition
mode Ring is non empty Abelian add-associative right_zeroed right_complementable associative right_unital distributive left_unital doubleLoopStr ;
end;

theorem :: FUNCSDOM:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set holds RRing A is commutative Ring
proof end;

definition
attr c1 is strict;
struct AlgebraStr -> doubleLoopStr , RLSStruct ;
aggr AlgebraStr(# carrier, mult, add, Mult, unity, Zero #) -> AlgebraStr ;
end;

registration
cluster non empty AlgebraStr ;
existence
not for b1 being AlgebraStr holds b1 is empty
proof end;
end;

definition
let A be non empty set ;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
func RAlgebra A -> strict AlgebraStr equals :: FUNCSDOM:def 19
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 :
for A being non empty set holds RAlgebra A = AlgebraStr(# (Funcs A,REAL ),(RealFuncMult A),(RealFuncAdd A),(RealFuncExtMult A),(RealFuncUnit A),(RealFuncZero A) #);

registration
let A be non empty set ;
cluster RAlgebra A -> non empty strict ;
coherence
not RAlgebra A is empty
proof end;
end;

Lm5: now
let A be non empty set ; :: thesis: for x, e being Element of (RAlgebra A) st e = RealFuncUnit A holds
( x * e = x & e * x = x )

set F = RAlgebra A;
let x, e be Element of (RAlgebra A); :: thesis: ( e = RealFuncUnit A implies ( x * e = x & e * x = x ) )
assume A1: e = RealFuncUnit A ; :: thesis: ( x * e = x & e * x = x )
reconsider f = x as Element of Funcs A,REAL ;
thus x * e = the mult of (RAlgebra A) . x,e
.= (RealFuncMult A) . f,(RealFuncUnit A) by A1
.= (RealFuncMult A) . (RealFuncUnit A),f by Th18
.= x by Th20 ; :: thesis: e * x = x
thus e * x = the mult of (RAlgebra A) . e,x
.= (RealFuncMult A) . (RealFuncUnit A),f by A1
.= x by Th20 ; :: thesis: verum
end;

registration
let A be non empty set ;
cluster RAlgebra A -> non empty unital strict ;
coherence
RAlgebra A is unital
proof end;
end;

theorem Th44: :: FUNCSDOM:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set holds 1. (RAlgebra A) = RealFuncUnit A
proof end;

theorem :: FUNCSDOM:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FUNCSDOM:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FUNCSDOM:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FUNCSDOM:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th49: :: FUNCSDOM:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for x, y, z being Element of (RAlgebra A)
for a, b being Real holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (RAlgebra A)) = x & ex t being Element of (RAlgebra A) st x + t = 0. (RAlgebra A) & x * y = y * x & (x * y) * z = x * (y * z) & x * (1. (RAlgebra A)) = x & x * (y + z) = (x * y) + (x * z) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) )
proof end;

definition
let IT be non empty AlgebraStr ;
attr IT is Algebra-like means :Def20: :: FUNCSDOM:def 20
for x, y, z being Element of IT
for a, b being Real holds
( x * (1. IT) = x & x * (y + z) = (x * y) + (x * z) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) );
end;

:: deftheorem Def20 defines Algebra-like FUNCSDOM:def 20 :
for IT being non empty AlgebraStr holds
( IT is Algebra-like iff for x, y, z being Element of IT
for a, b being Real holds
( x * (1. IT) = x & x * (y + z) = (x * y) + (x * z) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) ) );

registration
cluster non empty Abelian add-associative right_zeroed right_complementable associative commutative strict Algebra-like AlgebraStr ;
existence
ex b1 being non empty AlgebraStr st
( b1 is strict & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is commutative & b1 is associative & b1 is Algebra-like )
proof end;
end;

definition
mode Algebra is non empty Abelian add-associative right_zeroed right_complementable associative commutative Algebra-like AlgebraStr ;
end;

theorem :: FUNCSDOM:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set holds RAlgebra A is Algebra
proof end;