funcsdom.miz



    begin

    reserve x1,x2,z for set;

    reserve A,B for non empty set;

    definition

      let A be set, 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

      proof

        reconsider f, g as Element of ( Funcs (A,B)) qua non empty set;

        (F . (f,g)) is Element of ( Funcs (A,B));

        hence thesis;

      end;

    end

    definition

      let A,B,C,D be non empty set;

      let F be Function of [:C, D:], ( Funcs (A,B));

      let cd be Element of [:C, D:];

      :: original: .

      redefine

      func F . cd -> Element of ( Funcs (A,B)) ;

      coherence

      proof

        (F . cd) is Element of ( Funcs (A,B));

        hence thesis;

      end;

    end

    reserve f,g,h for Element of ( Funcs (A, REAL ));

    definition

      let X be non empty set, Z be set;

      let F be BinOp of X, f,g be Function of Z, X;

      :: original: .:

      redefine

      func F .: (f,g) -> Element of ( Funcs (Z,X)) ;

      coherence

      proof

        (F .: (f,g)) in ( Funcs (Z,X)) by FUNCT_2: 8;

        hence thesis;

      end;

    end

    definition

      let X be non empty set, Z be set;

      let F be BinOp of X, a be Element of X, f be Function of Z, X;

      :: original: [;]

      redefine

      func F [;] (a,f) -> Element of ( Funcs (Z,X)) ;

      coherence

      proof

        (F [;] (a,f)) in ( Funcs (Z,X)) by FUNCT_2: 8;

        hence thesis;

      end;

    end

    definition

      let A be set;

      :: FUNCSDOM:def1

      func RealFuncAdd (A) -> BinOp of ( Funcs (A, REAL )) means

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

      existence

      proof

        deffunc F( Element of ( Funcs (A, REAL )), Element of ( Funcs (A, REAL ))) = ( addreal .: ($1,$2));

        consider F be BinOp of ( Funcs (A, REAL )) such that

         A1: for x,y be Element of ( Funcs (A, REAL )) holds (F . (x,y)) = F(x,y) from BINOP_1:sch 4;

        take F;

        let f,g be Element of ( Funcs (A, REAL ));

        thus thesis by A1;

      end;

      uniqueness

      proof

        let it1,it2 be BinOp of ( Funcs (A, REAL )) such that

         A2: for f,g be Element of ( Funcs (A, REAL )) holds (it1 . (f,g)) = ( addreal .: (f,g)) and

         A3: for f,g be Element of ( Funcs (A, REAL )) holds (it2 . (f,g)) = ( addreal .: (f,g));

        now

          let f,g be Element of ( Funcs (A, REAL ));

          

          thus (it1 . (f,g)) = ( addreal .: (f,g)) by A2

          .= (it2 . (f,g)) by A3;

        end;

        hence thesis;

      end;

    end

    registration

      let A be set;

      cluster ( RealFuncAdd A) -> real-functions-valued;

      coherence

      proof

        let x be object;

        set IT = ( RealFuncAdd A);

        assume x in ( dom IT);

        then (IT . x) is Function of A, REAL by FUNCT_2: 66, PARTFUN1: 4;

        hence (IT . x) is real-valued Function;

      end;

    end

    definition

      let A be set;

      :: FUNCSDOM:def2

      func RealFuncMult (A) -> BinOp of ( Funcs (A, REAL )) means

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

      existence

      proof

        deffunc F( Element of ( Funcs (A, REAL )), Element of ( Funcs (A, REAL ))) = ( multreal .: ($1,$2));

        consider F be BinOp of ( Funcs (A, REAL )) such that

         A1: for x,y be Element of ( Funcs (A, REAL )) holds (F . (x,y)) = F(x,y) from BINOP_1:sch 4;

        take F;

        let f,g be Element of ( Funcs (A, REAL ));

        thus thesis by A1;

      end;

      uniqueness

      proof

        let it1,it2 be BinOp of ( Funcs (A, REAL )) such that

         A2: for f,g be Element of ( Funcs (A, REAL )) holds (it1 . (f,g)) = ( multreal .: (f,g)) and

         A3: for f,g be Element of ( Funcs (A, REAL )) holds (it2 . (f,g)) = ( multreal .: (f,g));

        now

          let f,g be Element of ( Funcs (A, REAL ));

          

          thus (it1 . (f,g)) = ( multreal .: (f,g)) by A2

          .= (it2 . (f,g)) by A3;

        end;

        hence thesis;

      end;

    end

    registration

      let A be set;

      cluster ( RealFuncMult A) -> real-functions-valued;

      coherence

      proof

        let x be object;

        set IT = ( RealFuncMult A);

        assume x in ( dom IT);

        then (IT . x) is Function of A, REAL by FUNCT_2: 66, PARTFUN1: 4;

        hence (IT . x) is real-valued Function;

      end;

    end

    definition

      let A be set;

      :: FUNCSDOM:def3

      func RealFuncExtMult (A) -> Function of [: REAL , ( Funcs (A, REAL )):], ( Funcs (A, REAL )) means

      : Def3: for a be Real, f be Element of ( Funcs (A, REAL )) holds (it . (a,f)) = ( multreal [;] (a,f));

      existence

      proof

        deffunc F( Element of REAL , Element of ( Funcs (A, REAL ))) = ( multreal [;] ($1,$2));

        consider F be Function of [: REAL , ( Funcs (A, REAL )):], ( Funcs (A, REAL )) such that

         A1: for a be Element of REAL , f be Element of ( Funcs (A, REAL )) holds (F . (a,f)) = F(a,f) from BINOP_1:sch 4;

        take F;

        let a be Real, f be Element of ( Funcs (A, REAL ));

        a in REAL by XREAL_0:def 1;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let it1,it2 be Function of [: REAL , ( Funcs (A, REAL )):], ( Funcs (A, REAL )) such that

         A2: for a be Real, f be Element of ( Funcs (A, REAL )) holds (it1 . (a,f)) = ( multreal [;] (a,f)) and

         A3: for a be Real, f be Element of ( Funcs (A, REAL )) holds (it2 . (a,f)) = ( multreal [;] (a,f));

        now

          let a be Element of REAL , f be Element of ( Funcs (A, REAL ));

          

          thus (it1 . (a,f)) = ( multreal [;] (a,f)) by A2

          .= (it2 . (a,f)) by A3;

        end;

        hence thesis;

      end;

    end

    registration

      let A be set;

      cluster ( RealFuncExtMult A) -> real-functions-valued;

      coherence

      proof

        let x be object;

        set IT = ( RealFuncExtMult A);

        assume x in ( dom IT);

        then (IT . x) is Function of A, REAL by FUNCT_2: 66, PARTFUN1: 4;

        hence (IT . x) is real-valued Function;

      end;

    end

    reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

    definition

      let A be set;

      :: FUNCSDOM:def4

      func RealFuncZero A -> Element of ( Funcs (A, REAL )) equals (A --> 0 );

      coherence

      proof

        (A --> ( In ( 0 , REAL ))) is Function of A, REAL ;

        hence thesis by FUNCT_2: 8;

      end;

      :: FUNCSDOM:def5

      func RealFuncUnit A -> Element of ( Funcs (A, REAL )) equals (A --> 1);

      coherence

      proof

        (A --> jj) is Function of A, REAL ;

        hence thesis by FUNCT_2: 8;

      end;

    end

    theorem :: FUNCSDOM:1

    

     Th1: h = (( RealFuncAdd A) . (f,g)) iff for x be Element of A holds (h . x) = ((f . x) + (g . x))

    proof

       A1:

      now

        assume

         A2: for x be Element of A holds (h . x) = ((f . x) + (g . x));

        now

          let x be Element of A;

          

           A3: ( dom ( addreal .: (f,g))) = A by FUNCT_2:def 1;

          

          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;

        end;

        hence h = (( RealFuncAdd A) . (f,g));

      end;

      now

        assume

         A4: h = (( RealFuncAdd A) . (f,g));

        let x be Element of A;

        

         A5: ( dom ( addreal .: (f,g))) = A by FUNCT_2:def 1;

        

        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;

      end;

      hence thesis by A1;

    end;

    theorem :: FUNCSDOM:2

    

     Th2: h = (( RealFuncMult A) . (f,g)) iff for x be Element of A holds (h . x) = ((f . x) * (g . x))

    proof

       A1:

      now

        assume

         A2: for x be Element of A holds (h . x) = ((f . x) * (g . x));

        now

          let x be Element of A;

          

           A3: ( dom ( multreal .: (f,g))) = A by FUNCT_2:def 1;

          

          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;

        end;

        hence h = (( RealFuncMult A) . (f,g));

      end;

      now

        assume

         A4: h = (( RealFuncMult A) . (f,g));

        let x be Element of A;

        

         A5: ( dom ( multreal .: (f,g))) = A by FUNCT_2:def 1;

        

        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;

      end;

      hence thesis by A1;

    end;

    theorem :: FUNCSDOM:3

    ( RealFuncZero A) <> ( RealFuncUnit A)

    proof

      set a = the Element of A;

      (( RealFuncZero A) . a) = 0 ;

      hence thesis by FUNCOP_1: 7;

    end;

    reserve a,b for Real;

    theorem :: FUNCSDOM:4

    

     Th4: h = (( RealFuncExtMult A) . [a, f]) iff for x be Element of A holds (h . x) = (a * (f . x))

    proof

      reconsider aa = a as Element of REAL by XREAL_0:def 1;

      thus h = (( RealFuncExtMult A) . [a, f]) implies for x be Element of A holds (h . x) = (a * (f . x))

      proof

        assume

         A1: h = (( RealFuncExtMult A) . [a, f]);

        let x be Element of A;

        h = (( RealFuncExtMult A) . (a,f)) by A1;

        

        hence (h . x) = (( multreal [;] (aa,f)) . x) by Def3

        .= ( multreal . (aa,(f . x))) by FUNCOP_1: 53

        .= (a * (f . x)) by BINOP_2:def 11;

      end;

      now

        assume

         A2: for x be Element of A holds (h . x) = (a * (f . x));

        for x be Element of A holds (h . x) = ((( RealFuncExtMult A) . [aa, f]) . x)

        proof

          let x be Element of A;

          

           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) . [aa, f]) . x) by A3, FUNCOP_1: 53;

        end;

        hence h = (( RealFuncExtMult A) . (a,f)) by FUNCT_2: 63;

      end;

      hence thesis;

    end;

    theorem :: FUNCSDOM:5

    

     Th5: for A be set, f,g be Element of ( Funcs (A, REAL )) holds (( RealFuncAdd A) . (f,g)) = (( RealFuncAdd A) . (g,f))

    proof

      let A be set, f,g be Element of ( Funcs (A, REAL ));

      

      thus (( RealFuncAdd A) . (f,g)) = ( addreal .: (f,g)) by Def1

      .= ( addreal .: (g,f)) by FUNCOP_1: 65

      .= (( RealFuncAdd A) . (g,f)) by Def1;

    end;

    theorem :: FUNCSDOM:6

    

     Th6: for A be set, f,g,h be 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, f,g,h be Element of ( Funcs (A, REAL ));

      

      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;

    end;

    theorem :: FUNCSDOM:7

    

     Th7: for A be set, f,g be Element of ( Funcs (A, REAL )) holds (( RealFuncMult A) . (f,g)) = (( RealFuncMult A) . (g,f))

    proof

      let A be set, f,g be Element of ( Funcs (A, REAL ));

      

      thus (( RealFuncMult A) . (f,g)) = ( multreal .: (f,g)) by Def2

      .= ( multreal .: (g,f)) by FUNCOP_1: 65

      .= (( RealFuncMult A) . (g,f)) by Def2;

    end;

    theorem :: FUNCSDOM:8

    

     Th8: for A be set, f,g,h be 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, f,g,h be Element of ( Funcs (A, REAL ));

      

      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;

    end;

    theorem :: FUNCSDOM:9

    

     Th9: for A be set, f be Element of ( Funcs (A, REAL )) holds (( RealFuncMult A) . (( RealFuncUnit A),f)) = f

    proof

      let A be set, f be Element of ( Funcs (A, REAL ));

      per cases ;

        suppose A = {} ;

        then

         A1: f = {} ;

        

        thus (( RealFuncMult A) . (( RealFuncUnit A),f)) = ( multreal .: (( RealFuncUnit A),f)) by Def2

        .= f by A1;

      end;

        suppose A <> {} ;

        then

        reconsider A as non empty set;

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

        now

          let x be Element of A;

          

          thus ((( RealFuncMult A) . (( RealFuncUnit A),f)) . x) = ((( RealFuncUnit A) . x) * (f . x)) by Th2

          .= (1 * (f . x))

          .= (f . x);

        end;

        hence thesis;

      end;

    end;

    theorem :: FUNCSDOM:10

    

     Th10: for A be set, f be Element of ( Funcs (A, REAL )) holds (( RealFuncAdd A) . (( RealFuncZero A),f)) = f

    proof

      let A be set, f be Element of ( Funcs (A, REAL ));

      per cases ;

        suppose A = {} ;

        then

         A1: f = {} ;

        

        thus (( RealFuncAdd A) . (( RealFuncZero A),f)) = ( addreal .: (( RealFuncZero A),f)) by Def1

        .= f by A1;

      end;

        suppose A <> {} ;

        then

        reconsider A as non empty set;

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

        now

          let x be Element of A;

          

          thus ((( RealFuncAdd A) . (( RealFuncZero A),f)) . x) = ((( RealFuncZero A) . x) + (f . x)) by Th1

          .= ( 0 + (f . x))

          .= (f . x);

        end;

        hence thesis;

      end;

    end;

    theorem :: FUNCSDOM:11

    

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

    proof

      let A be set, f be Element of ( Funcs (A, REAL ));

      per cases ;

        suppose

         A1: A = {} ;

        

        then (( RealFuncAdd A) . (f,(( RealFuncExtMult A) . [( - jj), f]))) = {}

        .= ( RealFuncZero A) by A1;

        hence thesis;

      end;

        suppose A <> {} ;

        then

        reconsider A as non empty set;

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

        now

          let x be Element of A;

          set y = (f . x);

          

          thus ((( RealFuncAdd A) . (f,(( RealFuncExtMult A) . [( - jj), f]))) . x) = ((f . x) + ((( RealFuncExtMult A) . [( - jj), f]) . x)) by Th1

          .= ((f . x) + (( - 1) * y)) by Th4

          .= (( RealFuncZero A) . x);

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end;

    theorem :: FUNCSDOM:12

    

     Th12: for A be set, f be Element of ( Funcs (A, REAL )) holds (( RealFuncExtMult A) . (1,f)) = f

    proof

      let A be set, f be Element of ( Funcs (A, REAL ));

      per cases ;

        suppose A = {} ;

        then

         A1: f = {} ;

        

        thus (( RealFuncExtMult A) . (1,f)) = ( multreal [;] (jj,f)) by Def3

        .= f by A1;

      end;

        suppose A <> {} ;

        then

        reconsider A as non empty set;

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

        reconsider g = (( RealFuncExtMult A) . (jj,f)) as Element of ( Funcs (A, REAL ));

        now

          let x be Element of A;

          

          thus (g . x) = (jj * (f . x)) by Th4

          .= (f . x);

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end;

    theorem :: FUNCSDOM:13

    

     Th13: for A be set, f be Element of ( Funcs (A, REAL )) holds (( RealFuncExtMult A) . (a,(( RealFuncExtMult A) . (b,f)))) = (( RealFuncExtMult A) . ((a * b),f))

    proof

      let A be set, f be Element of ( Funcs (A, REAL ));

      reconsider aa = a, bb = b as Element of REAL by XREAL_0:def 1;

      per cases ;

        suppose

         A1: A = {} ;

        (( RealFuncExtMult A) . (b,f)) = ( multreal [;] (b,f)) by Def3;

        

        hence (( RealFuncExtMult A) . (a,(( RealFuncExtMult A) . (b,f)))) = ( multreal [;] (aa,( multreal [;] (bb,f)))) by Def3

        .= ( multreal [;] ((a * b),f)) by A1

        .= (( RealFuncExtMult A) . ((a * b),f)) by Def3;

      end;

        suppose A <> {} ;

        then

        reconsider A as non empty set;

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

        now

          let x be Element of A;

          

          thus ((( RealFuncExtMult A) . [aa, (( RealFuncExtMult A) . [bb, f])]) . x) = (aa * ((( RealFuncExtMult A) . [bb, f]) . x)) by Th4

          .= (aa * (bb * (f . x))) by Th4

          .= ((aa * bb) * (f . x))

          .= ((( RealFuncExtMult A) . [(aa * bb), f]) . x) by Th4;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end;

    theorem :: FUNCSDOM:14

    

     Th14: for A be set, f be Element of ( Funcs (A, REAL )) holds (( RealFuncAdd A) . ((( RealFuncExtMult A) . (a,f)),(( RealFuncExtMult A) . (b,f)))) = (( RealFuncExtMult A) . ((a + b),f))

    proof

      let A be set, f be Element of ( Funcs (A, REAL ));

      reconsider aa = a, bb = b as Element of REAL by XREAL_0:def 1;

      per cases ;

        suppose

         A1: A = {} ;

        

        thus (( RealFuncAdd A) . ((( RealFuncExtMult A) . (a,f)),(( RealFuncExtMult A) . (b,f)))) = (( RealFuncAdd A) . ((( RealFuncExtMult A) . (aa,f)),(( RealFuncExtMult A) . (bb,f))))

        .= {} by A1

        .= ( multreal [;] ((a + b),f)) by A1

        .= (( RealFuncExtMult A) . ((a + b),f)) by Def3;

      end;

        suppose A <> {} ;

        then

        reconsider A as non empty set;

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

        now

          let x be Element of A;

          

          thus ((( RealFuncAdd A) . ((( RealFuncExtMult A) . [aa, f]),(( RealFuncExtMult A) . [bb, f]))) . x) = (((( RealFuncExtMult A) . [aa, f]) . x) + ((( RealFuncExtMult A) . [bb, f]) . x)) by Th1

          .= ((a * (f . x)) + ((( RealFuncExtMult A) . [bb, f]) . x)) by Th4

          .= ((a * (f . x)) + (b * (f . x))) by Th4

          .= ((a + b) * (f . x))

          .= ((( RealFuncExtMult A) . [(aa + bb), f]) . x) by Th4;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end;

    

     Lm2: for A be set, f,g be 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 set, f,g be Element of ( Funcs (A, REAL ));

      reconsider aa = a as Element of REAL by XREAL_0:def 1;

      per cases ;

        suppose

         A1: A = {} ;

        

        thus (( RealFuncAdd A) . ((( RealFuncExtMult A) . (a,f)),(( RealFuncExtMult A) . (a,g)))) = (( RealFuncAdd A) . ((( RealFuncExtMult A) . (aa,f)),(( RealFuncExtMult A) . (aa,g))))

        .= {} by A1

        .= ( multreal [;] (a,(( RealFuncAdd A) . (f,g)))) by A1

        .= (( RealFuncExtMult A) . (a,(( RealFuncAdd A) . (f,g)))) by Def3;

      end;

        suppose A <> {} ;

        then

        reconsider A as non empty set;

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

        now

          let x be Element of A;

          

          thus ((( RealFuncAdd A) . ((( RealFuncExtMult A) . [aa, f]),(( RealFuncExtMult A) . [aa, g]))) . x) = (((( RealFuncExtMult A) . [aa, f]) . x) + ((( RealFuncExtMult A) . [aa, g]) . x)) by Th1

          .= ((a * (f . x)) + ((( RealFuncExtMult A) . [aa, 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) . [aa, (( RealFuncAdd A) . (f,g))]) . x) by Th4;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end;

    theorem :: FUNCSDOM:15

    

     Th15: for A be set, f,g,h be 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, f,g,h be Element of ( Funcs (A, REAL ));

      

       A1: ( multreal .: (f,( addreal .: (g,h)))) = ( addreal .: (( multreal .: (f,g)),( multreal .: (f,h))))

      proof

        let a be Element of A;

        per cases ;

          suppose A = {} ;

          hence (( multreal .: (f,( addreal .: (g,h)))) . a) = (( addreal .: (( multreal .: (f,g)),( multreal .: (f,h)))) . a);

        end;

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

        end;

      end;

      

      thus (( RealFuncMult A) . (f,(( RealFuncAdd A) . (g,h)))) = (( RealFuncMult A) . (f,( addreal .: (g,h)))) by Def1

      .= ( addreal .: (( multreal .: (f,g)),( multreal .: (f,h)))) by A1, Def2

      .= (( 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;

    end;

    theorem :: FUNCSDOM:16

    

     Th16: for A be set, f,g,h be Element of ( Funcs (A, REAL )), a be Real holds (( RealFuncMult A) . ((( RealFuncExtMult A) . (a,f)),g)) = (( RealFuncExtMult A) . (a,(( RealFuncMult A) . (f,g))))

    proof

      let A be set, f,g,h be Element of ( Funcs (A, REAL )), a be Real;

      reconsider aa = a as Element of REAL by XREAL_0:def 1;

      

      thus (( RealFuncMult A) . ((( RealFuncExtMult A) . (a,f)),g)) = (( RealFuncMult A) . (( multreal [;] (a,f)),g)) by Def3

      .= ( multreal .: (( multreal [;] (aa,f)),g)) by Def2

      .= ( multreal [;] (aa,( multreal .: (f,g)))) by FUNCOP_1: 85

      .= (( RealFuncExtMult A) . (a,( multreal .: (f,g)))) by Def3

      .= (( RealFuncExtMult A) . (a,(( RealFuncMult A) . (f,g)))) by Def2;

    end;

    theorem :: FUNCSDOM:17

    

     Th17: x1 in A implies (( RealFuncZero A) +* (x1 .--> 1)) in ( Funcs (A, REAL )) & (( RealFuncUnit A) +* (x1 .--> 0 )) in ( Funcs (A, REAL ))

    proof

      assume

       a0: x1 in A;

      

       A2: ( dom (( RealFuncZero A) +* (x1 .--> 1))) = (( dom ( RealFuncZero A)) \/ ( dom (x1 .--> 1))) by FUNCT_4:def 1

      .= (( dom ( RealFuncZero A)) \/ {x1})

      .= (A \/ {x1})

      .= A by a0, XBOOLE_1: 12, ZFMISC_1: 31;

      

       a2: ( dom (( RealFuncUnit A) +* (x1 .--> 0 ))) = (( dom ( RealFuncUnit A)) \/ ( dom (x1 .--> 0 ))) by FUNCT_4:def 1

      .= (( dom ( RealFuncUnit A)) \/ {x1})

      .= (A \/ {x1})

      .= A by a0, XBOOLE_1: 12, ZFMISC_1: 31;

      

       H2: ( rng (( RealFuncZero A) +* (x1 .--> 1))) c= (( rng ( RealFuncZero A)) \/ ( rng (x1 .--> 1))) by FUNCT_4: 17;

      

       B1: ( rng ( RealFuncZero A)) c= REAL by RELAT_1:def 19;

      ( rng (x1 .--> 1)) = {1} by FUNCOP_1: 8;

      then ( rng (x1 .--> 1)) c= REAL by XREAL_0:def 1, ZFMISC_1: 31;

      then (( rng ( RealFuncZero A)) \/ ( rng (x1 .--> 1))) c= ( REAL \/ REAL ) by B1, XBOOLE_1: 13;

      then

       S1: (( RealFuncZero A) +* (x1 .--> 1)) is Function of A, REAL by A2, FUNCT_2: 2, H2, XBOOLE_1: 1;

      

       H2: ( rng (( RealFuncUnit A) +* (x1 .--> 0 ))) c= (( rng ( RealFuncUnit A)) \/ ( rng (x1 .--> 0 ))) by FUNCT_4: 17;

      

       B1: ( rng ( RealFuncUnit A)) c= REAL by RELAT_1:def 19;

      ( rng (x1 .--> 0 )) = { 0 } by FUNCOP_1: 8;

      then ( rng (x1 .--> 0 )) c= REAL by XREAL_0:def 1, ZFMISC_1: 31;

      then (( rng ( RealFuncUnit A)) \/ ( rng (x1 .--> 0 ))) c= ( REAL \/ REAL ) by B1, XBOOLE_1: 13;

      then (( RealFuncUnit A) +* (x1 .--> 0 )) is Function of A, REAL by a2, FUNCT_2: 2, H2, XBOOLE_1: 1;

      hence thesis by S1, FUNCT_2: 8;

    end;

    theorem :: FUNCSDOM:18

    

     Th18: x1 in A & x2 in A & x1 <> x2 & f = (( RealFuncZero A) +* (x1 .--> 1)) & g = (( RealFuncUnit A) +* (x1 .--> 0 )) implies for a, b st (( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))) = ( RealFuncZero A) holds a = 0 & b = 0

    proof

      assume that

       A1: x1 in A and

       A2: x2 in A and

       A3: x1 <> x2 and

       A4: f = (( RealFuncZero A) +* (x1 .--> 1)) & g = (( RealFuncUnit A) +* (x1 .--> 0 ));

      

       a5: (f . x2) = (( RealFuncZero A) . x2) by A3, A4, FUNCT_4: 83

      .= 0 by A2, FUNCOP_1: 7;

      

       A5: (g . x2) = (( RealFuncUnit A) . x2) by A3, A4, FUNCT_4: 83

      .= 1 by A2, FUNCOP_1: 7;

      

       a6: (f . x1) = 1 by A4, FUNCT_4: 113;

      

       A6: (g . x1) = 0 by A4, FUNCT_4: 113;

      let a, b;

      reconsider x1, x2 as Element of A by A1, A2;

      reconsider aa = a, bb = b as Element of REAL by XREAL_0:def 1;

      assume

       A7: (( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))) = ( RealFuncZero A);

      

      then

       A8: 0 = ((( RealFuncAdd A) . ((( RealFuncExtMult A) . [aa, f]),(( RealFuncExtMult A) . [bb, g]))) . x2)

      .= (((( RealFuncExtMult A) . [aa, f]) . x2) + ((( RealFuncExtMult A) . [bb, g]) . x2)) by Th1

      .= ((a * (f . x2)) + ((( RealFuncExtMult A) . [bb, g]) . x2)) by Th4

      .= ( 0 + (b * 1)) by A5, Th4, a5

      .= b;

       0 = ((( RealFuncAdd A) . ((( RealFuncExtMult A) . [aa, f]),(( RealFuncExtMult A) . [bb, g]))) . x1) by A7

      .= (((( RealFuncExtMult A) . [aa, f]) . x1) + ((( RealFuncExtMult A) . [bb, g]) . x1)) by Th1

      .= ((a * (f . x1)) + ((( RealFuncExtMult A) . [bb, g]) . x1)) by Th4

      .= (a + (b * 0 )) by A6, Th4, a6

      .= a;

      hence thesis by A8;

    end;

    ::$Canceled

    theorem :: FUNCSDOM:20

    

     Th20: A = {x1, x2} & x1 <> x2 & f = (( RealFuncZero A) +* (x1 .--> 1)) & g = (( RealFuncUnit A) +* (x1 .--> 0 )) implies for h holds ex a, b st h = (( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g])))

    proof

      assume that

       A1: A = {x1, x2} and

       A2: x1 <> x2 and

       A3: f = (( RealFuncZero A) +* (x1 .--> 1)) & g = (( RealFuncUnit A) +* (x1 .--> 0 ));

      

       a4: x2 in A by A1, TARSKI:def 2;

      

       A4: (f . x2) = (( RealFuncZero A) . x2) by A2, A3, FUNCT_4: 83

      .= 0 by FUNCOP_1: 7, a4;

      

       A5: (g . x2) = (( RealFuncUnit A) . x2) by A2, A3, FUNCT_4: 83

      .= 1 by FUNCOP_1: 7, a4;

      

       a6: (f . x1) = 1 by A3, FUNCT_4: 113;

      

       B6: (g . x1) = 0 by A3, FUNCT_4: 113;

      let h;

      reconsider x1, x2 as Element of A by A1, TARSKI:def 2;

      take a = (h . x1), b = (h . x2);

      now

        let x be Element of A;

        

         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 A5, 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 * 1) + ((( RealFuncExtMult A) . [b, g]) . x1)) by a6, Th4

        .= (a + (b * 0 )) by Th4, B6

        .= (h . x1);

        hence (h . x) = ((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))) . x) by A6, A7;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    ::$Canceled

    theorem :: FUNCSDOM:22

    

     Th22: A = {x1, x2} & x1 <> x2 implies ex f, g st (for a, b st (( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))) = ( RealFuncZero A) holds a = 0 & b = 0 ) & for h holds ex a, b st h = (( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g])))

    proof

      assume that

       A1: A = {x1, x2} and

       A2: x1 <> x2;

      x1 in A by TARSKI:def 2, A1;

      then

      reconsider f = (( RealFuncZero A) +* (x1 .--> 1)), g = (( RealFuncUnit A) +* (x1 .--> 0 )) as Element of ( Funcs (A, REAL )) by Th17;

      take f, g;

      x1 in A & x2 in A by A1, TARSKI:def 2;

      hence thesis by A1, A2, Th18, Th20;

    end;

    definition

      let A be set;

      :: FUNCSDOM:def6

      func RealVectSpace (A) -> strict RealLinearSpace equals RLSStruct (# ( Funcs (A, REAL )), ( RealFuncZero A), ( RealFuncAdd A), ( RealFuncExtMult A) #);

      coherence

      proof

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

        

         A1: S is add-associative by Th6;

        

         A2: S is right_complementable

        proof

          let u be Element of S;

          reconsider u9 = u as Element of ( Funcs (A, REAL ));

          reconsider w = (( RealFuncExtMult A) . [( - jj), u9]) as VECTOR of S;

          take w;

          thus thesis by Th11;

        end;

        

         A3: S is vector-distributive scalar-distributive scalar-associative scalar-unital by Lm2, Th14, Th13, Th12;

        

         A4: S is right_zeroed

        proof

          let u be Element of S;

          reconsider u9 = u as Element of ( Funcs (A, REAL ));

          

          thus (u + ( 0. S)) = (( RealFuncAdd A) . (( RealFuncZero A),u9)) by Th5

          .= u by Th10;

        end;

        S is Abelian by Th5;

        hence thesis by A1, A4, A2, A3;

      end;

    end

    theorem :: FUNCSDOM:23

    ex V be strict RealLinearSpace st ex u,v be Element of V st (for a, b st ((a * u) + (b * v)) = ( 0. V) holds a = 0 & b = 0 ) & for w be Element of V holds ex a, b st w = ((a * u) + (b * v))

    proof

      set A = { 0 , 1};

      take V = ( RealVectSpace A);

      consider f,g be Element of ( Funcs (A, REAL )) such that

       A1: for a, b st (( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))) = ( RealFuncZero A) holds a = 0 & b = 0 and

       A2: for h be Element of ( Funcs (A, REAL )) holds ex a, b st h = (( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))) by Th22;

      reconsider u = f, v = g as Element of V;

      take u, v;

      thus for a, b st ((a * u) + (b * v)) = ( 0. V) holds a = 0 & b = 0 by A1;

      thus for w be Element of V holds ex a, b st w = ((a * u) + (b * v))

      proof

        let w be Element of V;

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

        consider a, b such that

         A3: h = (( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))) by A2;

        h = ((a * u) + (b * v)) by A3;

        hence thesis;

      end;

    end;

    definition

      let A;

      :: FUNCSDOM:def7

      func RRing (A) -> strict doubleLoopStr equals doubleLoopStr (# ( Funcs (A, REAL )), ( RealFuncAdd A), ( RealFuncMult A), ( RealFuncUnit A), ( RealFuncZero A) #);

      correctness ;

    end

    registration

      let A;

      cluster ( RRing A) -> non empty;

      coherence ;

    end

     Lm3:

    now

      let A;

      set FR = ( RRing A);

      let h,a be Element of FR;

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

      assume

       A1: a = ( RealFuncUnit A);

      

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

      .= h by Th9;

      thus (a * h) = h by A1, Th9;

    end;

    registration

      let A;

      cluster ( RRing A) -> unital;

      coherence

      proof

        reconsider e = ( RealFuncUnit A) as Element of ( RRing A);

        take e;

        thus thesis by Lm3;

      end;

    end

    theorem :: FUNCSDOM:24

    ( 1. ( RRing A)) = ( RealFuncUnit A);

    theorem :: FUNCSDOM:25

    

     Th25: for x,y,z be Element of ( RRing A) holds (x + y) = (y + x) & ((x + y) + z) = (x + (y + z)) & (x + ( 0. ( RRing A))) = x & (ex t be 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 x,y,z be Element of ( RRing A);

      set IT = ( RRing A);

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

      thus (x + y) = (y + x) by Th5;

      thus ((x + y) + z) = (x + (y + z)) by Th6;

      

      thus (x + ( 0. ( RRing A))) = (( RealFuncAdd A) . (( RealFuncZero A),f)) by Th5

      .= x by Th10;

      thus ex t be Element of ( RRing A) st (x + t) = ( 0. ( RRing A))

      proof

        set h = (( RealFuncExtMult A) . [( - jj), f]);

        reconsider t = h as Element of IT;

        take t;

        thus thesis by Th11;

      end;

      thus (x * y) = (y * x) by Th7;

      thus ((x * y) * z) = (x * (y * z)) by Th8;

      

      thus (x * ( 1. ( RRing A))) = (( RealFuncMult A) . (( RealFuncUnit A),f)) by Th7

      .= x by Th9;

      hence (( 1. ( RRing A)) * x) = x by Th7;

      thus (x * (y + z)) = ((x * y) + (x * z)) by Th15;

      

      hence ((y + z) * x) = ((x * y) + (x * z)) by Th7

      .= ((y * x) + (x * z)) by Th7

      .= ((y * x) + (z * x)) by Th7;

    end;

    registration

      cluster strict Abelian add-associative right_zeroed right_complementable associative commutative right_unital right-distributive for 1 -element doubleLoopStr;

      existence

      proof

        take L = Trivial-doubleLoopStr ;

        thus L is strict;

        thus L is Abelian by STRUCT_0:def 10;

        thus L is add-associative by STRUCT_0:def 10;

        thus L is right_zeroed by STRUCT_0:def 10;

        thus L is right_complementable

        proof

          let x be Element of L;

          take x;

          thus thesis by STRUCT_0:def 10;

        end;

        thus L is associative by STRUCT_0:def 10;

        thus L is commutative by STRUCT_0:def 10;

        thus L is right_unital by STRUCT_0:def 10;

        let x be Element of L;

        thus thesis by STRUCT_0:def 10;

      end;

    end

    theorem :: FUNCSDOM:26

    ( RRing A) is commutative Ring

    proof

      

       A1: ( RRing A) is Abelian by Th25;

      

       A2: ( RRing A) is add-associative by Th25;

      

       A3: ( RRing A) is right_complementable

      proof

        let x be Element of ( RRing A);

        consider t be Element of ( RRing A) such that

         A4: (x + t) = ( 0. ( RRing A)) by Th25;

        take t;

        thus thesis by A4;

      end;

      

       A5: ( RRing A) is right_zeroed by Th25;

      

       A6: ( RRing A) is distributive by Th25;

      

       A7: ( RRing A) is well-unital by Th25;

      

       A8: ( RRing A) is associative by Th25;

      ( RRing A) is commutative by Th25;

      hence thesis by A1, A2, A5, A3, A8, A7, A6;

    end;

    definition

      struct ( doubleLoopStr, RLSStruct) AlgebraStr (# the carrier -> set,

the multF, addF -> BinOp of the carrier,

the Mult -> Function of [: REAL , the carrier:], the carrier,

the OneF, ZeroF -> Element of the carrier #)

       attr strict strict;

    end

    registration

      cluster non empty for AlgebraStr;

      existence

      proof

        set X = the non empty set, m = the BinOp of X, M = the Function of [: REAL , X:], X, u = the Element of X;

        take AlgebraStr (# X, m, m, M, u, u #);

        thus the carrier of AlgebraStr (# X, m, m, M, u, u #) is non empty;

      end;

    end

    definition

      let A be set;

      :: FUNCSDOM:def8

      func RAlgebra A -> strict AlgebraStr equals AlgebraStr (# ( Funcs (A, REAL )), ( RealFuncMult A), ( RealFuncAdd A), ( RealFuncExtMult A), ( RealFuncUnit A), ( RealFuncZero A) #);

      correctness ;

    end

    registration

      let A;

      cluster ( RAlgebra A) -> non empty;

      coherence ;

    end

     Lm4:

    now

      let A;

      set F = ( RAlgebra A);

      let x,e be Element of F;

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

      assume

       A1: e = ( RealFuncUnit A);

      

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

      .= x by Th9;

      thus (e * x) = x by A1, Th9;

    end;

    registration

      let A;

      cluster ( RAlgebra A) -> unital;

      coherence

      proof

        reconsider e = ( RealFuncUnit A) as Element of ( RAlgebra A);

        take e;

        thus thesis by Lm4;

      end;

    end

    theorem :: FUNCSDOM:27

    ( 1. ( RAlgebra A)) = ( RealFuncUnit A);

    definition

      let IT be non empty AlgebraStr;

      :: FUNCSDOM:def9

      attr IT is vector-associative means for x,y be Element of IT holds for a holds (a * (x * y)) = ((a * x) * y);

    end

    registration

      let A be set;

      cluster ( RAlgebra A) -> non empty;

      coherence ;

    end

    registration

      let A be set;

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

      coherence

      proof

        thus ( RAlgebra A) is strict;

        thus ( RAlgebra A) is Abelian by Th5;

        thus ( RAlgebra A) is add-associative by Th6;

        thus ( RAlgebra A) is right_zeroed

        proof

          let x be Element of ( RAlgebra A);

          

          thus (x + ( 0. ( RAlgebra A))) = (( RealFuncAdd A) . (( RealFuncZero A),x)) by Th5

          .= x by Th10;

        end;

        thus ( RAlgebra A) is right_complementable

        proof

          let x be Element of ( RAlgebra A);

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

          reconsider t = (( RealFuncExtMult A) . [( - jj), f]) as Element of ( RAlgebra A);

          take t;

          thus thesis by Th11;

        end;

        thus ( RAlgebra A) is commutative by Th7;

        thus ( RAlgebra A) is associative by Th8;

        thus ( RAlgebra A) is right_unital

        proof

          let x be Element of ( RAlgebra A);

          

          thus (x * ( 1. ( RAlgebra A))) = (( RealFuncMult A) . (( RealFuncUnit A),x)) by Th7

          .= x by Th9;

        end;

        thus ( RAlgebra A) is right-distributive by Th15;

        thus ( RAlgebra A) is vector-associative by Th16;

        thus ( RAlgebra A) is scalar-associative by Th13;

        thus ( RAlgebra A) is vector-distributive by Lm2;

        let a,b be Real, v be Element of ( RAlgebra A);

        thus thesis by Th14;

      end;

    end

    registration

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

      existence

      proof

        take ( RAlgebra {} );

        thus thesis;

      end;

    end

    definition

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

    end

    theorem :: FUNCSDOM:28

    (( RealFuncAdd A) . (f,g)) = (f + g)

    proof

      

       A1: ( dom (( RealFuncAdd A) . (f,g))) = A by FUNCT_2:def 1;

      

       a1: ( dom (f + g)) = (( dom f) /\ ( dom g)) by VALUED_1:def 1

      .= (A /\ ( dom g)) by FUNCT_2:def 1

      .= (A /\ A) by FUNCT_2:def 1

      .= A;

      now

        let x be object;

        assume

         a0: x in ( dom (f + g));

        

         A3: ( dom ( addreal .: (f,g))) = A by FUNCT_2:def 1;

        

        thus ((( RealFuncAdd A) . (f,g)) . x) = (( addreal .: (f,g)) . x) by Def1

        .= ( addreal . ((f . x),(g . x))) by a1, a0, A3, FUNCOP_1: 22

        .= ((f . x) + (g . x)) by BINOP_2:def 9

        .= ((f + g) . x) by VALUED_1: 1, a1, a0;

      end;

      hence thesis by a1, A1, FUNCT_1: 2;

    end;

    theorem :: FUNCSDOM:29

    (( RealFuncMult A) . (f,g)) = (f (#) g)

    proof

      

       A1: ( dom (( RealFuncMult A) . (f,g))) = A by FUNCT_2:def 1;

      

       a1: ( dom (f (#) g)) = (( dom f) /\ ( dom g)) by VALUED_1:def 4

      .= (A /\ ( dom g)) by FUNCT_2:def 1

      .= (A /\ A) by FUNCT_2:def 1

      .= A;

      now

        let x be object;

        assume

         a0: x in ( dom (f (#) g));

        

         A3: ( dom ( multreal .: (f,g))) = A by FUNCT_2:def 1;

        

        thus ((( RealFuncMult A) . (f,g)) . x) = (( multreal .: (f,g)) . x) by Def2

        .= ( multreal . ((f . x),(g . x))) by a1, a0, A3, FUNCOP_1: 22

        .= ((f . x) * (g . x)) by BINOP_2:def 11

        .= ((f (#) g) . x) by VALUED_1: 5;

      end;

      hence thesis by A1, a1, FUNCT_1: 2;

    end;

    theorem :: FUNCSDOM:30

    (( RealFuncExtMult A) . (a,f)) = (a (#) f)

    proof

      reconsider aa = a as Element of REAL by XREAL_0:def 1;

      set h = (( RealFuncExtMult A) . (a,f));

      

       b1: ( dom (a (#) f)) = ( dom f) by VALUED_1:def 5

      .= A by FUNCT_2:def 1;

       A2:

      now

        let x be Element of A;

        

        thus (h . x) = (( multreal [;] (aa,f)) . x) by Def3

        .= ( multreal . (aa,(f . x))) by FUNCOP_1: 53

        .= (a * (f . x)) by BINOP_2:def 11

        .= ((a (#) f) . x) by VALUED_1:def 5, b1;

      end;

      a in REAL & f in ( Funcs (A, REAL )) by XREAL_0:def 1;

      then [a, f] in [: REAL , ( Funcs (A, REAL )):] by ZFMISC_1: 87;

      then (( RealFuncExtMult A) . (a,f)) is Function of A, REAL by FUNCT_2: 66, FUNCT_2: 5;

      then

       B1: ( dom (( RealFuncExtMult A) . (a,f))) = A by FUNCT_2:def 1;

      for x be object st x in ( dom (a (#) f)) holds ((( RealFuncExtMult A) . (a,f)) . x) = ((a (#) f) . x) by A2, b1;

      hence thesis by FUNCT_1: 2, B1, b1;

    end;