:: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski

::

:: Received March 23, 1990

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

definition

let A be set ;

let 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)

end;
let 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;

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)

end;
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;

definition

let X be non empty set ;

let Z be 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)

end;
let Z be 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;

definition

let X be non empty set ;

let Z be 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)

end;
let Z be 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;

definition

let A be set ;

ex b_{1} being BinOp of (Funcs (A,REAL)) st

for f, g being Element of Funcs (A,REAL) holds b_{1} . (f,g) = addreal .: (f,g)

for b_{1}, b_{2} being BinOp of (Funcs (A,REAL)) st ( for f, g being Element of Funcs (A,REAL) holds b_{1} . (f,g) = addreal .: (f,g) ) & ( for f, g being Element of Funcs (A,REAL) holds b_{2} . (f,g) = addreal .: (f,g) ) holds

b_{1} = b_{2}

end;
func RealFuncAdd A -> BinOp of (Funcs (A,REAL)) means :Def1: :: FUNCSDOM:def 1

for f, g being Element of Funcs (A,REAL) holds it . (f,g) = addreal .: (f,g);

existence for f, g being Element of Funcs (A,REAL) holds it . (f,g) = addreal .: (f,g);

ex b

for f, g being Element of Funcs (A,REAL) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines RealFuncAdd FUNCSDOM:def 1 :

for A being set

for b_{2} being BinOp of (Funcs (A,REAL)) holds

( b_{2} = RealFuncAdd A iff for f, g being Element of Funcs (A,REAL) holds b_{2} . (f,g) = addreal .: (f,g) );

for A being set

for b

( b

definition

let A be set ;

ex b_{1} being BinOp of (Funcs (A,REAL)) st

for f, g being Element of Funcs (A,REAL) holds b_{1} . (f,g) = multreal .: (f,g)

for b_{1}, b_{2} being BinOp of (Funcs (A,REAL)) st ( for f, g being Element of Funcs (A,REAL) holds b_{1} . (f,g) = multreal .: (f,g) ) & ( for f, g being Element of Funcs (A,REAL) holds b_{2} . (f,g) = multreal .: (f,g) ) holds

b_{1} = b_{2}

end;
func RealFuncMult A -> BinOp of (Funcs (A,REAL)) means :Def2: :: FUNCSDOM:def 2

for f, g being Element of Funcs (A,REAL) holds it . (f,g) = multreal .: (f,g);

existence for f, g being Element of Funcs (A,REAL) holds it . (f,g) = multreal .: (f,g);

ex b

for f, g being Element of Funcs (A,REAL) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines RealFuncMult FUNCSDOM:def 2 :

for A being set

for b_{2} being BinOp of (Funcs (A,REAL)) holds

( b_{2} = RealFuncMult A iff for f, g being Element of Funcs (A,REAL) holds b_{2} . (f,g) = multreal .: (f,g) );

for A being set

for b

( b

definition

let A be set ;

ex b_{1} being Function of [:REAL,(Funcs (A,REAL)):],(Funcs (A,REAL)) st

for a being Real

for f being Element of Funcs (A,REAL) holds b_{1} . (a,f) = multreal [;] (a,f)

for b_{1}, b_{2} being Function of [:REAL,(Funcs (A,REAL)):],(Funcs (A,REAL)) st ( for a being Real

for f being Element of Funcs (A,REAL) holds b_{1} . (a,f) = multreal [;] (a,f) ) & ( for a being Real

for f being Element of Funcs (A,REAL) holds b_{2} . (a,f) = multreal [;] (a,f) ) holds

b_{1} = b_{2}

end;
func RealFuncExtMult A -> Function of [:REAL,(Funcs (A,REAL)):],(Funcs (A,REAL)) means :Def3: :: FUNCSDOM:def 3

for a being Real

for f being Element of Funcs (A,REAL) holds it . (a,f) = multreal [;] (a,f);

existence for a being Real

for f being Element of Funcs (A,REAL) holds it . (a,f) = multreal [;] (a,f);

ex b

for a being Real

for f being Element of Funcs (A,REAL) holds b

proof end;

uniqueness for b

for f being Element of Funcs (A,REAL) holds b

for f being Element of Funcs (A,REAL) holds b

b

proof end;

:: deftheorem Def3 defines RealFuncExtMult FUNCSDOM:def 3 :

for A being set

for b_{2} being Function of [:REAL,(Funcs (A,REAL)):],(Funcs (A,REAL)) holds

( b_{2} = RealFuncExtMult A iff for a being Real

for f being Element of Funcs (A,REAL) holds b_{2} . (a,f) = multreal [;] (a,f) );

for A being set

for b

( b

for f being Element of Funcs (A,REAL) holds b

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 Th1: :: FUNCSDOM:1

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) )

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 Th2: :: FUNCSDOM:2

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) )

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 Th4: :: FUNCSDOM:4

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) )

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 Th5: :: FUNCSDOM:5

