:: FUNCSDOM semantic presentation 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 funcF . (f,g) -> Element of Funcs (A,B); coherence F . (f,g) is Element of Funcs (A,B) proof reconsider f = f, g = g as Element of Funcs (A,B) ; F . (f,g) is Element of Funcs (A,B) ; hence F . (f,g) is Element of Funcs (A,B) ; ::_thesis: verum 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 funcF . cd -> Element of Funcs (A,B); coherence F . cd is Element of Funcs (A,B) proof F . cd is Element of Funcs (A,B) ; hence F . cd is Element of Funcs (A,B) ; ::_thesis: verum end; 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 funcF .: (f,g) -> Element of Funcs (Z,X); coherence F .: (f,g) is Element of Funcs (Z,X) proof F .: (f,g) in Funcs (Z,X) by FUNCT_2:8; hence F .: (f,g) is Element of Funcs (Z,X) ; ::_thesis: verum end; 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 funcF [;] (a,f) -> Element of Funcs (Z,X); coherence F [;] (a,f) is Element of Funcs (Z,X) proof F [;] (a,f) in Funcs (Z,X) by FUNCT_2:8; hence F [;] (a,f) is Element of Funcs (Z,X) ; ::_thesis: verum end; end; definition let A be set ; 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 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 deffunc H1( Element of Funcs (A,REAL), Element of Funcs (A,REAL)) -> Element of Funcs (A,REAL) = addreal .: ($1,$2); consider F being BinOp of (Funcs (A,REAL)) such that A1: for x, y being Element of Funcs (A,REAL) holds F . (x,y) = H1(x,y) from BINOP_1:sch_4(); take F ; ::_thesis: for f, g being Element of Funcs (A,REAL) holds F . (f,g) = addreal .: (f,g) let f, g be Element of Funcs (A,REAL); ::_thesis: F . (f,g) = addreal .: (f,g) thus F . (f,g) = addreal .: (f,g) by A1; ::_thesis: verum 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 let it1, it2 be BinOp of (Funcs (A,REAL)); ::_thesis: ( ( for f, g being Element of Funcs (A,REAL) holds it1 . (f,g) = addreal .: (f,g) ) & ( for f, g being Element of Funcs (A,REAL) holds it2 . (f,g) = addreal .: (f,g) ) implies it1 = it2 ) assume that A2: for f, g being Element of Funcs (A,REAL) holds it1 . (f,g) = addreal .: (f,g) and A3: for f, g being Element of Funcs (A,REAL) holds it2 . (f,g) = addreal .: (f,g) ; ::_thesis: it1 = it2 now__::_thesis:_for_f,_g_being_Element_of_Funcs_(A,REAL)_holds_it1_._(f,g)_=_it2_._(f,g) let f, g be Element of Funcs (A,REAL); ::_thesis: it1 . (f,g) = it2 . (f,g) thus it1 . (f,g) = addreal .: (f,g) by A2 .= it2 . (f,g) by A3 ; ::_thesis: verum end; hence it1 = it2 by BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def1 defines RealFuncAdd FUNCSDOM:def_1_:_ for A being 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 set ; 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 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 deffunc H1( Element of Funcs (A,REAL), Element of Funcs (A,REAL)) -> Element of Funcs (A,REAL) = multreal .: ($1,$2); consider F being BinOp of (Funcs (A,REAL)) such that A1: for x, y being Element of Funcs (A,REAL) holds F . (x,y) = H1(x,y) from BINOP_1:sch_4(); take F ; ::_thesis: for f, g being Element of Funcs (A,REAL) holds F . (f,g) = multreal .: (f,g) let f, g be Element of Funcs (A,REAL); ::_thesis: F . (f,g) = multreal .: (f,g) thus F . (f,g) = multreal .: (f,g) by A1; ::_thesis: verum 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 let it1, it2 be BinOp of (Funcs (A,REAL)); ::_thesis: ( ( for f, g being Element of Funcs (A,REAL) holds it1 . (f,g) = multreal .: (f,g) ) & ( for f, g being Element of Funcs (A,REAL) holds it2 . (f,g) = multreal .: (f,g) ) implies it1 = it2 ) assume that A2: for f, g being Element of Funcs (A,REAL) holds it1 . (f,g) = multreal .: (f,g) and A3: for f, g being Element of Funcs (A,REAL) holds it2 . (f,g) = multreal .: (f,g) ; ::_thesis: it1 = it2 now__::_thesis:_for_f,_g_being_Element_of_Funcs_(A,REAL)_holds_it1_._(f,g)_=_it2_._(f,g) let f, g be Element of Funcs (A,REAL); ::_thesis: it1 . (f,g) = it2 . (f,g) thus it1 . (f,g) = multreal .: (f,g) by A2 .= it2 . (f,g) by A3 ; ::_thesis: verum end; hence it1 = it2 by BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def2 defines RealFuncMult FUNCSDOM:def_2_:_ for A being 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 set ; 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 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) proof deffunc H1( Element of REAL , Element of Funcs (A,REAL)) -> Element of Funcs (A,REAL) = multreal [;] ($1,$2); consider F being Function of [:REAL,(Funcs (A,REAL)):],(Funcs (A,REAL)) such that A1: for a being Element of REAL for f being Element of Funcs (A,REAL) holds F . (a,f) = H1(a,f) from BINOP_1:sch_4(); take F ; ::_thesis: for a being Real for f being Element of Funcs (A,REAL) holds F . (a,f) = multreal [;] (a,f) let a be Real; ::_thesis: for f being Element of Funcs (A,REAL) holds F . (a,f) = multreal [;] (a,f) let f be Element of Funcs (A,REAL); ::_thesis: F . (a,f) = multreal [;] (a,f) thus F . (a,f) = multreal [;] (a,f) by A1; ::_thesis: verum 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) 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 proof let it1, it2 be Function of [:REAL,(Funcs (A,REAL)):],(Funcs (A,REAL)); ::_thesis: ( ( for a being Real for f being Element of Funcs (A,REAL) holds it1 . (a,f) = multreal [;] (a,f) ) & ( for a being Real for f being Element of Funcs (A,REAL) holds it2 . (a,f) = multreal [;] (a,f) ) implies it1 = it2 ) assume that A2: for a being Real for f being Element of Funcs (A,REAL) holds it1 . (a,f) = multreal [;] (a,f) and A3: for a being Real for f being Element of Funcs (A,REAL) holds it2 . (a,f) = multreal [;] (a,f) ; ::_thesis: it1 = it2 now__::_thesis:_for_a_being_Real for_f_being_Element_of_Funcs_(A,REAL)_holds_it1_._(a,f)_=_it2_._(a,f) let a be Real; ::_thesis: for f being Element of Funcs (A,REAL) holds it1 . (a,f) = it2 . (a,f) let f be Element of Funcs (A,REAL); ::_thesis: it1 . (a,f) = it2 . (a,f) thus it1 . (a,f) = multreal [;] (a,f) by A2 .= it2 . (a,f) by A3 ; ::_thesis: verum end; hence it1 = it2 by BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def3 defines RealFuncExtMult FUNCSDOM:def_3_:_ for A being 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) holds b2 . (a,f) = multreal [;] (a,f) ); definition let A be set ; func RealFuncZero A -> Element of Funcs (A,REAL) equals :: FUNCSDOM:def 4 A --> 0; coherence A --> 0 is Element of Funcs (A,REAL) proof A --> 0 is Function of A,REAL by FUNCOP_1:45; hence A --> 0 is Element of Funcs (A,REAL) by FUNCT_2:8; ::_thesis: verum end; end; :: deftheorem defines RealFuncZero FUNCSDOM:def_4_:_ for A being set holds RealFuncZero A = A --> 0; definition let A be set ; func RealFuncUnit A -> Element of Funcs (A,REAL) equals :: FUNCSDOM:def 5 A --> 1; coherence A --> 1 is Element of Funcs (A,REAL) proof A --> 1 is Function of A,REAL by FUNCOP_1:45; hence A --> 1 is Element of Funcs (A,REAL) by FUNCT_2:8; ::_thesis: verum end; end; :: deftheorem defines RealFuncUnit FUNCSDOM:def_5_:_ for A being 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 let A, B be non empty set ; ::_thesis: for x being Element of A for f being Function of A,B holds x in dom f let x be Element of A; ::_thesis: for f being Function of A,B holds x in dom f let f be Function of A,B; ::_thesis: x in dom f x in A ; hence x in dom f by FUNCT_2:def_1; ::_thesis: verum 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) ) proof let A be non empty set ; ::_thesis: 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) ) let h, f, g be Element of Funcs (A,REAL); ::_thesis: ( h = (RealFuncAdd A) . (f,g) iff for x being Element of A holds h . x = (f . x) + (g . x) ) A1: now__::_thesis:_(_(_for_x_being_Element_of_A_holds_h_._x_=_(f_._x)_+_(g_._x)_)_implies_h_=_(RealFuncAdd_A)_._(f,g)_) assume A2: for x being Element of A holds h . x = (f . x) + (g . x) ; ::_thesis: h = (RealFuncAdd A) . (f,g) now__::_thesis:_for_x_being_Element_of_A_holds_((RealFuncAdd_A)_._(f,g))_._x_=_h_._x let x be Element of A; ::_thesis: ((RealFuncAdd A) . (f,g)) . x = h . x A3: x in dom (addreal .: (f,g)) by Lm1; thus ((RealFuncAdd A) . (f,g)) . x = (addreal .: (f,g)) . x by Def1 .= addreal . ((f . x),(g . x)) by A3, FUNCOP_1:22 .= (f . x) + (g . x) by BINOP_2:def_9 .= h . x by A2 ; ::_thesis: verum end; hence h = (RealFuncAdd A) . (f,g) by FUNCT_2:63; ::_thesis: verum end; now__::_thesis:_(_h_=_(RealFuncAdd_A)_._(f,g)_implies_for_x_being_Element_of_A_holds_h_._x_=_(f_._x)_+_(g_._x)_) assume A4: h = (RealFuncAdd A) . (f,g) ; ::_thesis: for x being Element of A holds h . x = (f . x) + (g . x) let x be Element of A; ::_thesis: h . x = (f . x) + (g . x) A5: x in dom (addreal .: (f,g)) by Lm1; thus h . x = (addreal .: (f,g)) . x by A4, Def1 .= addreal . ((f . x),(g . x)) by A5, FUNCOP_1:22 .= (f . x) + (g . x) by BINOP_2:def_9 ; ::_thesis: verum end; hence ( h = (RealFuncAdd A) . (f,g) iff for x being Element of A holds h . x = (f . x) + (g . x) ) by A1; ::_thesis: verum 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) ) proof let A be non empty set ; ::_thesis: 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) ) let h, f, g be Element of Funcs (A,REAL); ::_thesis: ( h = (RealFuncMult A) . (f,g) iff for x being Element of A holds h . x = (f . x) * (g . x) ) A1: now__::_thesis:_(_(_for_x_being_Element_of_A_holds_h_._x_=_(f_._x)_*_(g_._x)_)_implies_h_=_(RealFuncMult_A)_._(f,g)_) assume A2: for x being Element of A holds h . x = (f . x) * (g . x) ; ::_thesis: h = (RealFuncMult A) . (f,g) now__::_thesis:_for_x_being_Element_of_A_holds_((RealFuncMult_A)_._(f,g))_._x_=_h_._x let x be Element of A; ::_thesis: ((RealFuncMult A) . (f,g)) . x = h . x A3: x in dom (multreal .: (f,g)) by Lm1; thus ((RealFuncMult A) . (f,g)) . x = (multreal .: (f,g)) . x by Def2 .= multreal . ((f . x),(g . x)) by A3, FUNCOP_1:22 .= (f . x) * (g . x) by BINOP_2:def_11 .= h . x by A2 ; ::_thesis: verum end; hence h = (RealFuncMult A) . (f,g) by FUNCT_2:63; ::_thesis: verum end; now__::_thesis:_(_h_=_(RealFuncMult_A)_._(f,g)_implies_for_x_being_Element_of_A_holds_h_._x_=_(f_._x)_*_(g_._x)_) assume A4: h = (RealFuncMult A) . (f,g) ; ::_thesis: for x being Element of A holds h . x = (f . x) * (g . x) let x be Element of A; ::_thesis: h . x = (f . x) * (g . x) A5: x in dom (multreal .: (f,g)) by Lm1; thus h . x = (multreal .: (f,g)) . x by A4, Def2 .= multreal . ((f . x),(g . x)) by A5, FUNCOP_1:22 .= (f . x) * (g . x) by BINOP_2:def_11 ; ::_thesis: verum end; hence ( h = (RealFuncMult A) . (f,g) iff for x being Element of A holds h . x = (f . x) * (g . x) ) by A1; ::_thesis: verum end; theorem :: FUNCSDOM:3 for A being non empty set holds RealFuncZero A <> RealFuncUnit A proof let A be non empty set ; ::_thesis: RealFuncZero A <> RealFuncUnit A set a = the Element of A; (RealFuncZero A) . the Element of A = 0 by FUNCOP_1:7; hence RealFuncZero A <> RealFuncUnit A by FUNCOP_1:7; ::_thesis: verum 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) ) proof let A be non empty set ; ::_thesis: 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) ) let h, f be Element of Funcs (A,REAL); ::_thesis: for a being Real holds ( h = (RealFuncExtMult A) . [a,f] iff for x being Element of A holds h . x = a * (f . x) ) let a be Real; ::_thesis: ( h = (RealFuncExtMult A) . [a,f] iff for x being Element of A holds h . x = a * (f . x) ) thus ( h = (RealFuncExtMult A) . [a,f] implies for x being Element of A holds h . x = a * (f . x) ) ::_thesis: ( ( for x being Element of A holds h . x = a * (f . x) ) implies h = (RealFuncExtMult A) . [a,f] ) proof assume A1: h = (RealFuncExtMult A) . [a,f] ; ::_thesis: for x being Element of A holds h . x = a * (f . x) let x be Element of A; ::_thesis: h . x = a * (f . x) h = (RealFuncExtMult A) . (a,f) by A1; hence h . x = (multreal [;] (a,f)) . x by Def3 .= multreal . (a,(f . x)) by FUNCOP_1:53 .= a * (f . x) by BINOP_2:def_11 ; ::_thesis: verum end; now__::_thesis:_(_(_for_x_being_Element_of_A_holds_h_._x_=_a_*_(f_._x)_)_implies_h_=_(RealFuncExtMult_A)_._(a,f)_) assume A2: for x being Element of A holds h . x = a * (f . x) ; ::_thesis: h = (RealFuncExtMult A) . (a,f) for x being Element of A holds h . x = ((RealFuncExtMult A) . [a,f]) . x proof let x be Element of A; ::_thesis: h . x = ((RealFuncExtMult A) . [a,f]) . x A3: multreal [;] (a,f) = (RealFuncExtMult A) . (a,f) by Def3; thus h . x = a * (f . x) by A2 .= multreal . (a,(f . x)) by BINOP_2:def_11 .= ((RealFuncExtMult A) . [a,f]) . x by A3, FUNCOP_1:53 ; ::_thesis: verum end; hence h = (RealFuncExtMult A) . (a,f) by FUNCT_2:63; ::_thesis: verum end; hence ( ( for x being Element of A holds h . x = a * (f . x) ) implies h = (RealFuncExtMult A) . [a,f] ) ; ::_thesis: verum 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) proof let A be set ; ::_thesis: for f, g being Element of Funcs (A,REAL) holds (RealFuncAdd A) . (f,g) = (RealFuncAdd A) . (g,f) let f, g be Element of Funcs (A,REAL); ::_thesis: (RealFuncAdd A) . (f,g) = (RealFuncAdd A) . (g,f) thus (RealFuncAdd A) . (f,g) = addreal .: (f,g) by Def1 .= addreal .: (g,f) by FUNCOP_1:65 .= (RealFuncAdd A) . (g,f) by Def1 ; ::_thesis: verum 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) proof let A be set ; ::_thesis: 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) let f, g, h be Element of Funcs (A,REAL); ::_thesis: (RealFuncAdd A) . (f,((RealFuncAdd A) . (g,h))) = (RealFuncAdd A) . (((RealFuncAdd A) . (f,g)),h) thus (RealFuncAdd A) . (f,((RealFuncAdd A) . (g,h))) = (RealFuncAdd A) . (f,(addreal .: (g,h))) by Def1 .= addreal .: (f,(addreal .: (g,h))) by Def1 .= addreal .: ((addreal .: (f,g)),h) by FUNCOP_1:61 .= (RealFuncAdd A) . ((addreal .: (f,g)),h) by Def1 .= (RealFuncAdd A) . (((RealFuncAdd A) . (f,g)),h) by Def1 ; ::_thesis: verum 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) proof let A be set ; ::_thesis: for f, g being Element of Funcs (A,REAL) holds (RealFuncMult A) . (f,g) = (RealFuncMult A) . (g,f) let f, g be Element of Funcs (A,REAL); ::_thesis: (RealFuncMult A) . (f,g) = (RealFuncMult A) . (g,f) thus (RealFuncMult A) . (f,g) = multreal .: (f,g) by Def2 .= multreal .: (g,f) by FUNCOP_1:65 .= (RealFuncMult A) . (g,f) by Def2 ; ::_thesis: verum 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) proof let A be set ; ::_thesis: 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) let f, g, h be Element of Funcs (A,REAL); ::_thesis: (RealFuncMult A) . (f,((RealFuncMult A) . (g,h))) = (RealFuncMult A) . (((RealFuncMult A) . (f,g)),h) thus (RealFuncMult A) . (f,((RealFuncMult A) . (g,h))) = (RealFuncMult A) . (f,(multreal .: (g,h))) by Def2 .= multreal .: (f,(multreal .: (g,h))) by Def2 .= multreal .: ((multreal .: (f,g)),h) by FUNCOP_1:61 .= (RealFuncMult A) . ((multreal .: (f,g)),h) by Def2 .= (RealFuncMult A) . (((RealFuncMult A) . (f,g)),h) by Def2 ; ::_thesis: verum end; theorem Th9: :: FUNCSDOM:9 for A being set for f being Element of Funcs (A,REAL) holds (RealFuncMult A) . ((RealFuncUnit A),f) = f proof let A be set ; ::_thesis: for f being Element of Funcs (A,REAL) holds (RealFuncMult A) . ((RealFuncUnit A),f) = f let f be Element of Funcs (A,REAL); ::_thesis: (RealFuncMult A) . ((RealFuncUnit A),f) = f percases ( A = {} or A <> {} ) ; suppose A = {} ; ::_thesis: (RealFuncMult A) . ((RealFuncUnit A),f) = f then A1: f = {} ; thus (RealFuncMult A) . ((RealFuncUnit A),f) = multreal .: ((RealFuncUnit A),f) by Def2 .= f by A1 ; ::_thesis: verum end; suppose A <> {} ; ::_thesis: (RealFuncMult A) . ((RealFuncUnit A),f) = f then reconsider A = A as non empty set ; reconsider f = f as Element of Funcs (A,REAL) ; now__::_thesis:_for_x_being_Element_of_A_holds_((RealFuncMult_A)_._((RealFuncUnit_A),f))_._x_=_f_._x let x be Element of A; ::_thesis: ((RealFuncMult A) . ((RealFuncUnit A),f)) . x = f . x thus ((RealFuncMult A) . ((RealFuncUnit A),f)) . x = ((RealFuncUnit A) . x) * (f . x) by Th2 .= 1 * (f . x) by FUNCOP_1:7 .= f . x ; ::_thesis: verum end; hence (RealFuncMult A) . ((RealFuncUnit A),f) = f by FUNCT_2:63; ::_thesis: verum end; end; end; theorem Th10: :: FUNCSDOM:10 for A being set for f being Element of Funcs (A,REAL) holds (RealFuncAdd A) . ((RealFuncZero A),f) = f proof let A be set ; ::_thesis: for f being Element of Funcs (A,REAL) holds (RealFuncAdd A) . ((RealFuncZero A),f) = f let f be Element of Funcs (A,REAL); ::_thesis: (RealFuncAdd A) . ((RealFuncZero A),f) = f percases ( A = {} or A <> {} ) ; suppose A = {} ; ::_thesis: (RealFuncAdd A) . ((RealFuncZero A),f) = f then A1: f = {} ; thus (RealFuncAdd A) . ((RealFuncZero A),f) = addreal .: ((RealFuncZero A),f) by Def1 .= f by A1 ; ::_thesis: verum end; suppose A <> {} ; ::_thesis: (RealFuncAdd A) . ((RealFuncZero A),f) = f then reconsider A = A as non empty set ; reconsider f = f as Element of Funcs (A,REAL) ; now__::_thesis:_for_x_being_Element_of_A_holds_((RealFuncAdd_A)_._((RealFuncZero_A),f))_._x_=_f_._x let x be Element of A; ::_thesis: ((RealFuncAdd A) . ((RealFuncZero A),f)) . x = f . x thus ((RealFuncAdd A) . ((RealFuncZero A),f)) . x = ((RealFuncZero A) . x) + (f . x) by Th1 .= 0 + (f . x) by FUNCOP_1:7 .= f . x ; ::_thesis: verum end; hence (RealFuncAdd A) . ((RealFuncZero A),f) = f by FUNCT_2:63; ::_thesis: verum end; end; 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 proof let A be set ; ::_thesis: for f being Element of Funcs (A,REAL) holds (RealFuncAdd A) . (f,((RealFuncExtMult A) . [(- 1),f])) = RealFuncZero A let f be Element of Funcs (A,REAL); ::_thesis: (RealFuncAdd A) . (f,((RealFuncExtMult A) . [(- 1),f])) = RealFuncZero A percases ( A = {} or A <> {} ) ; supposeA1: A = {} ; ::_thesis: (RealFuncAdd A) . (f,((RealFuncExtMult A) . [(- 1),f])) = RealFuncZero A hence (RealFuncAdd A) . (f,((RealFuncExtMult A) . [(- 1),f])) = {} .= RealFuncZero A by A1 ; ::_thesis: verum end; suppose A <> {} ; ::_thesis: (RealFuncAdd A) . (f,((RealFuncExtMult A) . [(- 1),f])) = RealFuncZero A then reconsider A = A as non empty set ; reconsider f = f as Element of Funcs (A,REAL) ; now__::_thesis:_for_x_being_Element_of_A_holds_((RealFuncAdd_A)_._(f,((RealFuncExtMult_A)_._[(-_1),f])))_._x_=_(RealFuncZero_A)_._x let x be Element of A; ::_thesis: ((RealFuncAdd A) . (f,((RealFuncExtMult A) . [(- 1),f]))) . x = (RealFuncZero A) . x set y = f . x; thus ((RealFuncAdd A) . (f,((RealFuncExtMult A) . [(- 1),f]))) . x = (f . x) + (((RealFuncExtMult A) . [(- 1),f]) . x) by Th1 .= (f . x) + ((- 1) * (f . x)) by Th4 .= (RealFuncZero A) . x by FUNCOP_1:7 ; ::_thesis: verum end; hence (RealFuncAdd A) . (f,((RealFuncExtMult A) . [(- 1),f])) = RealFuncZero A by FUNCT_2:63; ::_thesis: verum end; end; end; theorem Th12: :: FUNCSDOM:12 for A being set for f being Element of Funcs (A,REAL) holds (RealFuncExtMult A) . (1,f) = f proof let A be set ; ::_thesis: for f being Element of Funcs (A,REAL) holds (RealFuncExtMult A) . (1,f) = f let f be Element of Funcs (A,REAL); ::_thesis: (RealFuncExtMult A) . (1,f) = f percases ( A = {} or A <> {} ) ; suppose A = {} ; ::_thesis: (RealFuncExtMult A) . (1,f) = f then A1: f = {} ; thus (RealFuncExtMult A) . (1,f) = multreal [;] (1,f) by Def3 .= f by A1 ; ::_thesis: verum end; suppose A <> {} ; ::_thesis: (RealFuncExtMult A) . (1,f) = f then reconsider A = A as non empty set ; reconsider f = f as Element of Funcs (A,REAL) ; reconsider g = (RealFuncExtMult A) . (1,f) as Element of Funcs (A,REAL) ; now__::_thesis:_for_x_being_Element_of_A_holds_g_._x_=_f_._x let x be Element of A; ::_thesis: g . x = f . x thus g . x = 1 * (f . x) by Th4 .= f . x ; ::_thesis: verum end; hence (RealFuncExtMult A) . (1,f) = f by FUNCT_2:63; ::_thesis: verum end; end; 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) proof let a, b be Real; ::_thesis: 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) let A be set ; ::_thesis: for f being Element of Funcs (A,REAL) holds (RealFuncExtMult A) . (a,((RealFuncExtMult A) . (b,f))) = (RealFuncExtMult A) . ((a * b),f) let f be Element of Funcs (A,REAL); ::_thesis: (RealFuncExtMult A) . (a,((RealFuncExtMult A) . (b,f))) = (RealFuncExtMult A) . ((a * b),f) percases ( A = {} or A <> {} ) ; supposeA1: A = {} ; ::_thesis: (RealFuncExtMult A) . (a,((RealFuncExtMult A) . (b,f))) = (RealFuncExtMult A) . ((a * b),f) (RealFuncExtMult A) . (b,f) = multreal [;] (b,f) by Def3; hence (RealFuncExtMult A) . (a,((RealFuncExtMult A) . (b,f))) = multreal [;] (a,(multreal [;] (b,f))) by Def3 .= multreal [;] ((a * b),f) by A1 .= (RealFuncExtMult A) . ((a * b),f) by Def3 ; ::_thesis: verum end; suppose A <> {} ; ::_thesis: (RealFuncExtMult A) . (a,((RealFuncExtMult A) . (b,f))) = (RealFuncExtMult A) . ((a * b),f) then reconsider A = A as non empty set ; reconsider f = f as Element of Funcs (A,REAL) ; now__::_thesis:_for_x_being_Element_of_A_holds_((RealFuncExtMult_A)_._[a,((RealFuncExtMult_A)_._[b,f])])_._x_=_((RealFuncExtMult_A)_._[(a_*_b),f])_._x let x be Element of A; ::_thesis: ((RealFuncExtMult A) . [a,((RealFuncExtMult A) . [b,f])]) . x = ((RealFuncExtMult A) . [(a * b),f]) . x thus ((RealFuncExtMult A) . [a,((RealFuncExtMult A) . [b,f])]) . x = a * (((RealFuncExtMult A) . [b,f]) . x) by Th4 .= a * (b * (f . x)) by Th4 .= (a * b) * (f . x) .= ((RealFuncExtMult A) . [(a * b),f]) . x by Th4 ; ::_thesis: verum end; hence (RealFuncExtMult A) . (a,((RealFuncExtMult A) . (b,f))) = (RealFuncExtMult A) . ((a * b),f) by FUNCT_2:63; ::_thesis: verum end; end; 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) proof let a, b be Real; ::_thesis: 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) let A be set ; ::_thesis: for f being Element of Funcs (A,REAL) holds (RealFuncAdd A) . (((RealFuncExtMult A) . (a,f)),((RealFuncExtMult A) . (b,f))) = (RealFuncExtMult A) . ((a + b),f) let f be Element of Funcs (A,REAL); ::_thesis: (RealFuncAdd A) . (((RealFuncExtMult A) . (a,f)),((RealFuncExtMult A) . (b,f))) = (RealFuncExtMult A) . ((a + b),f) percases ( A = {} or A <> {} ) ; supposeA1: A = {} ; ::_thesis: (RealFuncAdd A) . (((RealFuncExtMult A) . (a,f)),((RealFuncExtMult A) . (b,f))) = (RealFuncExtMult A) . ((a + b),f) hence (RealFuncAdd A) . (((RealFuncExtMult A) . (a,f)),((RealFuncExtMult A) . (b,f))) = {} .= multreal [;] ((a + b),f) by A1 .= (RealFuncExtMult A) . ((a + b),f) by Def3 ; ::_thesis: verum end; suppose A <> {} ; ::_thesis: (RealFuncAdd A) . (((RealFuncExtMult A) . (a,f)),((RealFuncExtMult A) . (b,f))) = (RealFuncExtMult A) . ((a + b),f) then reconsider A = A as non empty set ; reconsider f = f as Element of Funcs (A,REAL) ; now__::_thesis:_for_x_being_Element_of_A_holds_((RealFuncAdd_A)_._(((RealFuncExtMult_A)_._[a,f]),((RealFuncExtMult_A)_._[b,f])))_._x_=_((RealFuncExtMult_A)_._[(a_+_b),f])_._x let x be Element of A; ::_thesis: ((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,f]))) . x = ((RealFuncExtMult A) . [(a + b),f]) . x thus ((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,f]))) . x = (((RealFuncExtMult A) . [a,f]) . x) + (((RealFuncExtMult A) . [b,f]) . x) by Th1 .= (a * (f . x)) + (((RealFuncExtMult A) . [b,f]) . x) by Th4 .= (a * (f . x)) + (b * (f . x)) by Th4 .= (a + b) * (f . x) .= ((RealFuncExtMult A) . [(a + b),f]) . x by Th4 ; ::_thesis: verum end; hence (RealFuncAdd A) . (((RealFuncExtMult A) . (a,f)),((RealFuncExtMult A) . (b,f))) = (RealFuncExtMult A) . ((a + b),f) by FUNCT_2:63; ::_thesis: verum end; end; 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 let a be Real; ::_thesis: 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))) let A be set ; ::_thesis: 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))) let f, g be Element of Funcs (A,REAL); ::_thesis: (RealFuncAdd A) . (((RealFuncExtMult A) . (a,f)),((RealFuncExtMult A) . (a,g))) = (RealFuncExtMult A) . (a,((RealFuncAdd A) . (f,g))) percases ( A = {} or A <> {} ) ; supposeA1: A = {} ; ::_thesis: (RealFuncAdd A) . (((RealFuncExtMult A) . (a,f)),((RealFuncExtMult A) . (a,g))) = (RealFuncExtMult A) . (a,((RealFuncAdd A) . (f,g))) hence (RealFuncAdd A) . (((RealFuncExtMult A) . (a,f)),((RealFuncExtMult A) . (a,g))) = {} .= multreal [;] (a,((RealFuncAdd A) . (f,g))) by A1 .= (RealFuncExtMult A) . (a,((RealFuncAdd A) . (f,g))) by Def3 ; ::_thesis: verum end; suppose A <> {} ; ::_thesis: (RealFuncAdd A) . (((RealFuncExtMult A) . (a,f)),((RealFuncExtMult A) . (a,g))) = (RealFuncExtMult A) . (a,((RealFuncAdd A) . (f,g))) then reconsider A = A as non empty set ; reconsider f = f, g = g as Element of Funcs (A,REAL) ; now__::_thesis:_for_x_being_Element_of_A_holds_((RealFuncAdd_A)_._(((RealFuncExtMult_A)_._[a,f]),((RealFuncExtMult_A)_._[a,g])))_._x_=_((RealFuncExtMult_A)_._[a,((RealFuncAdd_A)_._(f,g))])_._x let x be Element of A; ::_thesis: ((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [a,g]))) . x = ((RealFuncExtMult A) . [a,((RealFuncAdd A) . (f,g))]) . x thus ((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [a,g]))) . x = (((RealFuncExtMult A) . [a,f]) . x) + (((RealFuncExtMult A) . [a,g]) . x) by Th1 .= (a * (f . x)) + (((RealFuncExtMult A) . [a,g]) . x) by Th4 .= (a * (f . x)) + (a * (g . x)) by Th4 .= a * ((f . x) + (g . x)) .= a * (((RealFuncAdd A) . (f,g)) . x) by Th1 .= ((RealFuncExtMult A) . [a,((RealFuncAdd A) . (f,g))]) . x by Th4 ; ::_thesis: verum end; hence (RealFuncAdd A) . (((RealFuncExtMult A) . (a,f)),((RealFuncExtMult A) . (a,g))) = (RealFuncExtMult A) . (a,((RealFuncAdd A) . (f,g))) by FUNCT_2:63; ::_thesis: verum end; end; 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))) proof let A be set ; ::_thesis: 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))) let f, g, h be Element of Funcs (A,REAL); ::_thesis: (RealFuncMult A) . (f,((RealFuncAdd A) . (g,h))) = (RealFuncAdd A) . (((RealFuncMult A) . (f,g)),((RealFuncMult A) . (f,h))) A1: multreal .: (f,(addreal .: (g,h))) = addreal .: ((multreal .: (f,g)),(multreal .: (f,h))) proof let a be Element of A; :: according to FUNCT_2:def_8 ::_thesis: (multreal .: (f,(addreal .: (g,h)))) . a = (addreal .: ((multreal .: (f,g)),(multreal .: (f,h)))) . a percases ( A = {} or A <> {} ) ; suppose A = {} ; ::_thesis: (multreal .: (f,(addreal .: (g,h)))) . a = (addreal .: ((multreal .: (f,g)),(multreal .: (f,h)))) . a then f = {} ; hence (multreal .: (f,(addreal .: (g,h)))) . a = (addreal .: ((multreal .: (f,g)),(multreal .: (f,h)))) . a ; ::_thesis: verum end; suppose A <> {} ; ::_thesis: (multreal .: (f,(addreal .: (g,h)))) . a = (addreal .: ((multreal .: (f,g)),(multreal .: (f,h)))) . a then reconsider B = A as non empty set ; reconsider ff = f, gg = g, hh = h as Element of Funcs (B,REAL) ; reconsider b = a as Element of B ; thus (multreal .: (f,(addreal .: (g,h)))) . a = multreal . ((f . b),((addreal .: (g,h)) . b)) by FUNCOP_1:37 .= multreal . ((f . b),(addreal . ((g . b),(h . b)))) by FUNCOP_1:37 .= (ff . b) * (addreal . ((gg . b),(hh . b))) by BINOP_2:def_11 .= (ff . b) * ((gg . b) + (hh . b)) by BINOP_2:def_9 .= ((ff . b) * (gg . b)) + ((ff . b) * (hh . b)) .= ((ff . b) * (gg . b)) + (multreal . ((ff . b),(hh . b))) by BINOP_2:def_11 .= (multreal . ((ff . b),(gg . b))) + (multreal . ((ff . b),(hh . b))) by BINOP_2:def_11 .= addreal . ((multreal . ((f . a),(g . a))),(multreal . ((f . a),(h . a)))) by BINOP_2:def_9 .= addreal . ((multreal . ((f . a),(g . a))),((multreal .: (ff,h)) . a)) by FUNCOP_1:37 .= addreal . (((multreal .: (ff,g)) . a),((multreal .: (ff,h)) . a)) by FUNCOP_1:37 .= (addreal .: ((multreal .: (f,g)),(multreal .: (f,h)))) . a by FUNCOP_1:37 ; ::_thesis: verum end; end; end; thus (RealFuncMult A) . (f,((RealFuncAdd A) . (g,h))) = (RealFuncMult A) . (f,(addreal .: (g,h))) by Def1 .= multreal .: (f,(addreal .: (g,h))) by Def2 .= addreal .: ((multreal .: (f,g)),(multreal .: (f,h))) by A1 .= (RealFuncAdd A) . ((multreal .: (f,g)),(multreal .: (f,h))) by Def1 .= (RealFuncAdd A) . (((RealFuncMult A) . (f,g)),(multreal .: (f,h))) by Def2 .= (RealFuncAdd A) . (((RealFuncMult A) . (f,g)),((RealFuncMult A) . (f,h))) by Def2 ; ::_thesis: verum 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))) proof let A be set ; ::_thesis: 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))) let f, g, h be Element of Funcs (A,REAL); ::_thesis: for a being Real holds (RealFuncMult A) . (((RealFuncExtMult A) . (a,f)),g) = (RealFuncExtMult A) . (a,((RealFuncMult A) . (f,g))) let a be Real; ::_thesis: (RealFuncMult A) . (((RealFuncExtMult A) . (a,f)),g) = (RealFuncExtMult A) . (a,((RealFuncMult A) . (f,g))) thus (RealFuncMult A) . (((RealFuncExtMult A) . (a,f)),g) = (RealFuncMult A) . ((multreal [;] (a,f)),g) by Def3 .= multreal .: ((multreal [;] (a,f)),g) by Def2 .= multreal [;] (a,(multreal .: (f,g))) by FUNCOP_1:85 .= (RealFuncExtMult A) . (a,(multreal .: (f,g))) by Def3 .= (RealFuncExtMult A) . (a,((RealFuncMult A) . (f,g))) by Def2 ; ::_thesis: verum 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 ) ) ) ) proof let x1 be set ; ::_thesis: 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 ) ) ) ) let A be non empty set ; ::_thesis: 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 ) ) ) ) deffunc H1( set ) -> Element of NAT = 1; deffunc H2( set ) -> Element of NAT = 0 ; defpred S1[ set ] means $1 = x1; A1: for z being set st z in A holds ( ( S1[z] implies H1(z) in REAL ) & ( not S1[z] implies H2(z) in REAL ) ) ; consider f being Function of A,REAL such that A2: for z being set st z in A holds ( ( S1[z] implies f . z = H1(z) ) & ( not S1[z] implies f . z = H2(z) ) ) from FUNCT_2:sch_5(A1); A3: for z being set st z in A holds ( ( S1[z] implies H2(z) in REAL ) & ( not S1[z] implies H1(z) in REAL ) ) ; consider g being Function of A,REAL such that A4: for z being set st z in A holds ( ( S1[z] implies g . z = H2(z) ) & ( not S1[z] implies g . z = H1(z) ) ) from FUNCT_2:sch_5(A3); reconsider f = f, g = g as Element of Funcs (A,REAL) by FUNCT_2:8; take f ; ::_thesis: ex 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 ) ) ) ) take g ; ::_thesis: ( ( 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 ) ) ) ) thus ( ( 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 ) ) ) ) by A2, A4; ::_thesis: verum 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 ) proof let x1, x2 be set ; ::_thesis: 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 ) let A be non empty set ; ::_thesis: 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 ) let f, g be Element of Funcs (A,REAL); ::_thesis: ( 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 ) ) ) implies for a, b being Real st (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A holds ( a = 0 & b = 0 ) ) assume that A1: x1 in A and A2: x2 in A and A3: x1 <> x2 and A4: ( ( 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 ) ) ) ) ; ::_thesis: for a, b being Real st (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A holds ( a = 0 & b = 0 ) A5: ( f . x2 = 0 & g . x2 = 1 ) by A2, A3, A4; A6: ( f . x1 = 1 & g . x1 = 0 ) by A1, A4; let a, b be Real; ::_thesis: ( (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A implies ( a = 0 & b = 0 ) ) reconsider x1 = x1, x2 = x2 as Element of A by A1, A2; assume A7: (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A ; ::_thesis: ( a = 0 & b = 0 ) then A8: 0 = ((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))) . x2 by FUNCOP_1:7 .= (((RealFuncExtMult A) . [a,f]) . x2) + (((RealFuncExtMult A) . [b,g]) . x2) by Th1 .= (a * (f . x2)) + (((RealFuncExtMult A) . [b,g]) . x2) by Th4 .= 0 + (b * 1) by A5, Th4 .= b ; 0 = ((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))) . x1 by A7, FUNCOP_1:7 .= (((RealFuncExtMult A) . [a,f]) . x1) + (((RealFuncExtMult A) . [b,g]) . x1) by Th1 .= (a * (f . x1)) + (((RealFuncExtMult A) . [b,g]) . x1) by Th4 .= a + (b * 0) by A6, Th4 .= a ; hence ( a = 0 & b = 0 ) by A8; ::_thesis: verum 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 ) proof let x1, x2 be set ; ::_thesis: 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 ) let A be non empty set ; ::_thesis: ( x1 in A & x2 in A & x1 <> x2 implies 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 ) ) assume A1: ( x1 in A & x2 in A & x1 <> x2 ) ; ::_thesis: 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 ) consider f, g being Element of Funcs (A,REAL) such that A2: ( ( 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 ) ) ) ) by Th17; take f ; ::_thesis: ex 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 ) take g ; ::_thesis: for a, b being Real st (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A holds ( a = 0 & b = 0 ) let a, b be Real; ::_thesis: ( (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A implies ( a = 0 & b = 0 ) ) assume (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A ; ::_thesis: ( a = 0 & b = 0 ) hence ( a = 0 & b = 0 ) by A1, A2, Th18; ::_thesis: verum 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])) proof let x1, x2 be set ; ::_thesis: 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])) let A be non empty set ; ::_thesis: 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])) let f, g be Element of Funcs (A,REAL); ::_thesis: ( 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 ) ) ) implies 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])) ) assume that A1: A = {x1,x2} and A2: x1 <> x2 and A3: ( ( 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 ) ) ) ) ; ::_thesis: 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])) x2 in A by A1, TARSKI:def_2; then A4: ( f . x2 = 0 & g . x2 = 1 ) by A2, A3; x1 in A by A1, TARSKI:def_2; then A5: ( f . x1 = 1 & g . x1 = 0 ) by A3; let h be Element of Funcs (A,REAL); ::_thesis: ex a, b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) reconsider x1 = x1, x2 = x2 as Element of A by A1, TARSKI:def_2; take a = h . x1; ::_thesis: ex b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) take b = h . x2; ::_thesis: h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) now__::_thesis:_for_x_being_Element_of_A_holds_h_._x_=_((RealFuncAdd_A)_._(((RealFuncExtMult_A)_._[a,f]),((RealFuncExtMult_A)_._[b,g])))_._x let x be Element of A; ::_thesis: h . x = ((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))) . x A6: ( x = x1 or x = x2 ) by A1, TARSKI:def_2; A7: ((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))) . x2 = (((RealFuncExtMult A) . [a,f]) . x2) + (((RealFuncExtMult A) . [b,g]) . x2) by Th1 .= (a * (f . x2)) + (((RealFuncExtMult A) . [b,g]) . x2) by Th4 .= 0 + (b * 1) by A4, Th4 .= h . x2 ; ((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))) . x1 = (((RealFuncExtMult A) . [a,f]) . x1) + (((RealFuncExtMult A) . [b,g]) . x1) by Th1 .= (a * (f . x1)) + (((RealFuncExtMult A) . [b,g]) . x1) by Th4 .= a + (b * 0) by A5, Th4 .= h . x1 ; hence h . x = ((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))) . x by A6, A7; ::_thesis: verum end; hence h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) by FUNCT_2:63; ::_thesis: verum 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])) proof let x1, x2 be set ; ::_thesis: 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])) let A be non empty set ; ::_thesis: ( A = {x1,x2} & x1 <> x2 implies 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])) ) assume A1: ( A = {x1,x2} & x1 <> x2 ) ; ::_thesis: 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])) consider f, g being Element of Funcs (A,REAL) such that A2: ( ( 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 ) ) ) ) by Th17; take f ; ::_thesis: ex 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])) take g ; ::_thesis: 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])) let h be Element of Funcs (A,REAL); ::_thesis: ex a, b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) thus ex a, b being Real st h = (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) by A1, A2, Th20; ::_thesis: verum 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])) ) ) proof let x1, x2 be set ; ::_thesis: 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])) ) ) let A be non empty set ; ::_thesis: ( A = {x1,x2} & x1 <> x2 implies 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])) ) ) ) assume that A1: A = {x1,x2} and A2: x1 <> x2 ; ::_thesis: 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])) ) ) consider f, g being Element of Funcs (A,REAL) such that A3: ( ( 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 ) ) ) ) by Th17; take f ; ::_thesis: ex 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])) ) ) take g ; ::_thesis: ( ( 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])) ) ) ( x1 in A & x2 in A ) by A1, TARSKI:def_2; hence ( ( 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])) ) ) by A1, A2, A3, Th18, Th20; ::_thesis: verum end; definition let A be set ; 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) #) is strict RealLinearSpace proof set S = RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #); A1: RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is add-associative proof let u, v, w be Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #); :: according to RLVECT_1:def_3 ::_thesis: (u + v) + w = u + (v + w) thus (u + v) + w = u + (v + w) by Th6; ::_thesis: verum end; A2: RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is right_complementable proof let u be Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #); :: according to ALGSTR_0:def_16 ::_thesis: u is right_complementable reconsider u9 = u as Element of Funcs (A,REAL) ; reconsider w = (RealFuncExtMult A) . [(- 1),u9] as VECTOR of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) ; take w ; :: according to ALGSTR_0:def_11 ::_thesis: u + w = 0. RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) thus u + w = 0. RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) by Th11; ::_thesis: verum end; A3: ( RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is vector-distributive & RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is scalar-distributive & RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is scalar-associative & RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is scalar-unital ) proof thus for a being real number for v, w being Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) holds a * (v + w) = (a * v) + (a * w) :: according to RLVECT_1:def_5 ::_thesis: ( RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is scalar-distributive & RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is scalar-associative & RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is scalar-unital ) proof let a be real number ; ::_thesis: for v, w being Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) holds a * (v + w) = (a * v) + (a * w) reconsider a = a as Real by XREAL_0:def_1; for v, w being Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) holds a * (v + w) = (a * v) + (a * w) by Lm2; hence for v, w being Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) holds a * (v + w) = (a * v) + (a * w) ; ::_thesis: verum end; thus for a, b being real number for v being Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) holds (a + b) * v = (a * v) + (b * v) :: according to RLVECT_1:def_6 ::_thesis: ( RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is scalar-associative & RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is scalar-unital ) proof let a, b be real number ; ::_thesis: for v being Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) holds (a + b) * v = (a * v) + (b * v) reconsider a = a, b = b as Real by XREAL_0:def_1; for v being Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) holds (a + b) * v = (a * v) + (b * v) by Th14; hence for v being Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) holds (a + b) * v = (a * v) + (b * v) ; ::_thesis: verum end; thus for a, b being real number for v being Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) holds (a * b) * v = a * (b * v) :: according to RLVECT_1:def_7 ::_thesis: RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is scalar-unital proof let a, b be real number ; ::_thesis: for v being Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) holds (a * b) * v = a * (b * v) reconsider a = a, b = b as Real by XREAL_0:def_1; for v being Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) holds (a * b) * v = a * (b * v) by Th13; hence for v being Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) holds (a * b) * v = a * (b * v) ; ::_thesis: verum end; let v be Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #); :: according to RLVECT_1:def_8 ::_thesis: 1 * v = v thus 1 * v = v by Th12; ::_thesis: verum end; A4: RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is right_zeroed proof let u be Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #); :: according to RLVECT_1:def_4 ::_thesis: u + (0. RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #)) = u reconsider u9 = u as Element of Funcs (A,REAL) ; thus u + (0. RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #)) = (RealFuncAdd A) . ((RealFuncZero A),u9) by Th5 .= u by Th10 ; ::_thesis: verum end; RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is Abelian proof let u, v be Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #); :: according to RLVECT_1:def_2 ::_thesis: u + v = v + u thus u + v = v + u by Th5; ::_thesis: verum end; hence RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is strict RealLinearSpace by A1, A4, A2, A3; ::_thesis: verum end; end; :: deftheorem defines RealVectSpace FUNCSDOM:def_6_:_ 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) ) ) proof set A = {0,1}; take V = RealVectSpace {0,1}; ::_thesis: 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) ) ) consider f, g being Element of Funcs ({0,1},REAL) such that A1: for a, b being Real st (RealFuncAdd {0,1}) . (((RealFuncExtMult {0,1}) . [a,f]),((RealFuncExtMult {0,1}) . [b,g])) = RealFuncZero {0,1} holds ( a = 0 & b = 0 ) and A2: for h being Element of Funcs ({0,1},REAL) ex a, b being Real st h = (RealFuncAdd {0,1}) . (((RealFuncExtMult {0,1}) . [a,f]),((RealFuncExtMult {0,1}) . [b,g])) by Th22; reconsider u = f, v = g as Element of V ; take u ; ::_thesis: ex 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) ) ) take v ; ::_thesis: ( ( 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) ) ) thus for a, b being Real st (a * u) + (b * v) = 0. V holds ( a = 0 & b = 0 ) by A1; ::_thesis: for w being Element of V ex a, b being Real st w = (a * u) + (b * v) thus for w being Element of V ex a, b being Real st w = (a * u) + (b * v) ::_thesis: verum proof let w be Element of V; ::_thesis: ex a, b being Real st w = (a * u) + (b * v) reconsider h = w as Element of Funcs ({0,1},REAL) ; consider a, b being Real such that A3: h = (RealFuncAdd {0,1}) . (((RealFuncExtMult {0,1}) . [a,f]),((RealFuncExtMult {0,1}) . [b,g])) by A2; h = (a * u) + (b * v) by A3; hence ex a, b being Real st w = (a * u) + (b * v) ; ::_thesis: verum end; end; definition let A be non empty set ; func RRing A -> strict doubleLoopStr equals :: FUNCSDOM:def 7 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 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) #); registration let A be non empty set ; cluster RRing A -> non empty strict ; coherence not RRing A is empty ; 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_) 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; registration let A be non empty set ; cluster RRing A -> strict unital ; coherence RRing A is unital proof reconsider e = RealFuncUnit A as Element of (RRing A) ; take e ; :: according to GROUP_1:def_1 ::_thesis: for b1 being Element of the carrier of (RRing A) holds ( b1 * e = b1 & e * b1 = b1 ) thus for b1 being Element of the carrier of (RRing A) holds ( b1 * e = b1 & e * b1 = b1 ) by Lm3; ::_thesis: verum end; end; theorem :: FUNCSDOM:24 for A being non empty set holds 1. (RRing A) = RealFuncUnit A ; 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) ) proof let A be non empty set ; ::_thesis: 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) ) let x, y, z be Element of (RRing A); ::_thesis: ( 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) ) set IT = RRing A; reconsider f = x as Element of Funcs (A,REAL) ; thus x + y = y + x by Th5; ::_thesis: ( (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) ) thus (x + y) + z = x + (y + z) by Th6; ::_thesis: ( 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) ) thus x + (0. (RRing A)) = (RealFuncAdd A) . ((RealFuncZero A),f) by Th5 .= x by Th10 ; ::_thesis: ( 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) ) thus ex t being Element of (RRing A) st x + t = 0. (RRing A) ::_thesis: ( 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 set h = (RealFuncExtMult A) . [(- 1),f]; reconsider t = (RealFuncExtMult A) . [(- 1),f] as Element of (RRing A) ; take t ; ::_thesis: x + t = 0. (RRing A) thus x + t = 0. (RRing A) by Th11; ::_thesis: verum end; thus x * y = y * x by Th7; ::_thesis: ( (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) ) thus (x * y) * z = x * (y * z) by Th8; ::_thesis: ( x * (1. (RRing A)) = x & (1. (RRing A)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) ) thus x * (1. (RRing A)) = (RealFuncMult A) . ((RealFuncUnit A),f) by Th7 .= x by Th9 ; ::_thesis: ( (1. (RRing A)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) ) hence (1. (RRing A)) * x = x by Th7; ::_thesis: ( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) ) thus x * (y + z) = (x * y) + (x * z) by Th15; ::_thesis: (y + z) * x = (y * x) + (z * x) hence (y + z) * x = (x * y) + (x * z) by Th7 .= (y * x) + (x * z) by Th7 .= (y * x) + (z * x) by Th7 ; ::_thesis: verum end; registration 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 b1 being 1 -element 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 take L = Trivial-doubleLoopStr ; ::_thesis: ( L is strict & L is Abelian & L is add-associative & L is right_zeroed & L is right_complementable & L is associative & L is commutative & L is right_unital & L is right-distributive ) thus L is strict ; ::_thesis: ( L is Abelian & L is add-associative & L is right_zeroed & L is right_complementable & L is associative & L is commutative & L is right_unital & L is right-distributive ) thus L is Abelian ::_thesis: ( L is add-associative & L is right_zeroed & L is right_complementable & L is associative & L is commutative & L is right_unital & L is right-distributive ) proof let x be Element of L; :: according to RLVECT_1:def_2 ::_thesis: for b1 being Element of the carrier of L holds x + b1 = b1 + x thus for b1 being Element of the carrier of L holds x + b1 = b1 + x by STRUCT_0:def_10; ::_thesis: verum end; thus L is add-associative ::_thesis: ( L is right_zeroed & L is right_complementable & L is associative & L is commutative & L is right_unital & L is right-distributive ) proof let x be Element of L; :: according to RLVECT_1:def_3 ::_thesis: for b1, b2 being Element of the carrier of L holds (x + b1) + b2 = x + (b1 + b2) thus for b1, b2 being Element of the carrier of L holds (x + b1) + b2 = x + (b1 + b2) by STRUCT_0:def_10; ::_thesis: verum end; thus L is right_zeroed ::_thesis: ( L is right_complementable & L is associative & L is commutative & L is right_unital & L is right-distributive ) proof let x be Element of L; :: according to RLVECT_1:def_4 ::_thesis: x + (0. L) = x thus x + (0. L) = x by STRUCT_0:def_10; ::_thesis: verum end; thus L is right_complementable ::_thesis: ( L is associative & L is commutative & L is right_unital & L is right-distributive ) proof let x be Element of L; :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable take x ; :: according to ALGSTR_0:def_11 ::_thesis: x + x = 0. L thus x + x = 0. L by STRUCT_0:def_10; ::_thesis: verum end; thus L is associative ::_thesis: ( L is commutative & L is right_unital & L is right-distributive ) proof let x be Element of L; :: according to GROUP_1:def_3 ::_thesis: for b1, b2 being Element of the carrier of L holds (x * b1) * b2 = x * (b1 * b2) thus for b1, b2 being Element of the carrier of L holds (x * b1) * b2 = x * (b1 * b2) by STRUCT_0:def_10; ::_thesis: verum end; thus L is commutative ::_thesis: ( L is right_unital & L is right-distributive ) proof let x be Element of L; :: according to GROUP_1:def_12 ::_thesis: for b1 being Element of the carrier of L holds x * b1 = b1 * x thus for b1 being Element of the carrier of L holds x * b1 = b1 * x by STRUCT_0:def_10; ::_thesis: verum end; thus L is right_unital ::_thesis: L is right-distributive proof let x be Element of L; :: according to VECTSP_1:def_4 ::_thesis: x * (1. L) = x thus x * (1. L) = x by STRUCT_0:def_10; ::_thesis: verum end; let x be Element of L; :: according to VECTSP_1:def_2 ::_thesis: for b1, b2 being Element of the carrier of L holds x * (b1 + b2) = (x * b1) + (x * b2) thus for b1, b2 being Element of the carrier of L holds x * (b1 + b2) = (x * b1) + (x * b2) by STRUCT_0:def_10; ::_thesis: verum end; end; definition mode Ring is non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; end; theorem :: FUNCSDOM:26 for A being non empty set holds RRing A is commutative Ring proof let A be non empty set ; ::_thesis: RRing A is commutative Ring A1: RRing A is Abelian proof let x be Element of (RRing A); :: according to RLVECT_1:def_2 ::_thesis: for b1 being Element of the carrier of (RRing A) holds x + b1 = b1 + x thus for b1 being Element of the carrier of (RRing A) holds x + b1 = b1 + x by Th25; ::_thesis: verum end; A2: RRing A is add-associative proof let x be Element of (RRing A); :: according to RLVECT_1:def_3 ::_thesis: for b1, b2 being Element of the carrier of (RRing A) holds (x + b1) + b2 = x + (b1 + b2) thus for b1, b2 being Element of the carrier of (RRing A) holds (x + b1) + b2 = x + (b1 + b2) by Th25; ::_thesis: verum end; A3: RRing A is right_complementable proof let x be Element of (RRing A); :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable consider t being Element of (RRing A) such that A4: x + t = 0. (RRing A) by Th25; take t ; :: according to ALGSTR_0:def_11 ::_thesis: x + t = 0. (RRing A) thus x + t = 0. (RRing A) by A4; ::_thesis: verum end; A5: RRing A is right_zeroed proof let x be Element of (RRing A); :: according to RLVECT_1:def_4 ::_thesis: x + (0. (RRing A)) = x thus x + (0. (RRing A)) = x by Th25; ::_thesis: verum end; A6: RRing A is distributive proof let x be Element of (RRing A); :: according to VECTSP_1:def_7 ::_thesis: for b1, b2 being Element of the carrier of (RRing A) holds ( x * (b1 + b2) = (x * b1) + (x * b2) & (b1 + b2) * x = (b1 * x) + (b2 * x) ) thus for b1, b2 being Element of the carrier of (RRing A) holds ( x * (b1 + b2) = (x * b1) + (x * b2) & (b1 + b2) * x = (b1 * x) + (b2 * x) ) by Th25; ::_thesis: verum end; A7: RRing A is well-unital proof let x be Element of (RRing A); :: according to VECTSP_1:def_6 ::_thesis: ( x * (1. (RRing A)) = x & (1. (RRing A)) * x = x ) thus ( x * (1. (RRing A)) = x & (1. (RRing A)) * x = x ) by Th25; ::_thesis: verum end; A8: RRing A is associative proof let x be Element of (RRing A); :: according to GROUP_1:def_3 ::_thesis: for b1, b2 being Element of the carrier of (RRing A) holds (x * b1) * b2 = x * (b1 * b2) thus for b1, b2 being Element of the carrier of (RRing A) holds (x * b1) * b2 = x * (b1 * b2) by Th25; ::_thesis: verum end; RRing A is commutative proof let x be Element of (RRing A); :: according to GROUP_1:def_12 ::_thesis: for b1 being Element of the carrier of (RRing A) holds x * b1 = b1 * x thus for b1 being Element of the carrier of (RRing A) holds x * b1 = b1 * x by Th25; ::_thesis: verum end; hence RRing A is commutative Ring by A1, A2, A5, A3, A8, A7, A6; ::_thesis: verum end; definition attrc1 is strict ; struct AlgebraStr -> doubleLoopStr , RLSStruct ; aggrAlgebraStr(# carrier, multF, addF, Mult, OneF, ZeroF #) -> AlgebraStr ; end; registration cluster non empty for AlgebraStr ; existence not for b1 being AlgebraStr holds b1 is empty proof set X = the non empty set ; set m = the BinOp of the non empty set ; set M = the Function of [:REAL, the non empty set :], the non empty set ; set u = the Element of the non empty set ; take AlgebraStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set , the Element of the non empty set , the Element of the non empty set #) ; ::_thesis: not AlgebraStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set , the Element of the non empty set , the Element of the non empty set #) is empty thus not the carrier of AlgebraStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set , the Element of the non empty set , the Element of the non empty set #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum end; end; definition let A be set ; func RAlgebra A -> strict AlgebraStr equals :: FUNCSDOM:def 8 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 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) #); registration let A be non empty set ; cluster RAlgebra A -> non empty strict ; coherence not RAlgebra A is empty ; end; 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_) 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; registration let A be non empty set ; cluster RAlgebra A -> unital strict ; coherence RAlgebra A is unital proof reconsider e = RealFuncUnit A as Element of (RAlgebra A) ; take e ; :: according to GROUP_1:def_1 ::_thesis: for b1 being Element of the carrier of (RAlgebra A) holds ( b1 * e = b1 & e * b1 = b1 ) thus for b1 being Element of the carrier of (RAlgebra A) holds ( b1 * e = b1 & e * b1 = b1 ) by Lm4; ::_thesis: verum end; end; theorem :: FUNCSDOM:27 for A being non empty set holds 1. (RAlgebra A) = RealFuncUnit A ; definition let IT be non empty AlgebraStr ; attrIT 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; end; :: 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 ); registration let A be set ; cluster RAlgebra A -> non empty strict ; coherence not RAlgebra A is empty ; end; registration let A be set ; 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 thus RAlgebra A is strict ; ::_thesis: ( 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 ) thus RAlgebra A is Abelian ::_thesis: ( 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 let x, y be Element of (RAlgebra A); :: according to RLVECT_1:def_2 ::_thesis: x + y = y + x thus x + y = y + x by Th5; ::_thesis: verum end; thus RAlgebra A is add-associative ::_thesis: ( 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 let x, y, z be Element of (RAlgebra A); :: according to RLVECT_1:def_3 ::_thesis: (x + y) + z = x + (y + z) thus (x + y) + z = x + (y + z) by Th6; ::_thesis: verum end; thus RAlgebra A is right_zeroed ::_thesis: ( 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 let x be Element of (RAlgebra A); :: according to RLVECT_1:def_4 ::_thesis: x + (0. (RAlgebra A)) = x thus x + (0. (RAlgebra A)) = (RealFuncAdd A) . ((RealFuncZero A),x) by Th5 .= x by Th10 ; ::_thesis: verum end; thus RAlgebra A is right_complementable ::_thesis: ( 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 let x be Element of (RAlgebra A); :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable reconsider f = x as Element of Funcs (A,REAL) ; reconsider t = (RealFuncExtMult A) . [(- 1),f] as Element of (RAlgebra A) ; take t ; :: according to ALGSTR_0:def_11 ::_thesis: x + t = 0. (RAlgebra A) thus x + t = 0. (RAlgebra A) by Th11; ::_thesis: verum end; thus RAlgebra A is commutative ::_thesis: ( 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 let x, y be Element of (RAlgebra A); :: according to GROUP_1:def_12 ::_thesis: x * y = y * x thus x * y = y * x by Th7; ::_thesis: verum end; thus RAlgebra A is associative ::_thesis: ( 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 let x, y, z be Element of (RAlgebra A); :: according to GROUP_1:def_3 ::_thesis: (x * y) * z = x * (y * z) thus (x * y) * z = x * (y * z) by Th8; ::_thesis: verum end; thus RAlgebra A is right_unital ::_thesis: ( 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 let x be Element of (RAlgebra A); :: according to VECTSP_1:def_4 ::_thesis: x * (1. (RAlgebra A)) = x thus x * (1. (RAlgebra A)) = (RealFuncMult A) . ((RealFuncUnit A),x) by Th7 .= x by Th9 ; ::_thesis: verum end; thus RAlgebra A is right-distributive ::_thesis: ( RAlgebra A is vector-associative & RAlgebra A is scalar-associative & RAlgebra A is vector-distributive & RAlgebra A is scalar-distributive ) proof let x, y, z be Element of (RAlgebra A); :: according to VECTSP_1:def_2 ::_thesis: x * (y + z) = (x * y) + (x * z) thus x * (y + z) = (x * y) + (x * z) by Th15; ::_thesis: verum end; thus RAlgebra A is vector-associative ::_thesis: ( RAlgebra A is scalar-associative & RAlgebra A is vector-distributive & RAlgebra A is scalar-distributive ) proof let x, y be Element of (RAlgebra A); :: according to FUNCSDOM:def_9 ::_thesis: for a being Real holds a * (x * y) = (a * x) * y let a be Real; ::_thesis: a * (x * y) = (a * x) * y thus (a * x) * y = a * (x * y) by Th16; ::_thesis: verum end; thus RAlgebra A is scalar-associative ::_thesis: ( RAlgebra A is vector-distributive & RAlgebra A is scalar-distributive ) proof let a, b be real number ; :: according to RLVECT_1:def_7 ::_thesis: for b1 being Element of the carrier of (RAlgebra A) holds (a * b) * b1 = a * (b * b1) let x be Element of (RAlgebra A); ::_thesis: (a * b) * x = a * (b * x) reconsider a = a, b = b as Element of REAL by XREAL_0:def_1; (a * b) * x = a * (b * x) by Th13; hence (a * b) * x = a * (b * x) ; ::_thesis: verum end; thus RAlgebra A is vector-distributive ::_thesis: RAlgebra A is scalar-distributive proof let a be real number ; :: according to RLVECT_1:def_5 ::_thesis: for b1, b2 being Element of the carrier of (RAlgebra A) holds a * (b1 + b2) = (a * b1) + (a * b2) let v, w be Element of (RAlgebra A); ::_thesis: a * (v + w) = (a * v) + (a * w) reconsider a = a as Element of REAL by XREAL_0:def_1; a * (v + w) = (a * v) + (a * w) by Lm2; hence a * (v + w) = (a * v) + (a * w) ; ::_thesis: verum end; let a, b be real number ; :: according to RLVECT_1:def_6 ::_thesis: for b1 being Element of the carrier of (RAlgebra A) holds (a + b) * b1 = (a * b1) + (b * b1) let v be Element of (RAlgebra A); ::_thesis: (a + b) * v = (a * v) + (b * v) reconsider a = a, b = b as Element of REAL by XREAL_0:def_1; (a + b) * v = (a * v) + (b * v) by Th14; hence (a + b) * v = (a * v) + (b * v) ; ::_thesis: verum end; end; registration 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 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 right_unital & b1 is right-distributive & b1 is vector-associative & b1 is scalar-associative & b1 is vector-distributive & b1 is scalar-distributive ) proof take RAlgebra {} ; ::_thesis: ( RAlgebra {} is strict & RAlgebra {} is Abelian & RAlgebra {} is add-associative & RAlgebra {} is right_zeroed & RAlgebra {} is right_complementable & RAlgebra {} is commutative & RAlgebra {} is associative & RAlgebra {} is right_unital & RAlgebra {} is right-distributive & RAlgebra {} is vector-associative & RAlgebra {} is scalar-associative & RAlgebra {} is vector-distributive & RAlgebra {} is scalar-distributive ) thus ( RAlgebra {} is strict & RAlgebra {} is Abelian & RAlgebra {} is add-associative & RAlgebra {} is right_zeroed & RAlgebra {} is right_complementable & RAlgebra {} is commutative & RAlgebra {} is associative & RAlgebra {} is right_unital & RAlgebra {} is right-distributive & RAlgebra {} is vector-associative & RAlgebra {} is scalar-associative & RAlgebra {} is vector-distributive & RAlgebra {} is scalar-distributive ) ; ::_thesis: verum end; 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;