for A being set

for f, g being Element of Funcs (A,REAL) holds (RealFuncAdd A) . (f,g) = (RealFuncAdd A) . (g,f)

for f, g being Element of Funcs (A,REAL) holds (RealFuncAdd A) . (f,g) = (RealFuncAdd A) . (g,f)

proof end;

theorem Th6: :: FUNCSDOM:6

for A being 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)

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 Th7: :: FUNCSDOM:7

for A being set

for f, g being Element of Funcs (A,REAL) holds (RealFuncMult A) . (f,g) = (RealFuncMult A) . (g,f)

for f, g being Element of Funcs (A,REAL) holds (RealFuncMult A) . (f,g) = (RealFuncMult A) . (g,f)

proof end;

theorem Th8: :: FUNCSDOM:8

for A being 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)

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 Th9: :: FUNCSDOM:9

for A being set

for f being Element of Funcs (A,REAL) holds (RealFuncMult A) . ((RealFuncUnit A),f) = f

for f being Element of Funcs (A,REAL) holds (RealFuncMult A) . ((RealFuncUnit A),f) = f

proof end;

theorem Th10: :: FUNCSDOM:10

for A being set

for f being Element of Funcs (A,REAL) holds (RealFuncAdd A) . ((RealFuncZero A),f) = f

for f being Element of Funcs (A,REAL) holds (RealFuncAdd A) . ((RealFuncZero A),f) = f

proof end;

theorem Th11: :: FUNCSDOM:11

for A being set

for f being Element of Funcs (A,REAL) holds (RealFuncAdd A) . (f,((RealFuncExtMult A) . [(- 1),f])) = RealFuncZero A

for f being Element of Funcs (A,REAL) holds (RealFuncAdd A) . (f,((RealFuncExtMult A) . [(- 1),f])) = RealFuncZero A

proof end;

theorem Th13: :: FUNCSDOM:13

for a, b being Real

for A being set

for f being Element of Funcs (A,REAL) holds (RealFuncExtMult A) . (a,((RealFuncExtMult A) . (b,f))) = (RealFuncExtMult A) . ((a * b),f)

for A being set

for f being Element of Funcs (A,REAL) holds (RealFuncExtMult A) . (a,((RealFuncExtMult A) . (b,f))) = (RealFuncExtMult A) . ((a * b),f)

proof end;

theorem Th14: :: FUNCSDOM:14

for a, b being Real

for A being set

for f being Element of Funcs (A,REAL) holds (RealFuncAdd A) . (((RealFuncExtMult A) . (a,f)),((RealFuncExtMult A) . (b,f))) = (RealFuncExtMult A) . ((a + b),f)

for A being set

for f being Element of Funcs (A,REAL) holds (RealFuncAdd A) . (((RealFuncExtMult A) . (a,f)),((RealFuncExtMult A) . (b,f))) = (RealFuncExtMult A) . ((a + b),f)

proof end;

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)))

proof end;

theorem Th15: :: FUNCSDOM:15

for A being 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)))

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 Th16: :: FUNCSDOM:16

for A being set

for f, g, h 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)))

for f, g, h 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 Th17: :: FUNCSDOM:17

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 ) ) ) )

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 Th18: :: FUNCSDOM:18

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 )

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:19

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 )

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 Th20: :: FUNCSDOM:20

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]))

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:21

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]))

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 Th22: :: FUNCSDOM:22

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])) ) )

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;

definition

let A be set ;

RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is strict RealLinearSpace

end;
func RealVectSpace A -> strict RealLinearSpace equals :: FUNCSDOM:def 6

RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #);

coherence RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #);

RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is strict RealLinearSpace

proof end;

:: deftheorem defines RealVectSpace FUNCSDOM:def 6 :

for A being set holds RealVectSpace A = RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #);

for A being set holds RealVectSpace A = RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #);

theorem :: FUNCSDOM:23

ex V being strict RealLinearSpace ex u, v being Element of V st

( ( for a, b being Real st (a * u) + (b * v) = 0. V holds

( a = 0 & b = 0 ) ) & ( for w being Element of V ex a, b being Real st w = (a * u) + (b * v) ) )

( ( for a, b being Real st (a * u) + (b * v) = 0. V holds

( a = 0 & b = 0 ) ) & ( for w being Element of V ex a, b being Real st w = (a * u) + (b * v) ) )

proof end;

definition

let A be non empty set ;

coherence

doubleLoopStr(# (Funcs (A,REAL)),(RealFuncAdd A),(RealFuncMult A),(RealFuncUnit A),(RealFuncZero A) #) is strict doubleLoopStr ;

;

end;
func RRing A -> strict doubleLoopStr equals :: FUNCSDOM:def 7

doubleLoopStr(# (Funcs (A,REAL)),(RealFuncAdd A),(RealFuncMult A),(RealFuncUnit A),(RealFuncZero A) #);

correctness doubleLoopStr(# (Funcs (A,REAL)),(RealFuncAdd A),(RealFuncMult A),(RealFuncUnit A),(RealFuncZero A) #);

coherence

doubleLoopStr(# (Funcs (A,REAL)),(RealFuncAdd A),(RealFuncMult A),(RealFuncUnit A),(RealFuncZero A) #) is strict doubleLoopStr ;

;

:: deftheorem defines RRing FUNCSDOM:def 7 :

for A being non empty set holds RRing A = doubleLoopStr(# (Funcs (A,REAL)),(RealFuncAdd A),(RealFuncMult A),(RealFuncUnit A),(RealFuncZero A) #);

for A being non empty set holds RRing A = doubleLoopStr(# (Funcs (A,REAL)),(RealFuncAdd A),(RealFuncMult A),(RealFuncUnit A),(RealFuncZero A) #);

registration
end;

Lm3: now :: thesis: for A being non empty set

for h, a being Element of (RRing A) st a = RealFuncUnit A holds

( h * a = h & a * h = h )

for h, a being Element of (RRing A) st a = RealFuncUnit A holds

( h * a = h & a * h = h )

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 ) )

reconsider g = h as Element of Funcs (A,REAL) ;

assume A1: a = RealFuncUnit A ; :: thesis: ( h * a = h & a * h = h )

hence h * a = (RealFuncMult A) . ((RealFuncUnit A),g) by Th7

.= h by Th9 ;

:: thesis: a * h = h

thus a * h = h by A1, Th9; :: thesis: verum

end;
( 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 ) )

reconsider g = h as Element of Funcs (A,REAL) ;

assume A1: a = RealFuncUnit A ; :: thesis: ( h * a = h & a * h = h )

hence h * a = (RealFuncMult A) . ((RealFuncUnit A),g) by Th7

.= h by Th9 ;

:: thesis: a * h = h

thus a * h = h by A1, Th9; :: thesis: verum

registration
end;

theorem Th25: :: FUNCSDOM:25

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) )

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

ex b_{1} being 1 -element doubleLoopStr st

( b_{1} is strict & b_{1} is Abelian & b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable & b_{1} is associative & b_{1} is commutative & b_{1} is right_unital & b_{1} is right-distributive )
end;

cluster non empty trivial V52() 1 -element right_complementable strict associative commutative right-distributive right_unital Abelian add-associative right_zeroed for doubleLoopStr ;

existence ex b

( b

proof end;

definition

mode Ring is non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;

end;
definition

attr c_{1} is strict ;

struct AlgebraStr -> doubleLoopStr , RLSStruct ;

aggr AlgebraStr(# carrier, multF, addF, Mult, OneF, ZeroF #) -> AlgebraStr ;

end;
struct AlgebraStr -> doubleLoopStr , RLSStruct ;

aggr AlgebraStr(# carrier, multF, addF, Mult, OneF, ZeroF #) -> AlgebraStr ;

definition

let A be set ;

coherence

AlgebraStr(# (Funcs (A,REAL)),(RealFuncMult A),(RealFuncAdd A),(RealFuncExtMult A),(RealFuncUnit A),(RealFuncZero A) #) is strict AlgebraStr ;

;

end;
func RAlgebra A -> strict AlgebraStr equals :: FUNCSDOM:def 8

AlgebraStr(# (Funcs (A,REAL)),(RealFuncMult A),(RealFuncAdd A),(RealFuncExtMult A),(RealFuncUnit A),(RealFuncZero A) #);

correctness AlgebraStr(# (Funcs (A,REAL)),(RealFuncMult A),(RealFuncAdd A),(RealFuncExtMult A),(RealFuncUnit A),(RealFuncZero A) #);

coherence

AlgebraStr(# (Funcs (A,REAL)),(RealFuncMult A),(RealFuncAdd A),(RealFuncExtMult A),(RealFuncUnit A),(RealFuncZero A) #) is strict AlgebraStr ;

;

:: deftheorem defines RAlgebra FUNCSDOM:def 8 :

for A being set holds RAlgebra A = AlgebraStr(# (Funcs (A,REAL)),(RealFuncMult A),(RealFuncAdd A),(RealFuncExtMult A),(RealFuncUnit A),(RealFuncZero A) #);

for A being set holds RAlgebra A = AlgebraStr(# (Funcs (A,REAL)),(RealFuncMult A),(RealFuncAdd A),(RealFuncExtMult A),(RealFuncUnit A),(RealFuncZero A) #);

Lm4: now :: thesis: for A being non empty set

for x, e being Element of (RAlgebra A) st e = RealFuncUnit A holds

( x * e = x & e * x = x )

for x, e being Element of (RAlgebra A) st e = RealFuncUnit A holds

( x * e = x & e * x = x )

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 ) )

reconsider f = x as Element of Funcs (A,REAL) ;

assume A1: e = RealFuncUnit A ; :: thesis: ( x * e = x & e * x = x )

hence x * e = (RealFuncMult A) . ((RealFuncUnit A),f) by Th7

.= x by Th9 ;

:: thesis: e * x = x

thus e * x = x by A1, Th9; :: thesis: verum

end;
( 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 ) )

reconsider f = x as Element of Funcs (A,REAL) ;

assume A1: e = RealFuncUnit A ; :: thesis: ( x * e = x & e * x = x )

hence x * e = (RealFuncMult A) . ((RealFuncUnit A),f) by Th7

.= x by Th9 ;

:: thesis: e * x = x

thus e * x = x by A1, Th9; :: thesis: verum

definition

let IT be non empty AlgebraStr ;

end;
attr IT is vector-associative means :: FUNCSDOM:def 9

for x, y being Element of IT

for a being Real holds a * (x * y) = (a * x) * y;

for x, y being Element of IT

for a being Real holds a * (x * y) = (a * x) * y;

:: deftheorem defines vector-associative FUNCSDOM:def 9 :

for IT being non empty AlgebraStr holds

( IT is vector-associative iff for x, y being Element of IT

for a being Real holds a * (x * y) = (a * x) * y );

for IT being non empty AlgebraStr holds

( IT is vector-associative iff for x, y being Element of IT

for a being Real holds a * (x * y) = (a * x) * y );

registration
end;

registration

let A be set ;

( RAlgebra A is strict & RAlgebra A is Abelian & RAlgebra A is add-associative & RAlgebra A is right_zeroed & RAlgebra A is right_complementable & RAlgebra A is commutative & RAlgebra A is associative & RAlgebra A is right_unital & RAlgebra A is right-distributive & RAlgebra A is vector-associative & RAlgebra A is scalar-associative & RAlgebra A is vector-distributive & RAlgebra A is scalar-distributive )

end;
cluster RAlgebra A -> right_complementable associative commutative right-distributive right_unital Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative strict vector-associative ;

coherence ( RAlgebra A is strict & RAlgebra A is Abelian & RAlgebra A is add-associative & RAlgebra A is right_zeroed & RAlgebra A is right_complementable & RAlgebra A is commutative & RAlgebra A is associative & RAlgebra A is right_unital & RAlgebra A is right-distributive & RAlgebra A is vector-associative & RAlgebra A is scalar-associative & RAlgebra A is vector-distributive & RAlgebra A is scalar-distributive )

proof end;

registration

ex b_{1} being non empty AlgebraStr st

( b_{1} is strict & b_{1} is Abelian & b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable & b_{1} is commutative & b_{1} is associative & b_{1} is right_unital & b_{1} is right-distributive & b_{1} is vector-associative & b_{1} is scalar-associative & b_{1} is vector-distributive & b_{1} is scalar-distributive )
end;

cluster non empty right_complementable associative commutative right-distributive right_unital Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative strict vector-associative for AlgebraStr ;

existence ex b

( b

proof end;

definition

mode Algebra is non empty right_complementable associative commutative right-distributive right_unital Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative AlgebraStr ;

end;