rfunct_1.miz

    begin

    reserve x for object,

X,Y for set;

    reserve C for non empty set;

    reserve c for Element of C;

    reserve f,f1,f2,f3,g,g1 for complex-valued Function;

    reserve r,p for Complex;



     Lm1: (( - 1) " ) = ( - 1);

    definition

      let f1,f2 be complex-valued Function;

      :: RFUNCT_1:def1

      func f1 / f2 -> Function means

      : Def1: ( dom it ) = (( dom f1) /\ (( dom f2) \ (f2 " { 0 }))) & for c be object st c in ( dom it ) holds (it . c) = ((f1 . c) * ((f2 . c) " ));

      existence

      proof

        deffunc F( object) = ((f1 . $1) * ((f2 . $1) " ));

        ex f be Function st ( dom f) = (( dom f1) /\ (( dom f2) \ (f2 " { 0 }))) & for x be object st x in (( dom f1) /\ (( dom f2) \ (f2 " { 0 }))) holds (f . x) = F(x) from FUNCT_1:sch 3;

        hence thesis;

      end;

      uniqueness

      proof

        let f,g be Function such that

         A1: ( dom f) = (( dom f1) /\ (( dom f2) \ (f2 " { 0 }))) and

         A2: for c be object st c in ( dom f) holds (f . c) = ((f1 . c) * ((f2 . c) " )) and

         A3: ( dom g) = (( dom f1) /\ (( dom f2) \ (f2 " { 0 }))) and

         A4: for c be object st c in ( dom g) holds (g . c) = ((f1 . c) * ((f2 . c) " ));

        now

          let x be object;

          assume

           A5: x in ( dom f);



          hence (f . x) = ((f1 . x) * ((f2 . x) " )) by A2

          .= (g . x) by A1, A3, A4, A5;

        end;

        hence thesis by A1, A3, FUNCT_1: 2;

      end;

    end

    registration

      let f1,f2 be complex-valued Function;

      cluster (f1 / f2) -> complex-valued;

      coherence

      proof

        let x be object;

        set F = (f1 / f2);

        assume x in ( dom F);

        then (F . x) = ((f1 . x) * ((f2 . x) " )) by Def1;

        hence thesis;

      end;

    end

    registration

      let f1,f2 be real-valued Function;

      cluster (f1 / f2) -> real-valued;

      coherence

      proof

        let x be object;

        set F = (f1 / f2);

        assume x in ( dom F);

        then (F . x) = ((f1 . x) * ((f2 . x) " )) by Def1;

        hence thesis;

      end;

    end

    definition

      let C be set, D be complex-membered set;

      let f1,f2 be PartFunc of C, D;

      :: original: /

      redefine

      func f1 / f2 -> PartFunc of C, COMPLEX ;

      coherence

      proof

        set F = (f1 / f2);



         A1: ( rng F) c= COMPLEX by VALUED_0:def 1;

        ( dom F) = (( dom f1) /\ (( dom f2) \ (f2 " { 0 }))) by Def1;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    definition

      let C be set, D be real-membered set;

      let f1,f2 be PartFunc of C, D;

      :: original: /

      redefine

      func f1 / f2 -> PartFunc of C, REAL ;

      coherence

      proof

        set F = (f1 / f2);

        ( rng F) c= REAL by VALUED_0:def 3;

        then F is PartFunc of ( dom F), REAL by RELSET_1: 4;

        hence thesis by RELSET_1: 5;

      end;

    end

    definition

      let f be complex-valued Function;

      :: RFUNCT_1:def2

      func f ^ -> Function means

      : Def2: ( dom it ) = (( dom f) \ (f " { 0 })) & for c be object st c in ( dom it ) holds (it . c) = ((f . c) " );

      existence

      proof

        deffunc F( object) = ((f . $1) " );

        ex h be Function st ( dom h) = (( dom f) \ (f " { 0 })) & for x be object st x in (( dom f) \ (f " { 0 })) holds (h . x) = F(x) from FUNCT_1:sch 3;

        hence thesis;

      end;

      uniqueness

      proof

        let h,g be Function such that

         A1: ( dom h) = (( dom f) \ (f " { 0 })) and

         A2: for c be object st c in ( dom h) holds (h . c) = ((f . c) " ) and

         A3: ( dom g) = (( dom f) \ (f " { 0 })) and

         A4: for c be object st c in ( dom g) holds (g . c) = ((f . c) " );

        now

          let x be object;

          assume

           A5: x in ( dom h);



          hence (h . x) = ((f . x) " ) by A2

          .= (g . x) by A1, A3, A4, A5;

        end;

        hence thesis by A1, A3, FUNCT_1: 2;

      end;

    end

    registration

      let f be complex-valued Function;

      cluster (f ^ ) -> complex-valued;

      coherence

      proof

        let x be object;

        set F = (f ^ );

        assume x in ( dom F);

        then (F . x) = ((f . x) " ) by Def2;

        hence thesis;

      end;

    end

    registration

      let f be real-valued Function;

      cluster (f ^ ) -> real-valued;

      coherence

      proof

        let x be object;

        set F = (f ^ );

        assume x in ( dom F);

        then (F . x) = ((f . x) " ) by Def2;

        hence thesis;

      end;

    end

    definition

      let C be set, D be complex-membered set, f be PartFunc of C, D;

      :: original: ^

      redefine

      func f ^ -> PartFunc of C, COMPLEX ;

      coherence

      proof

        set F = (f ^ );



         A1: ( rng F) c= COMPLEX by VALUED_0:def 1;

        ( dom F) = (( dom f) \ (f " { 0 })) by Def2;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    definition

      let C be set, D be real-membered set, f be PartFunc of C, D;

      :: original: ^

      redefine

      func f ^ -> PartFunc of C, REAL ;

      coherence

      proof

        set F = (f ^ );

        ( rng F) c= REAL by VALUED_0:def 3;

        then F is PartFunc of ( dom F), REAL by RELSET_1: 4;

        hence thesis by RELSET_1: 5;

      end;

    end

    theorem :: RFUNCT_1:1



     Th1: ( dom (g ^ )) c= ( dom g) & (( dom g) /\ (( dom g) \ (g " { 0 }))) = (( dom g) \ (g " { 0 }))

    proof

      ( dom (g ^ )) = (( dom g) \ (g " { 0 })) by Def2;

      hence ( dom (g ^ )) c= ( dom g);

      thus thesis by XBOOLE_1: 28;

    end;

    theorem :: RFUNCT_1:2



     Th2: (( dom (f1 (#) f2)) \ ((f1 (#) f2) " { 0 })) = ((( dom f1) \ (f1 " { 0 })) /\ (( dom f2) \ (f2 " { 0 })))

    proof

      thus (( dom (f1 (#) f2)) \ ((f1 (#) f2) " { 0 })) c= ((( dom f1) \ (f1 " { 0 })) /\ (( dom f2) \ (f2 " { 0 })))

      proof

        let x be object;

        assume

         A1: x in (( dom (f1 (#) f2)) \ ((f1 (#) f2) " { 0 }));

        then not x in ((f1 (#) f2) " { 0 }) by XBOOLE_0:def 5;

        then not ((f1 (#) f2) . x) in { 0 } by A1, FUNCT_1:def 7;

        then ((f1 (#) f2) . x) <> 0 by TARSKI:def 1;

        then

         A2: ((f1 . x) * (f2 . x)) <> 0 by VALUED_1: 5;

        then (f2 . x) <> 0 ;

        then not (f2 . x) in { 0 } by TARSKI:def 1;

        then

         A3: not x in (f2 " { 0 }) by FUNCT_1:def 7;

        x in ( dom (f1 (#) f2)) by A1;

        then

         A4: x in (( dom f1) /\ ( dom f2)) by VALUED_1:def 4;

        then x in ( dom f2) by XBOOLE_0:def 4;

        then

         A5: x in (( dom f2) \ (f2 " { 0 })) by A3, XBOOLE_0:def 5;

        (f1 . x) <> 0 by A2;

        then not (f1 . x) in { 0 } by TARSKI:def 1;

        then

         A6: not x in (f1 " { 0 }) by FUNCT_1:def 7;

        x in ( dom f1) by A4, XBOOLE_0:def 4;

        then x in (( dom f1) \ (f1 " { 0 })) by A6, XBOOLE_0:def 5;

        hence thesis by A5, XBOOLE_0:def 4;

      end;

      thus ((( dom f1) \ (f1 " { 0 })) /\ (( dom f2) \ (f2 " { 0 }))) c= (( dom (f1 (#) f2)) \ ((f1 (#) f2) " { 0 }))

      proof

        let x be object;

        assume

         A7: x in ((( dom f1) \ (f1 " { 0 })) /\ (( dom f2) \ (f2 " { 0 })));

        then x in (( dom f2) \ (f2 " { 0 })) by XBOOLE_0:def 4;

        then not x in (f2 " { 0 }) by XBOOLE_0:def 5;

        then not (f2 . x) in { 0 } by A7, FUNCT_1:def 7;

        then

         A8: (f2 . x) <> 0 by TARSKI:def 1;



         A9: x in (( dom f1) \ (f1 " { 0 })) by A7, XBOOLE_0:def 4;

        then not x in (f1 " { 0 }) by XBOOLE_0:def 5;

        then not (f1 . x) in { 0 } by A9, FUNCT_1:def 7;

        then (f1 . x) <> 0 by TARSKI:def 1;

        then ((f1 . x) * (f2 . x)) <> 0 by A8;

        then ((f1 (#) f2) . x) <> 0 by VALUED_1: 5;

        then not ((f1 (#) f2) . x) in { 0 } by TARSKI:def 1;

        then

         A10: not x in ((f1 (#) f2) " { 0 }) by FUNCT_1:def 7;

        x in (( dom f1) /\ ( dom f2)) by A7, A9, XBOOLE_0:def 4;

        then x in ( dom (f1 (#) f2)) by VALUED_1:def 4;

        hence thesis by A10, XBOOLE_0:def 5;

      end;

    end;

    theorem :: RFUNCT_1:3



     Th3: c in ( dom (f ^ )) implies (f . c) <> 0

    proof

      assume that

       A1: c in ( dom (f ^ )) and

       A2: (f . c) = 0 ;



       A3: c in (( dom f) \ (f " { 0 })) by A1, Def2;

      then

       A4: not c in (f " { 0 }) by XBOOLE_0:def 5;

      now

        per cases by A4, FUNCT_1:def 7;

          suppose not c in ( dom f);

          hence contradiction by A3;

        end;

          suppose not (f . c) in { 0 };

          hence contradiction by A2, TARSKI:def 1;

        end;

      end;

      hence contradiction;

    end;

    theorem :: RFUNCT_1:4



     Th4: ((f ^ ) " { 0 }) = {}

    proof

      set x = the Element of ((f ^ ) " { 0 });

      assume

       A1: ((f ^ ) " { 0 }) <> {} ;

      then

       A2: x in ( dom (f ^ )) by FUNCT_1:def 7;

      then

       A3: x in (( dom f) \ (f " { 0 })) by Def2;

      then not x in (f " { 0 }) by XBOOLE_0:def 5;

      then

       A4: not (f . x) in { 0 } by A3, FUNCT_1:def 7;

      ((f ^ ) qua Function . x) in { 0 } by A1, FUNCT_1:def 7;

      then ((f ^ ) . x) = 0 by TARSKI:def 1;

      then ((f . x) " ) = 0 by A2, Def2;

      hence contradiction by A4, TARSKI:def 1, XCMPLX_1: 202;

    end;

    theorem :: RFUNCT_1:5



     Th5: (( abs f) " { 0 }) = (f " { 0 }) & (( - f) " { 0 }) = (f " { 0 })

    proof

      now

        let c be object;

        reconsider cc = c as object;

        thus c in (( abs f) " { 0 }) implies c in (f " { 0 })

        proof

          assume

           A1: c in (( abs f) " { 0 });

          then (( abs f) . c) in { 0 } by FUNCT_1:def 7;

          then (( abs f) . c) = 0 by TARSKI:def 1;

          then |.(f . cc).| = 0 by VALUED_1: 18;

          then (f . c) = 0 by COMPLEX1: 45;

          then

           A2: (f . c) in { 0 } by TARSKI:def 1;

          c in ( dom ( abs f)) by A1, FUNCT_1:def 7;

          then c in ( dom f) by VALUED_1:def 11;

          hence thesis by A2, FUNCT_1:def 7;

        end;

        assume

         A3: c in (f " { 0 });

        then (f . c) in { 0 } by FUNCT_1:def 7;

        then (f . c) = 0 by TARSKI:def 1;

        then |.(f . cc).| = 0 by ABSVALUE: 2;

        then (( abs f) . c) = 0 by VALUED_1: 18;

        then

         A4: (( abs f) . c) in { 0 } by TARSKI:def 1;

        c in ( dom f) by A3, FUNCT_1:def 7;

        then c in ( dom ( abs f)) by VALUED_1:def 11;

        hence c in (( abs f) " { 0 }) by A4, FUNCT_1:def 7;

      end;

      hence (( abs f) " { 0 }) = (f " { 0 }) by TARSKI: 2;

      now

        let c be object;

        reconsider cc = c as object;

        thus c in (( - f) " { 0 }) implies c in (f " { 0 })

        proof

          assume

           A5: c in (( - f) " { 0 });

          then (( - f) . c) in { 0 } by FUNCT_1:def 7;

          then (( - f) . c) = 0 by TARSKI:def 1;

          then ( - ( - (f . cc))) = ( - ( In ( 0 , REAL ))) by VALUED_1: 8;

          then

           A6: (f . c) in { 0 } by TARSKI:def 1;

          c in ( dom ( - f)) by A5, FUNCT_1:def 7;

          then c in ( dom f) by VALUED_1: 8;

          hence thesis by A6, FUNCT_1:def 7;

        end;

        assume

         A7: c in (f " { 0 });

        then (f . c) in { 0 } by FUNCT_1:def 7;

        then (f . c) = 0 by TARSKI:def 1;

        then (( - f) . c) = ( - ( In ( 0 , REAL ))) by VALUED_1: 8;

        then

         A8: (( - f) . c) in { 0 } by TARSKI:def 1;

        c in ( dom f) by A7, FUNCT_1:def 7;

        then c in ( dom ( - f)) by VALUED_1: 8;

        hence c in (( - f) " { 0 }) by A8, FUNCT_1:def 7;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: RFUNCT_1:6



     Th6: ( dom ((f ^ ) ^ )) = ( dom (f | ( dom (f ^ ))))

    proof



       A1: ( dom (f ^ )) = (( dom f) \ (f " { 0 })) by Def2;



      thus ( dom ((f ^ ) ^ )) = (( dom (f ^ )) \ ((f ^ ) " { 0 })) by Def2

      .= (( dom (f ^ )) \ {} ) by Th4

      .= (( dom f) /\ ( dom (f ^ ))) by A1, XBOOLE_1: 28

      .= ( dom (f | ( dom (f ^ )))) by RELAT_1: 61;

    end;

    theorem :: RFUNCT_1:7



     Th7: r <> 0 implies ((r (#) f) " { 0 }) = (f " { 0 })

    proof

      assume

       A1: r <> 0 ;

      now

        let c be object;

        reconsider cc = c as object;

        thus c in ((r (#) f) " { 0 }) implies c in (f " { 0 })

        proof

          assume

           A2: c in ((r (#) f) " { 0 });

          then

           A3: c in ( dom (r (#) f)) by FUNCT_1:def 7;

          ((r (#) f) . c) in { 0 } by A2, FUNCT_1:def 7;

          then ((r (#) f) . c) = 0 by TARSKI:def 1;

          then (r * (f . cc)) = 0 by A3, VALUED_1:def 5;

          then (f . c) = 0 by A1;

          then

           A4: (f . c) in { 0 } by TARSKI:def 1;

          c in ( dom f) by A3, VALUED_1:def 5;

          hence thesis by A4, FUNCT_1:def 7;

        end;

        assume

         A5: c in (f " { 0 });

        then (f . c) in { 0 } by FUNCT_1:def 7;

        then (f . c) = 0 by TARSKI:def 1;

        then

         A6: (r * (f . cc)) = 0 ;



         A7: c in ( dom f) by A5, FUNCT_1:def 7;

        then c in ( dom (r (#) f)) by VALUED_1:def 5;

        then ((r (#) f) . c) = 0 by A6, VALUED_1:def 5;

        then

         A8: ((r (#) f) . c) in { 0 } by TARSKI:def 1;

        c in ( dom (r (#) f)) by A7, VALUED_1:def 5;

        hence c in ((r (#) f) " { 0 }) by A8, FUNCT_1:def 7;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: RFUNCT_1:8

    ((f1 + f2) + f3) = (f1 + (f2 + f3))

    proof



       A1: ( dom ((f1 + f2) + f3)) = (( dom (f1 + f2)) /\ ( dom f3)) by VALUED_1:def 1

      .= ((( dom f1) /\ ( dom f2)) /\ ( dom f3)) by VALUED_1:def 1

      .= (( dom f1) /\ (( dom f2) /\ ( dom f3))) by XBOOLE_1: 16

      .= (( dom f1) /\ ( dom (f2 + f3))) by VALUED_1:def 1

      .= ( dom (f1 + (f2 + f3))) by VALUED_1:def 1;

      now

        let c be object;

        assume

         A2: c in ( dom ((f1 + f2) + f3));

        then c in (( dom (f1 + f2)) /\ ( dom f3)) by VALUED_1:def 1;

        then

         A3: c in ( dom (f1 + f2)) by XBOOLE_0:def 4;

        c in (( dom f1) /\ ( dom (f2 + f3))) by A1, A2, VALUED_1:def 1;

        then

         A4: c in ( dom (f2 + f3)) by XBOOLE_0:def 4;



        thus (((f1 + f2) + f3) . c) = (((f1 + f2) . c) + (f3 . c)) by A2, VALUED_1:def 1

        .= (((f1 . c) + (f2 . c)) + (f3 . c)) by A3, VALUED_1:def 1

        .= ((f1 . c) + ((f2 . c) + (f3 . c)))

        .= ((f1 . c) + ((f2 + f3) . c)) by A4, VALUED_1:def 1

        .= ((f1 + (f2 + f3)) . c) by A1, A2, VALUED_1:def 1;

      end;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: RFUNCT_1:9



     Th9: ((f1 (#) f2) (#) f3) = (f1 (#) (f2 (#) f3))

    proof

       A1:

      now

        let c be object;

        assume c in ( dom ((f1 (#) f2) (#) f3));



        thus (((f1 (#) f2) (#) f3) . c) = (((f1 (#) f2) . c) * (f3 . c)) by VALUED_1: 5

        .= (((f1 . c) * (f2 . c)) * (f3 . c)) by VALUED_1: 5

        .= ((f1 . c) * ((f2 . c) * (f3 . c)))

        .= ((f1 . c) * ((f2 (#) f3) . c)) by VALUED_1: 5

        .= ((f1 (#) (f2 (#) f3)) . c) by VALUED_1: 5;

      end;

      ( dom ((f1 (#) f2) (#) f3)) = (( dom (f1 (#) f2)) /\ ( dom f3)) by VALUED_1:def 4

      .= ((( dom f1) /\ ( dom f2)) /\ ( dom f3)) by VALUED_1:def 4

      .= (( dom f1) /\ (( dom f2) /\ ( dom f3))) by XBOOLE_1: 16

      .= (( dom f1) /\ ( dom (f2 (#) f3))) by VALUED_1:def 4

      .= ( dom (f1 (#) (f2 (#) f3))) by VALUED_1:def 4;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: RFUNCT_1:10



     Th10: ((f1 + f2) (#) f3) = ((f1 (#) f3) + (f2 (#) f3))

    proof



       A1: ( dom ((f1 + f2) (#) f3)) = (( dom (f1 + f2)) /\ ( dom f3)) by VALUED_1:def 4

      .= ((( dom f1) /\ ( dom f2)) /\ (( dom f3) /\ ( dom f3))) by VALUED_1:def 1

      .= (((( dom f1) /\ ( dom f2)) /\ ( dom f3)) /\ ( dom f3)) by XBOOLE_1: 16

      .= (((( dom f1) /\ ( dom f3)) /\ ( dom f2)) /\ ( dom f3)) by XBOOLE_1: 16

      .= ((( dom f1) /\ ( dom f3)) /\ (( dom f2) /\ ( dom f3))) by XBOOLE_1: 16

      .= (( dom (f1 (#) f3)) /\ (( dom f2) /\ ( dom f3))) by VALUED_1:def 4

      .= (( dom (f1 (#) f3)) /\ ( dom (f2 (#) f3))) by VALUED_1:def 4

      .= ( dom ((f1 (#) f3) + (f2 (#) f3))) by VALUED_1:def 1;

      now

        let c be object;

        assume

         A2: c in ( dom ((f1 + f2) (#) f3));

        then c in (( dom (f1 + f2)) /\ ( dom f3)) by VALUED_1:def 4;

        then

         A3: c in ( dom (f1 + f2)) by XBOOLE_0:def 4;



        thus (((f1 + f2) (#) f3) . c) = (((f1 + f2) . c) * (f3 . c)) by VALUED_1: 5

        .= (((f1 . c) + (f2 . c)) * (f3 . c)) by A3, VALUED_1:def 1

        .= (((f1 . c) * (f3 . c)) + ((f2 . c) * (f3 . c)))

        .= (((f1 (#) f3) . c) + ((f2 . c) * (f3 . c))) by VALUED_1: 5

        .= (((f1 (#) f3) . c) + ((f2 (#) f3) . c)) by VALUED_1: 5

        .= (((f1 (#) f3) + (f2 (#) f3)) . c) by A1, A2, VALUED_1:def 1;

      end;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: RFUNCT_1:11

    (f3 (#) (f1 + f2)) = ((f3 (#) f1) + (f3 (#) f2)) by Th10;

    theorem :: RFUNCT_1:12



     Th12: (r (#) (f1 (#) f2)) = ((r (#) f1) (#) f2)

    proof



       A1: ( dom (r (#) (f1 (#) f2))) = ( dom (f1 (#) f2)) by VALUED_1:def 5

      .= (( dom f1) /\ ( dom f2)) by VALUED_1:def 4

      .= (( dom (r (#) f1)) /\ ( dom f2)) by VALUED_1:def 5

      .= ( dom ((r (#) f1) (#) f2)) by VALUED_1:def 4;

      now

        let c be object;

        assume

         A2: c in ( dom (r (#) (f1 (#) f2)));

        then c in (( dom (r (#) f1)) /\ ( dom f2)) by A1, VALUED_1:def 4;

        then

         A3: c in ( dom (r (#) f1)) by XBOOLE_0:def 4;



        thus ((r (#) (f1 (#) f2)) . c) = (r * ((f1 (#) f2) . c)) by A2, VALUED_1:def 5

        .= (r * ((f1 . c) * (f2 . c))) by VALUED_1: 5

        .= ((r * (f1 . c)) * (f2 . c))

        .= (((r (#) f1) . c) * (f2 . c)) by A3, VALUED_1:def 5

        .= (((r (#) f1) (#) f2) . c) by VALUED_1: 5;

      end;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: RFUNCT_1:13



     Th13: (r (#) (f1 (#) f2)) = (f1 (#) (r (#) f2))

    proof



       A1: ( dom (r (#) (f1 (#) f2))) = ( dom (f1 (#) f2)) by VALUED_1:def 5

      .= (( dom f1) /\ ( dom f2)) by VALUED_1:def 4

      .= (( dom f1) /\ ( dom (r (#) f2))) by VALUED_1:def 5

      .= ( dom (f1 (#) (r (#) f2))) by VALUED_1:def 4;

      now

        let c be object;

        assume

         A2: c in ( dom (r (#) (f1 (#) f2)));

        then c in (( dom f1) /\ ( dom (r (#) f2))) by A1, VALUED_1:def 4;

        then

         A3: c in ( dom (r (#) f2)) by XBOOLE_0:def 4;



        thus ((r (#) (f1 (#) f2)) . c) = (r * ((f1 (#) f2) . c)) by A2, VALUED_1:def 5

        .= (r * ((f1 . c) * (f2 . c))) by VALUED_1: 5

        .= ((f1 . c) * (r * (f2 . c)))

        .= ((f1 . c) * ((r (#) f2) . c)) by A3, VALUED_1:def 5

        .= ((f1 (#) (r (#) f2)) . c) by VALUED_1: 5;

      end;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: RFUNCT_1:14



     Th14: ((f1 - f2) (#) f3) = ((f1 (#) f3) - (f2 (#) f3))

    proof



       A1: ( dom ((f1 - f2) (#) f3)) = (( dom (f1 - f2)) /\ ( dom f3)) by VALUED_1:def 4

      .= ((( dom f1) /\ ( dom f2)) /\ (( dom f3) /\ ( dom f3))) by VALUED_1: 12

      .= (((( dom f1) /\ ( dom f2)) /\ ( dom f3)) /\ ( dom f3)) by XBOOLE_1: 16

      .= (((( dom f1) /\ ( dom f3)) /\ ( dom f2)) /\ ( dom f3)) by XBOOLE_1: 16

      .= ((( dom f1) /\ ( dom f3)) /\ (( dom f2) /\ ( dom f3))) by XBOOLE_1: 16

      .= (( dom (f1 (#) f3)) /\ (( dom f2) /\ ( dom f3))) by VALUED_1:def 4

      .= (( dom (f1 (#) f3)) /\ ( dom (f2 (#) f3))) by VALUED_1:def 4

      .= ( dom ((f1 (#) f3) - (f2 (#) f3))) by VALUED_1: 12;

      now

        let c be object;

        assume

         A2: c in ( dom ((f1 - f2) (#) f3));

        then c in (( dom (f1 - f2)) /\ ( dom f3)) by VALUED_1:def 4;

        then

         A3: c in ( dom (f1 - f2)) by XBOOLE_0:def 4;



        thus (((f1 - f2) (#) f3) . c) = (((f1 - f2) . c) * (f3 . c)) by VALUED_1: 5

        .= (((f1 . c) - (f2 . c)) * (f3 . c)) by A3, VALUED_1: 13

        .= (((f1 . c) * (f3 . c)) - ((f2 . c) * (f3 . c)))

        .= (((f1 (#) f3) . c) - ((f2 . c) * (f3 . c))) by VALUED_1: 5

        .= (((f1 (#) f3) . c) - ((f2 (#) f3) . c)) by VALUED_1: 5

        .= (((f1 (#) f3) - (f2 (#) f3)) . c) by A1, A2, VALUED_1: 13;

      end;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: RFUNCT_1:15

    ((f3 (#) f1) - (f3 (#) f2)) = (f3 (#) (f1 - f2)) by Th14;

    theorem :: RFUNCT_1:16

    (r (#) (f1 + f2)) = ((r (#) f1) + (r (#) f2))

    proof



       A1: ( dom (r (#) (f1 + f2))) = ( dom (f1 + f2)) by VALUED_1:def 5

      .= (( dom f1) /\ ( dom f2)) by VALUED_1:def 1

      .= (( dom f1) /\ ( dom (r (#) f2))) by VALUED_1:def 5

      .= (( dom (r (#) f1)) /\ ( dom (r (#) f2))) by VALUED_1:def 5

      .= ( dom ((r (#) f1) + (r (#) f2))) by VALUED_1:def 1;

      now

        let c be object;

        assume

         A2: c in ( dom (r (#) (f1 + f2)));

        then

         A3: c in ( dom (f1 + f2)) by VALUED_1:def 5;



         A4: c in (( dom (r (#) f1)) /\ ( dom (r (#) f2))) by A1, A2, VALUED_1:def 1;

        then

         A5: c in ( dom (r (#) f1)) by XBOOLE_0:def 4;



         A6: c in ( dom (r (#) f2)) by A4, XBOOLE_0:def 4;



        thus ((r (#) (f1 + f2)) . c) = (r * ((f1 + f2) . c)) by A2, VALUED_1:def 5

        .= (r * ((f1 . c) + (f2 . c))) by A3, VALUED_1:def 1

        .= ((r * (f1 . c)) + (r * (f2 . c)))

        .= (((r (#) f1) . c) + (r * (f2 . c))) by A5, VALUED_1:def 5

        .= (((r (#) f1) . c) + ((r (#) f2) . c)) by A6, VALUED_1:def 5

        .= (((r (#) f1) + (r (#) f2)) . c) by A1, A2, VALUED_1:def 1;

      end;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: RFUNCT_1:17

    ((r * p) (#) f) = (r (#) (p (#) f))

    proof



       A1: ( dom ((r * p) (#) f)) = ( dom f) by VALUED_1:def 5

      .= ( dom (p (#) f)) by VALUED_1:def 5

      .= ( dom (r (#) (p (#) f))) by VALUED_1:def 5;

      now

        let c be object;

        assume

         A2: c in ( dom ((r * p) (#) f));

        then

         A3: c in ( dom (p (#) f)) by A1, VALUED_1:def 5;



        thus (((r * p) (#) f) . c) = ((r * p) * (f . c)) by A2, VALUED_1:def 5

        .= (r * (p * (f . c)))

        .= (r * ((p (#) f) . c)) by A3, VALUED_1:def 5

        .= ((r (#) (p (#) f)) . c) by A1, A2, VALUED_1:def 5;

      end;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: RFUNCT_1:18

    (r (#) (f1 - f2)) = ((r (#) f1) - (r (#) f2))

    proof



       A1: ( dom (r (#) (f1 - f2))) = ( dom (f1 - f2)) by VALUED_1:def 5

      .= (( dom f1) /\ ( dom f2)) by VALUED_1: 12

      .= (( dom f1) /\ ( dom (r (#) f2))) by VALUED_1:def 5

      .= (( dom (r (#) f1)) /\ ( dom (r (#) f2))) by VALUED_1:def 5

      .= ( dom ((r (#) f1) - (r (#) f2))) by VALUED_1: 12;

      now

        let c be object;

        assume

         A2: c in ( dom (r (#) (f1 - f2)));

        then

         A3: c in ( dom (f1 - f2)) by VALUED_1:def 5;



         A4: c in (( dom (r (#) f1)) /\ ( dom (r (#) f2))) by A1, A2, VALUED_1: 12;

        then

         A5: c in ( dom (r (#) f1)) by XBOOLE_0:def 4;



         A6: c in ( dom (r (#) f2)) by A4, XBOOLE_0:def 4;



        thus ((r (#) (f1 - f2)) . c) = (r * ((f1 - f2) . c)) by A2, VALUED_1:def 5

        .= (r * ((f1 . c) - (f2 . c))) by A3, VALUED_1: 13

        .= ((r * (f1 . c)) - (r * (f2 . c)))

        .= (((r (#) f1) . c) - (r * (f2 . c))) by A5, VALUED_1:def 5

        .= (((r (#) f1) . c) - ((r (#) f2) . c)) by A6, VALUED_1:def 5

        .= (((r (#) f1) - (r (#) f2)) . c) by A1, A2, VALUED_1: 13;

      end;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: RFUNCT_1:19

    (f1 - f2) = (( - 1) (#) (f2 - f1))

    proof



       A1: ( dom (f1 - f2)) = (( dom f2) /\ ( dom f1)) by VALUED_1: 12

      .= ( dom (f2 - f1)) by VALUED_1: 12

      .= ( dom (( - 1) (#) (f2 - f1))) by VALUED_1:def 5;

      now



         A2: ( dom (f1 - f2)) = (( dom f2) /\ ( dom f1)) by VALUED_1: 12

        .= ( dom (f2 - f1)) by VALUED_1: 12;

        let c be object such that

         A3: c in ( dom (f1 - f2));



        thus ((f1 - f2) . c) = ((f1 . c) - (f2 . c)) by A3, VALUED_1: 13

        .= (( - 1) * ((f2 . c) - (f1 . c)))

        .= (( - 1) * ((f2 - f1) . c)) by A3, A2, VALUED_1: 13

        .= ((( - 1) (#) (f2 - f1)) . c) by A1, A3, VALUED_1:def 5;

      end;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: RFUNCT_1:20

    (f1 - (f2 + f3)) = ((f1 - f2) - f3)

    proof



       A1: ( dom (f1 - (f2 + f3))) = (( dom f1) /\ ( dom (f2 + f3))) by VALUED_1: 12

      .= (( dom f1) /\ (( dom f2) /\ ( dom f3))) by VALUED_1:def 1

      .= ((( dom f1) /\ ( dom f2)) /\ ( dom f3)) by XBOOLE_1: 16

      .= (( dom (f1 - f2)) /\ ( dom f3)) by VALUED_1: 12

      .= ( dom ((f1 - f2) - f3)) by VALUED_1: 12;

      now

        let c be object;

        assume

         A2: c in ( dom (f1 - (f2 + f3)));

        then c in (( dom f1) /\ ( dom (f2 + f3))) by VALUED_1: 12;

        then

         A3: c in ( dom (f2 + f3)) by XBOOLE_0:def 4;

        c in (( dom (f1 - f2)) /\ ( dom f3)) by A1, A2, VALUED_1: 12;

        then

         A4: c in ( dom (f1 - f2)) by XBOOLE_0:def 4;



        thus ((f1 - (f2 + f3)) . c) = ((f1 . c) - ((f2 + f3) . c)) by A2, VALUED_1: 13

        .= ((f1 . c) - ((f2 . c) + (f3 . c))) by A3, VALUED_1:def 1

        .= (((f1 . c) - (f2 . c)) - (f3 . c))

        .= (((f1 - f2) . c) - (f3 . c)) by A4, VALUED_1: 13

        .= (((f1 - f2) - f3) . c) by A1, A2, VALUED_1: 13;

      end;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: RFUNCT_1:21

    (1 (#) f) = f

    proof

       A1:

      now

        let c be object;

        assume c in ( dom (1 (#) f));



        hence ((1 (#) f) . c) = (1 * (f . c)) by VALUED_1:def 5

        .= (f . c);

      end;

      ( dom (1 (#) f)) = ( dom f) by VALUED_1:def 5;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: RFUNCT_1:22

    (f1 - (f2 - f3)) = ((f1 - f2) + f3)

    proof



       A1: ( dom (f1 - (f2 - f3))) = (( dom f1) /\ ( dom (f2 - f3))) by VALUED_1: 12

      .= (( dom f1) /\ (( dom f2) /\ ( dom f3))) by VALUED_1: 12

      .= ((( dom f1) /\ ( dom f2)) /\ ( dom f3)) by XBOOLE_1: 16

      .= (( dom (f1 - f2)) /\ ( dom f3)) by VALUED_1: 12

      .= ( dom ((f1 - f2) + f3)) by VALUED_1:def 1;

      now

        let c be object;

        assume

         A2: c in ( dom (f1 - (f2 - f3)));

        then c in (( dom f1) /\ ( dom (f2 - f3))) by VALUED_1: 12;

        then

         A3: c in ( dom (f2 - f3)) by XBOOLE_0:def 4;

        c in (( dom (f1 - f2)) /\ ( dom f3)) by A1, A2, VALUED_1:def 1;

        then

         A4: c in ( dom (f1 - f2)) by XBOOLE_0:def 4;



        thus ((f1 - (f2 - f3)) . c) = ((f1 . c) - ((f2 - f3) . c)) by A2, VALUED_1: 13

        .= ((f1 . c) - ((f2 . c) - (f3 . c))) by A3, VALUED_1: 13

        .= (((f1 . c) - (f2 . c)) + (f3 . c))

        .= (((f1 - f2) . c) + (f3 . c)) by A4, VALUED_1: 13

        .= (((f1 - f2) + f3) . c) by A1, A2, VALUED_1:def 1;

      end;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: RFUNCT_1:23

    (f1 + (f2 - f3)) = ((f1 + f2) - f3)

    proof



       A1: ( dom (f1 + (f2 - f3))) = (( dom f1) /\ ( dom (f2 - f3))) by VALUED_1:def 1

      .= (( dom f1) /\ (( dom f2) /\ ( dom f3))) by VALUED_1: 12

      .= ((( dom f1) /\ ( dom f2)) /\ ( dom f3)) by XBOOLE_1: 16

      .= (( dom (f1 + f2)) /\ ( dom f3)) by VALUED_1:def 1

      .= ( dom ((f1 + f2) - f3)) by VALUED_1: 12;

      now

        let c be object;

        assume

         A2: c in ( dom (f1 + (f2 - f3)));

        then c in (( dom f1) /\ ( dom (f2 - f3))) by VALUED_1:def 1;

        then

         A3: c in ( dom (f2 - f3)) by XBOOLE_0:def 4;

        c in (( dom (f1 + f2)) /\ ( dom f3)) by A1, A2, VALUED_1: 12;

        then

         A4: c in ( dom (f1 + f2)) by XBOOLE_0:def 4;



        thus ((f1 + (f2 - f3)) . c) = ((f1 . c) + ((f2 - f3) . c)) by A2, VALUED_1:def 1

        .= ((f1 . c) + ((f2 . c) - (f3 . c))) by A3, VALUED_1: 13

        .= (((f1 . c) + (f2 . c)) - (f3 . c))

        .= (((f1 + f2) . c) - (f3 . c)) by A4, VALUED_1:def 1

        .= (((f1 + f2) - f3) . c) by A1, A2, VALUED_1: 13;

      end;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: RFUNCT_1:24



     Th24: ( abs (f1 (#) f2)) = (( abs f1) (#) ( abs f2))

    proof

       A1:

      now

        let c be object;

        assume c in ( dom ( abs (f1 (#) f2)));



        thus (( abs (f1 (#) f2)) . c) = |.((f1 (#) f2) . c).| by VALUED_1: 18

        .= |.((f1 . c) * (f2 . c)).| by VALUED_1: 5

        .= ( |.(f1 . c).| * |.(f2 . c).|) by COMPLEX1: 65

        .= ((( abs f1) . c) * |.(f2 . c).|) by VALUED_1: 18

        .= ((( abs f1) . c) * (( abs f2) . c)) by VALUED_1: 18

        .= ((( abs f1) (#) ( abs f2)) . c) by VALUED_1: 5;

      end;

      ( dom ( abs (f1 (#) f2))) = ( dom (f1 (#) f2)) by VALUED_1:def 11

      .= (( dom f1) /\ ( dom f2)) by VALUED_1:def 4

      .= (( dom f1) /\ ( dom ( abs f2))) by VALUED_1:def 11

      .= (( dom ( abs f1)) /\ ( dom ( abs f2))) by VALUED_1:def 11

      .= ( dom (( abs f1) (#) ( abs f2))) by VALUED_1:def 4;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: RFUNCT_1:25

    ( abs (r (#) f)) = ( |.r.| (#) ( abs f))

    proof



       A1: ( dom ( abs (r (#) f))) = ( dom (r (#) f)) by VALUED_1:def 11

      .= ( dom f) by VALUED_1:def 5

      .= ( dom ( abs f)) by VALUED_1:def 11

      .= ( dom ( |.r.| (#) ( abs f))) by VALUED_1:def 5;

      now

        let c be object;

        assume

         A2: c in ( dom ( abs (r (#) f)));

        then

         A3: c in ( dom (r (#) f)) by VALUED_1:def 11;



        thus (( abs (r (#) f)) . c) = |.((r (#) f) . c).| by VALUED_1: 18

        .= |.(r * (f . c)).| by A3, VALUED_1:def 5

        .= ( |.r.| * |.(f . c).|) by COMPLEX1: 65

        .= ( |.r.| * (( abs f) . c)) by VALUED_1: 18

        .= (( |.r.| (#) ( abs f)) . c) by A1, A2, VALUED_1:def 5;

      end;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: RFUNCT_1:26



     Th26: ((f ^ ) ^ ) = (f | ( dom (f ^ )))

    proof



       A1: ( dom ((f ^ ) ^ )) = ( dom (f | ( dom (f ^ )))) by Th6;

      now

        let c be object;

        assume

         A2: c in ( dom ((f ^ ) ^ ));

        then c in (( dom f) /\ ( dom (f ^ ))) by A1, RELAT_1: 61;

        then

         A3: c in ( dom (f ^ )) by XBOOLE_0:def 4;



        thus (((f ^ ) ^ ) . c) = (((f ^ ) . c) " ) by A2, Def2

        .= (((f . c) " ) " ) by A3, Def2

        .= ((f | ( dom (f ^ ))) . c) by A1, A2, FUNCT_1: 47;

      end;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: RFUNCT_1:27



     Th27: ((f1 (#) f2) ^ ) = ((f1 ^ ) (#) (f2 ^ ))

    proof



       A1: ( dom ((f1 (#) f2) ^ )) = (( dom (f1 (#) f2)) \ ((f1 (#) f2) " { 0 })) by Def2

      .= ((( dom f1) \ (f1 " { 0 })) /\ (( dom f2) \ (f2 " { 0 }))) by Th2

      .= (( dom (f1 ^ )) /\ (( dom f2) \ (f2 " { 0 }))) by Def2

      .= (( dom (f1 ^ )) /\ ( dom (f2 ^ ))) by Def2

      .= ( dom ((f1 ^ ) (#) (f2 ^ ))) by VALUED_1:def 4;

      now

        let c be object;

        assume

         A2: c in ( dom ((f1 (#) f2) ^ ));

        then

         A3: c in (( dom (f1 ^ )) /\ ( dom (f2 ^ ))) by A1, VALUED_1:def 4;

        then

         A4: c in ( dom (f1 ^ )) by XBOOLE_0:def 4;



         A5: c in ( dom (f2 ^ )) by A3, XBOOLE_0:def 4;



        thus (((f1 (#) f2) ^ ) . c) = (((f1 (#) f2) . c) " ) by A2, Def2

        .= (((f1 . c) * (f2 . c)) " ) by VALUED_1: 5

        .= (((f1 . c) " ) * ((f2 . c) " )) by XCMPLX_1: 204

        .= (((f1 ^ ) . c) * ((f2 . c) " )) by A4, Def2

        .= (((f1 ^ ) . c) * ((f2 ^ ) . c)) by A5, Def2

        .= (((f1 ^ ) (#) (f2 ^ )) . c) by VALUED_1: 5;

      end;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: RFUNCT_1:28



     Th28: r <> 0 implies ((r (#) f) ^ ) = ((r " ) (#) (f ^ ))

    proof

      assume

       A1: r <> 0 ;



       A2: ( dom ((r (#) f) ^ )) = (( dom (r (#) f)) \ ((r (#) f) " { 0 })) by Def2

      .= (( dom (r (#) f)) \ (f " { 0 })) by A1, Th7

      .= (( dom f) \ (f " { 0 })) by VALUED_1:def 5

      .= ( dom (f ^ )) by Def2

      .= ( dom ((r " ) (#) (f ^ ))) by VALUED_1:def 5;

      now

        let c be object;

        assume

         A3: c in ( dom ((r (#) f) ^ ));

        then

         A4: c in (( dom (r (#) f)) \ ((r (#) f) " { 0 })) by Def2;



         A5: c in ( dom (f ^ )) by A2, A3, VALUED_1:def 5;



        thus (((r (#) f) ^ ) . c) = (((r (#) f) . c) " ) by A3, Def2

        .= ((r * (f . c)) " ) by A4, VALUED_1:def 5

        .= ((r " ) * ((f . c) " )) by XCMPLX_1: 204

        .= ((r " ) * ((f ^ ) . c)) by A5, Def2

        .= (((r " ) (#) (f ^ )) . c) by A2, A3, VALUED_1:def 5;

      end;

      hence thesis by A2, FUNCT_1: 2;

    end;

    theorem :: RFUNCT_1:29

    (( - f) ^ ) = (( - 1) (#) (f ^ )) by Lm1, Th28;

    theorem :: RFUNCT_1:30



     Th30: (( abs f) ^ ) = ( abs (f ^ ))

    proof



       A1: ( dom (( abs f) ^ )) = (( dom ( abs f)) \ (( abs f) " { 0 })) by Def2

      .= (( dom f) \ (( abs f) " { 0 })) by VALUED_1:def 11

      .= (( dom f) \ (f " { 0 })) by Th5

      .= ( dom (f ^ )) by Def2

      .= ( dom ( abs (f ^ ))) by VALUED_1:def 11;

      now

        let c be object;

        assume

         A2: c in ( dom (( abs f) ^ ));

        then

         A3: c in ( dom (f ^ )) by A1, VALUED_1:def 11;



        thus ((( abs f) ^ ) . c) = ((( abs f) . c) " ) by A2, Def2

        .= ( |.(f . c).| " ) by VALUED_1: 18

        .= (1 / |.(f . c).|) by XCMPLX_1: 215

        .= |.(1 / (f . c)).| by COMPLEX1: 80

        .= |.((f . c) " ).| by XCMPLX_1: 215

        .= |.((f ^ ) . c).| by A3, Def2

        .= (( abs (f ^ )) . c) by VALUED_1: 18;

      end;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: RFUNCT_1:31



     Th31: (f / g) = (f (#) (g ^ ))

    proof

       A1:

      now

        let c be object;

        assume

         A2: c in ( dom (f / g));

        then c in (( dom f) /\ (( dom g) \ (g " { 0 }))) by Def1;

        then c in (( dom f) /\ ( dom (g ^ ))) by Def2;

        then

         A3: c in ( dom (g ^ )) by XBOOLE_0:def 4;



        thus ((f / g) . c) = ((f . c) * ((g . c) " )) by A2, Def1

        .= ((f . c) * ((g ^ ) . c)) by A3, Def2

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

      end;

      ( dom (f / g)) = (( dom f) /\ (( dom g) \ (g " { 0 }))) by Def1

      .= (( dom f) /\ ( dom (g ^ ))) by Def2

      .= ( dom (f (#) (g ^ ))) by VALUED_1:def 4;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: RFUNCT_1:32



     Th32: (r (#) (g / f)) = ((r (#) g) / f)

    proof



      thus (r (#) (g / f)) = (r (#) (g (#) (f ^ ))) by Th31

      .= ((r (#) g) (#) (f ^ )) by Th12

      .= ((r (#) g) / f) by Th31;

    end;

    theorem :: RFUNCT_1:33

    ((f / g) (#) g) = (f | ( dom (g ^ )))

    proof



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

      .= ((( dom f) /\ (( dom g) \ (g " { 0 }))) /\ ( dom g)) by Def1

      .= (( dom f) /\ ((( dom g) \ (g " { 0 })) /\ ( dom g))) by XBOOLE_1: 16

      .= (( dom f) /\ (( dom (g ^ )) /\ ( dom g))) by Def2

      .= (( dom f) /\ ( dom (g ^ ))) by Th1, XBOOLE_1: 28

      .= ( dom (f | ( dom (g ^ )))) by RELAT_1: 61;

      now

        let c be object;

        assume

         A2: c in ( dom ((f / g) (#) g));

        then c in (( dom f) /\ ( dom (g ^ ))) by A1, RELAT_1: 61;

        then

         A3: c in ( dom (g ^ )) by XBOOLE_0:def 4;

        then

         A4: (g . c) <> 0 by Th3;



        thus (((f / g) (#) g) . c) = (((f / g) . c) * (g . c)) by VALUED_1: 5

        .= (((f (#) (g ^ )) . c) * (g . c)) by Th31

        .= (((f . c) * ((g ^ ) . c)) * (g . c)) by VALUED_1: 5

        .= (((f . c) * ((g . c) " )) * (g . c)) by A3, Def2

        .= ((f . c) * (((g . c) " ) * (g . c)))

        .= ((f . c) * 1) by A4, XCMPLX_0:def 7

        .= ((f | ( dom (g ^ ))) . c) by A1, A2, FUNCT_1: 47;

      end;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: RFUNCT_1:34



     Th34: ((f / g) (#) (f1 / g1)) = ((f (#) f1) / (g (#) g1))

    proof

       A1:

      now

        let c be object;

        assume c in ( dom ((f / g) (#) (f1 / g1)));



        thus (((f / g) (#) (f1 / g1)) . c) = (((f / g) . c) * ((f1 / g1) . c)) by VALUED_1: 5

        .= (((f (#) (g ^ )) . c) * ((f1 / g1) . c)) by Th31

        .= (((f (#) (g ^ )) . c) * ((f1 (#) (g1 ^ )) . c)) by Th31

        .= (((f . c) * ((g ^ ) . c)) * ((f1 (#) (g1 ^ )) . c)) by VALUED_1: 5

        .= (((f . c) * ((g ^ ) . c)) * ((f1 . c) * ((g1 ^ ) . c))) by VALUED_1: 5

        .= ((f . c) * ((f1 . c) * (((g ^ ) . c) * ((g1 ^ ) . c))))

        .= ((f . c) * ((f1 . c) * (((g ^ ) (#) (g1 ^ )) . c))) by VALUED_1: 5

        .= (((f . c) * (f1 . c)) * (((g ^ ) (#) (g1 ^ )) . c))

        .= (((f . c) * (f1 . c)) * (((g (#) g1) ^ ) . c)) by Th27

        .= (((f (#) f1) . c) * (((g (#) g1) ^ ) . c)) by VALUED_1: 5

        .= (((f (#) f1) (#) ((g (#) g1) ^ )) . c) by VALUED_1: 5

        .= (((f (#) f1) / (g (#) g1)) . c) by Th31;

      end;

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

      .= ((( dom f) /\ (( dom g) \ (g " { 0 }))) /\ ( dom (f1 / g1))) by Def1

      .= ((( dom f) /\ (( dom g) \ (g " { 0 }))) /\ (( dom f1) /\ (( dom g1) \ (g1 " { 0 })))) by Def1

      .= (( dom f) /\ ((( dom g) \ (g " { 0 })) /\ (( dom f1) /\ (( dom g1) \ (g1 " { 0 }))))) by XBOOLE_1: 16

      .= (( dom f) /\ (( dom f1) /\ ((( dom g) \ (g " { 0 })) /\ (( dom g1) \ (g1 " { 0 }))))) by XBOOLE_1: 16

      .= ((( dom f) /\ ( dom f1)) /\ ((( dom g) \ (g " { 0 })) /\ (( dom g1) \ (g1 " { 0 })))) by XBOOLE_1: 16

      .= (( dom (f (#) f1)) /\ ((( dom g) \ (g " { 0 })) /\ (( dom g1) \ (g1 " { 0 })))) by VALUED_1:def 4

      .= (( dom (f (#) f1)) /\ (( dom (g (#) g1)) \ ((g (#) g1) " { 0 }))) by Th2

      .= ( dom ((f (#) f1) / (g (#) g1))) by Def1;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: RFUNCT_1:35



     Th35: ((f1 / f2) ^ ) = ((f2 | ( dom (f2 ^ ))) / f1)

    proof



      thus ((f1 / f2) ^ ) = ((f1 (#) (f2 ^ )) ^ ) by Th31

      .= ((f1 ^ ) (#) ((f2 ^ ) ^ )) by Th27

      .= ((f2 | ( dom (f2 ^ ))) (#) (f1 ^ )) by Th26

      .= ((f2 | ( dom (f2 ^ ))) / f1) by Th31;

    end;

    theorem :: RFUNCT_1:36



     Th36: (g (#) (f1 / f2)) = ((g (#) f1) / f2)

    proof



      thus (g (#) (f1 / f2)) = (g (#) (f1 (#) (f2 ^ ))) by Th31

      .= ((g (#) f1) (#) (f2 ^ )) by Th9

      .= ((g (#) f1) / f2) by Th31;

    end;

    theorem :: RFUNCT_1:37

    (g / (f1 / f2)) = ((g (#) (f2 | ( dom (f2 ^ )))) / f1)

    proof



      thus (g / (f1 / f2)) = (g (#) ((f1 / f2) ^ )) by Th31

      .= (g (#) ((f2 | ( dom (f2 ^ ))) / f1)) by Th35

      .= ((g (#) (f2 | ( dom (f2 ^ )))) / f1) by Th36;

    end;

    theorem :: RFUNCT_1:38

    ( - (f / g)) = (( - f) / g) & (f / ( - g)) = ( - (f / g))

    proof

      thus ( - (f / g)) = (( - f) / g) by Th32;



      thus (f / ( - g)) = (f (#) (( - g) ^ )) by Th31

      .= (f (#) (( - 1) (#) (g ^ ))) by Lm1, Th28

      .= ( - (f (#) (g ^ ))) by Th13

      .= ( - (f / g)) by Th31;

    end;

    theorem :: RFUNCT_1:39

    ((f1 / f) + (f2 / f)) = ((f1 + f2) / f) & ((f1 / f) - (f2 / f)) = ((f1 - f2) / f)

    proof



      thus ((f1 / f) + (f2 / f)) = ((f1 (#) (f ^ )) + (f2 / f)) by Th31

      .= ((f1 (#) (f ^ )) + (f2 (#) (f ^ ))) by Th31

      .= ((f1 + f2) (#) (f ^ )) by Th10

      .= ((f1 + f2) / f) by Th31;



      thus ((f1 / f) - (f2 / f)) = ((f1 (#) (f ^ )) - (f2 / f)) by Th31

      .= ((f1 (#) (f ^ )) - (f2 (#) (f ^ ))) by Th31

      .= ((f1 - f2) (#) (f ^ )) by Th14

      .= ((f1 - f2) / f) by Th31;

    end;

    theorem :: RFUNCT_1:40



     Th40: ((f1 / f) + (g1 / g)) = (((f1 (#) g) + (g1 (#) f)) / (f (#) g))

    proof

       A1:

      now

        let c be object;



         A2: ( dom (g ^ )) c= ( dom g) by Th1;

        assume

         A3: c in ( dom ((f1 / f) + (g1 / g)));

        then

         A4: c in (( dom (f1 / f)) /\ ( dom (g1 / g))) by VALUED_1:def 1;

        then

         A5: c in ( dom (f1 / f)) by XBOOLE_0:def 4;



         A6: c in ( dom (g1 / g)) by A4, XBOOLE_0:def 4;



         A7: ( dom (f ^ )) c= ( dom f) by Th1;



         A8: c in (( dom (f1 (#) (f ^ ))) /\ ( dom (g1 / g))) by A4, Th31;

        then c in ( dom (f1 (#) (f ^ ))) by XBOOLE_0:def 4;

        then

         A9: c in (( dom f1) /\ ( dom (f ^ ))) by VALUED_1:def 4;

        then

         A10: c in ( dom (f ^ )) by XBOOLE_0:def 4;

        then

         A11: (f . c) <> 0 by Th3;

        c in (( dom (f1 (#) (f ^ ))) /\ ( dom (g1 (#) (g ^ )))) by A8, Th31;

        then c in ( dom (g1 (#) (g ^ ))) by XBOOLE_0:def 4;

        then

         A12: c in (( dom g1) /\ ( dom (g ^ ))) by VALUED_1:def 4;

        then

         A13: c in ( dom (g ^ )) by XBOOLE_0:def 4;

        then

         A14: (g . c) <> 0 by Th3;

        c in ( dom g1) by A12, XBOOLE_0:def 4;

        then c in (( dom g1) /\ ( dom f)) by A10, A7, XBOOLE_0:def 4;

        then

         A15: c in ( dom (g1 (#) f)) by VALUED_1:def 4;

        c in ( dom f1) by A9, XBOOLE_0:def 4;

        then c in (( dom f1) /\ ( dom g)) by A13, A2, XBOOLE_0:def 4;

        then c in ( dom (f1 (#) g)) by VALUED_1:def 4;

        then c in (( dom (f1 (#) g)) /\ ( dom (g1 (#) f))) by A15, XBOOLE_0:def 4;

        then

         A16: c in ( dom ((f1 (#) g) + (g1 (#) f))) by VALUED_1:def 1;

        c in (( dom (f ^ )) /\ ( dom (g ^ ))) by A10, A13, XBOOLE_0:def 4;

        then c in ( dom ((f ^ ) (#) (g ^ ))) by VALUED_1:def 4;

        then c in ( dom ((f (#) g) ^ )) by Th27;

        then c in (( dom ((f1 (#) g) + (g1 (#) f))) /\ ( dom ((f (#) g) ^ ))) by A16, XBOOLE_0:def 4;

        then c in ( dom (((f1 (#) g) + (g1 (#) f)) (#) ((f (#) g) ^ ))) by VALUED_1:def 4;

        then

         A17: c in ( dom (((f1 (#) g) + (g1 (#) f)) / (f (#) g))) by Th31;



        thus (((f1 / f) + (g1 / g)) . c) = (((f1 / f) . c) + ((g1 / g) . c)) by A3, VALUED_1:def 1

        .= (((f1 . c) * ((f . c) " )) + ((g1 / g) . c)) by A5, Def1

        .= (((f1 . c) * (1 * ((f . c) " ))) + (((g1 . c) * 1) * ((g . c) " ))) by A6, Def1

        .= (((f1 . c) * (((g . c) * ((g . c) " )) * ((f . c) " ))) + ((g1 . c) * (1 * ((g . c) " )))) by A14, XCMPLX_0:def 7

        .= (((f1 . c) * ((g . c) * (((g . c) " ) * ((f . c) " )))) + ((g1 . c) * (((f . c) * ((f . c) " )) * ((g . c) " )))) by A11, XCMPLX_0:def 7

        .= (((f1 . c) * ((g . c) * (((g . c) * (f . c)) " ))) + ((g1 . c) * ((f . c) * (((f . c) " ) * ((g . c) " ))))) by XCMPLX_1: 204

        .= (((f1 . c) * ((g . c) * (((f . c) * (g . c)) " ))) + ((g1 . c) * ((f . c) * (((f . c) * (g . c)) " )))) by XCMPLX_1: 204

        .= (((f1 . c) * ((g . c) * (((f (#) g) . c) " ))) + ((g1 . c) * ((f . c) * (((f . c) * (g . c)) " )))) by VALUED_1: 5

        .= ((((f1 . c) * (g . c)) * (((f (#) g) . c) " )) + ((g1 . c) * ((f . c) * (((f (#) g) . c) " )))) by VALUED_1: 5

        .= ((((f1 (#) g) . c) * (((f (#) g) . c) " )) + (((g1 . c) * (f . c)) * (((f (#) g) . c) " ))) by VALUED_1: 5

        .= ((((f1 (#) g) . c) * (((f (#) g) . c) " )) + (((g1 (#) f) . c) * (((f (#) g) . c) " ))) by VALUED_1: 5

        .= ((((f1 (#) g) . c) + ((g1 (#) f) . c)) * (((f (#) g) . c) " ))

        .= ((((f1 (#) g) + (g1 (#) f)) . c) * (((f (#) g) . c) " )) by A16, VALUED_1:def 1

        .= ((((f1 (#) g) + (g1 (#) f)) / (f (#) g)) . c) by A17, Def1;

      end;

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

      .= ((( dom f1) /\ (( dom f) \ (f " { 0 }))) /\ ( dom (g1 / g))) by Def1

      .= ((( dom f1) /\ (( dom f) \ (f " { 0 }))) /\ (( dom g1) /\ (( dom g) \ (g " { 0 })))) by Def1

      .= ((( dom f1) /\ (( dom f) /\ (( dom f) \ (f " { 0 })))) /\ (( dom g1) /\ (( dom g) \ (g " { 0 })))) by Th1

      .= (((( dom f) /\ (( dom f) \ (f " { 0 }))) /\ ( dom f1)) /\ ((( dom g) /\ (( dom g) \ (g " { 0 }))) /\ ( dom g1))) by Th1

      .= ((( dom f) /\ (( dom f) \ (f " { 0 }))) /\ (( dom f1) /\ ((( dom g) /\ (( dom g) \ (g " { 0 }))) /\ ( dom g1)))) by XBOOLE_1: 16

      .= ((( dom f) /\ (( dom f) \ (f " { 0 }))) /\ ((( dom f1) /\ (( dom g) /\ (( dom g) \ (g " { 0 })))) /\ ( dom g1))) by XBOOLE_1: 16

      .= ((( dom f) /\ (( dom f) \ (f " { 0 }))) /\ (((( dom f1) /\ ( dom g)) /\ (( dom g) \ (g " { 0 }))) /\ ( dom g1))) by XBOOLE_1: 16

      .= ((( dom f) /\ (( dom f) \ (f " { 0 }))) /\ ((( dom (f1 (#) g)) /\ (( dom g) \ (g " { 0 }))) /\ ( dom g1))) by VALUED_1:def 4

      .= ((( dom f) /\ (( dom f) \ (f " { 0 }))) /\ (( dom (f1 (#) g)) /\ (( dom g1) /\ (( dom g) \ (g " { 0 }))))) by XBOOLE_1: 16

      .= (( dom (f1 (#) g)) /\ (((( dom f) \ (f " { 0 })) /\ ( dom f)) /\ (( dom g1) /\ (( dom g) \ (g " { 0 }))))) by XBOOLE_1: 16

      .= (( dom (f1 (#) g)) /\ ((( dom f) \ (f " { 0 })) /\ (( dom f) /\ (( dom g1) /\ (( dom g) \ (g " { 0 })))))) by XBOOLE_1: 16

      .= (( dom (f1 (#) g)) /\ ((( dom f) \ (f " { 0 })) /\ ((( dom g1) /\ ( dom f)) /\ (( dom g) \ (g " { 0 }))))) by XBOOLE_1: 16

      .= (( dom (f1 (#) g)) /\ ((( dom f) \ (f " { 0 })) /\ (( dom (g1 (#) f)) /\ (( dom g) \ (g " { 0 }))))) by VALUED_1:def 4

      .= (( dom (f1 (#) g)) /\ (( dom (g1 (#) f)) /\ ((( dom f) \ (f " { 0 })) /\ (( dom g) \ (g " { 0 }))))) by XBOOLE_1: 16

      .= ((( dom (f1 (#) g)) /\ ( dom (g1 (#) f))) /\ ((( dom f) \ (f " { 0 })) /\ (( dom g) \ (g " { 0 })))) by XBOOLE_1: 16

      .= (( dom ((f1 (#) g) + (g1 (#) f))) /\ ((( dom f) \ (f " { 0 })) /\ (( dom g) \ (g " { 0 })))) by VALUED_1:def 1

      .= (( dom ((f1 (#) g) + (g1 (#) f))) /\ (( dom (f (#) g)) \ ((f (#) g) " { 0 }))) by Th2

      .= ( dom (((f1 (#) g) + (g1 (#) f)) / (f (#) g))) by Def1;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: RFUNCT_1:41

    ((f / g) / (f1 / g1)) = ((f (#) (g1 | ( dom (g1 ^ )))) / (g (#) f1))

    proof



      thus ((f / g) / (f1 / g1)) = ((f / g) (#) ((f1 / g1) ^ )) by Th31

      .= ((f / g) (#) ((g1 | ( dom (g1 ^ ))) / f1)) by Th35

      .= ((f (#) (g1 | ( dom (g1 ^ )))) / (g (#) f1)) by Th34;

    end;

    theorem :: RFUNCT_1:42

    ((f1 / f) - (g1 / g)) = (((f1 (#) g) - (g1 (#) f)) / (f (#) g))

    proof



      thus ((f1 / f) - (g1 / g)) = ((f1 / f) + ((( - 1) (#) g1) / g)) by Th32

      .= (((f1 (#) g) + ((( - 1) (#) g1) (#) f)) / (f (#) g)) by Th40

      .= (((f1 (#) g) - (g1 (#) f)) / (f (#) g)) by Th12;

    end;

    theorem :: RFUNCT_1:43

    ( abs (f1 / f2)) = (( abs f1) / ( abs f2))

    proof



      thus ( abs (f1 / f2)) = ( abs (f1 (#) (f2 ^ ))) by Th31

      .= (( abs f1) (#) ( abs (f2 ^ ))) by Th24

      .= (( abs f1) (#) (( abs f2) ^ )) by Th30

      .= (( abs f1) / ( abs f2)) by Th31;

    end;

    theorem :: RFUNCT_1:44



     Th44: ((f1 + f2) | X) = ((f1 | X) + (f2 | X)) & ((f1 + f2) | X) = ((f1 | X) + f2) & ((f1 + f2) | X) = (f1 + (f2 | X))

    proof

       A1:

      now

        let c be object;

        assume

         A2: c in ( dom ((f1 + f2) | X));

        then

         A3: c in (( dom (f1 + f2)) /\ X) by RELAT_1: 61;

        then

         A4: c in X by XBOOLE_0:def 4;



         A5: c in ( dom (f1 + f2)) by A3, XBOOLE_0:def 4;

        then

         A6: c in (( dom f1) /\ ( dom f2)) by VALUED_1:def 1;

        then c in ( dom f2) by XBOOLE_0:def 4;

        then c in (( dom f2) /\ X) by A4, XBOOLE_0:def 4;

        then

         A7: c in ( dom (f2 | X)) by RELAT_1: 61;

        c in ( dom f1) by A6, XBOOLE_0:def 4;

        then c in (( dom f1) /\ X) by A4, XBOOLE_0:def 4;

        then

         A8: c in ( dom (f1 | X)) by RELAT_1: 61;

        then c in (( dom (f1 | X)) /\ ( dom (f2 | X))) by A7, XBOOLE_0:def 4;

        then

         A9: c in ( dom ((f1 | X) + (f2 | X))) by VALUED_1:def 1;



        thus (((f1 + f2) | X) . c) = ((f1 + f2) . c) by A2, FUNCT_1: 47

        .= ((f1 . c) + (f2 . c)) by A5, VALUED_1:def 1

        .= (((f1 | X) . c) + (f2 . c)) by A8, FUNCT_1: 47

        .= (((f1 | X) . c) + ((f2 | X) . c)) by A7, FUNCT_1: 47

        .= (((f1 | X) + (f2 | X)) . c) by A9, VALUED_1:def 1;

      end;

      ( dom ((f1 + f2) | X)) = (( dom (f1 + f2)) /\ X) by RELAT_1: 61

      .= ((( dom f1) /\ ( dom f2)) /\ (X /\ X)) by VALUED_1:def 1

      .= (( dom f1) /\ (( dom f2) /\ (X /\ X))) by XBOOLE_1: 16

      .= (( dom f1) /\ ((( dom f2) /\ X) /\ X)) by XBOOLE_1: 16

      .= (( dom f1) /\ (X /\ ( dom (f2 | X)))) by RELAT_1: 61

      .= ((( dom f1) /\ X) /\ ( dom (f2 | X))) by XBOOLE_1: 16

      .= (( dom (f1 | X)) /\ ( dom (f2 | X))) by RELAT_1: 61

      .= ( dom ((f1 | X) + (f2 | X))) by VALUED_1:def 1;

      hence ((f1 + f2) | X) = ((f1 | X) + (f2 | X)) by A1, FUNCT_1: 2;

       A10:

      now

        let c be object;

        assume

         A11: c in ( dom ((f1 + f2) | X));

        then

         A12: c in (( dom (f1 + f2)) /\ X) by RELAT_1: 61;

        then

         A13: c in X by XBOOLE_0:def 4;



         A14: c in ( dom (f1 + f2)) by A12, XBOOLE_0:def 4;

        then

         A15: c in (( dom f1) /\ ( dom f2)) by VALUED_1:def 1;

        then c in ( dom f1) by XBOOLE_0:def 4;

        then c in (( dom f1) /\ X) by A13, XBOOLE_0:def 4;

        then

         A16: c in ( dom (f1 | X)) by RELAT_1: 61;

        c in ( dom f2) by A15, XBOOLE_0:def 4;

        then c in (( dom (f1 | X)) /\ ( dom f2)) by A16, XBOOLE_0:def 4;

        then

         A17: c in ( dom ((f1 | X) + f2)) by VALUED_1:def 1;



        thus (((f1 + f2) | X) . c) = ((f1 + f2) . c) by A11, FUNCT_1: 47

        .= ((f1 . c) + (f2 . c)) by A14, VALUED_1:def 1

        .= (((f1 | X) . c) + (f2 . c)) by A16, FUNCT_1: 47

        .= (((f1 | X) + f2) . c) by A17, VALUED_1:def 1;

      end;

      ( dom ((f1 + f2) | X)) = (( dom (f1 + f2)) /\ X) by RELAT_1: 61

      .= ((( dom f1) /\ ( dom f2)) /\ X) by VALUED_1:def 1

      .= ((( dom f1) /\ X) /\ ( dom f2)) by XBOOLE_1: 16

      .= (( dom (f1 | X)) /\ ( dom f2)) by RELAT_1: 61

      .= ( dom ((f1 | X) + f2)) by VALUED_1:def 1;

      hence ((f1 + f2) | X) = ((f1 | X) + f2) by A10, FUNCT_1: 2;

       A18:

      now

        let c be object;

        assume

         A19: c in ( dom ((f1 + f2) | X));

        then

         A20: c in (( dom (f1 + f2)) /\ X) by RELAT_1: 61;

        then

         A21: c in X by XBOOLE_0:def 4;



         A22: c in ( dom (f1 + f2)) by A20, XBOOLE_0:def 4;

        then

         A23: c in (( dom f1) /\ ( dom f2)) by VALUED_1:def 1;

        then c in ( dom f2) by XBOOLE_0:def 4;

        then c in (( dom f2) /\ X) by A21, XBOOLE_0:def 4;

        then

         A24: c in ( dom (f2 | X)) by RELAT_1: 61;

        c in ( dom f1) by A23, XBOOLE_0:def 4;

        then c in (( dom f1) /\ ( dom (f2 | X))) by A24, XBOOLE_0:def 4;

        then

         A25: c in ( dom (f1 + (f2 | X))) by VALUED_1:def 1;



        thus (((f1 + f2) | X) . c) = ((f1 + f2) . c) by A19, FUNCT_1: 47

        .= ((f1 . c) + (f2 . c)) by A22, VALUED_1:def 1

        .= ((f1 . c) + ((f2 | X) . c)) by A24, FUNCT_1: 47

        .= ((f1 + (f2 | X)) . c) by A25, VALUED_1:def 1;

      end;

      ( dom ((f1 + f2) | X)) = (( dom (f1 + f2)) /\ X) by RELAT_1: 61

      .= ((( dom f1) /\ ( dom f2)) /\ X) by VALUED_1:def 1

      .= (( dom f1) /\ (( dom f2) /\ X)) by XBOOLE_1: 16

      .= (( dom f1) /\ ( dom (f2 | X))) by RELAT_1: 61

      .= ( dom (f1 + (f2 | X))) by VALUED_1:def 1;

      hence thesis by A18, FUNCT_1: 2;

    end;

    theorem :: RFUNCT_1:45



     Th45: ((f1 (#) f2) | X) = ((f1 | X) (#) (f2 | X)) & ((f1 (#) f2) | X) = ((f1 | X) (#) f2) & ((f1 (#) f2) | X) = (f1 (#) (f2 | X))

    proof

       A1:

      now

        let c be object;

        assume

         A2: c in ( dom ((f1 (#) f2) | X));

        then

         A3: c in (( dom (f1 (#) f2)) /\ X) by RELAT_1: 61;

        then

         A4: c in X by XBOOLE_0:def 4;

        c in ( dom (f1 (#) f2)) by A3, XBOOLE_0:def 4;

        then

         A5: c in (( dom f1) /\ ( dom f2)) by VALUED_1:def 4;

        then c in ( dom f1) by XBOOLE_0:def 4;

        then c in (( dom f1) /\ X) by A4, XBOOLE_0:def 4;

        then

         A6: c in ( dom (f1 | X)) by RELAT_1: 61;

        c in ( dom f2) by A5, XBOOLE_0:def 4;

        then c in (( dom f2) /\ X) by A4, XBOOLE_0:def 4;

        then

         A7: c in ( dom (f2 | X)) by RELAT_1: 61;



        thus (((f1 (#) f2) | X) . c) = ((f1 (#) f2) . c) by A2, FUNCT_1: 47

        .= ((f1 . c) * (f2 . c)) by VALUED_1: 5

        .= (((f1 | X) . c) * (f2 . c)) by A6, FUNCT_1: 47

        .= (((f1 | X) . c) * ((f2 | X) . c)) by A7, FUNCT_1: 47

        .= (((f1 | X) (#) (f2 | X)) . c) by VALUED_1: 5;

      end;

      ( dom ((f1 (#) f2) | X)) = (( dom (f1 (#) f2)) /\ X) by RELAT_1: 61

      .= ((( dom f1) /\ ( dom f2)) /\ (X /\ X)) by VALUED_1:def 4

      .= (( dom f1) /\ (( dom f2) /\ (X /\ X))) by XBOOLE_1: 16

      .= (( dom f1) /\ ((( dom f2) /\ X) /\ X)) by XBOOLE_1: 16

      .= (( dom f1) /\ (X /\ ( dom (f2 | X)))) by RELAT_1: 61

      .= ((( dom f1) /\ X) /\ ( dom (f2 | X))) by XBOOLE_1: 16

      .= (( dom (f1 | X)) /\ ( dom (f2 | X))) by RELAT_1: 61

      .= ( dom ((f1 | X) (#) (f2 | X))) by VALUED_1:def 4;

      hence ((f1 (#) f2) | X) = ((f1 | X) (#) (f2 | X)) by A1, FUNCT_1: 2;

       A8:

      now

        let c be object;

        assume

         A9: c in ( dom ((f1 (#) f2) | X));

        then

         A10: c in (( dom (f1 (#) f2)) /\ X) by RELAT_1: 61;

        then c in ( dom (f1 (#) f2)) by XBOOLE_0:def 4;

        then c in (( dom f1) /\ ( dom f2)) by VALUED_1:def 4;

        then

         A11: c in ( dom f1) by XBOOLE_0:def 4;

        c in X by A10, XBOOLE_0:def 4;

        then c in (( dom f1) /\ X) by A11, XBOOLE_0:def 4;

        then

         A12: c in ( dom (f1 | X)) by RELAT_1: 61;



        thus (((f1 (#) f2) | X) . c) = ((f1 (#) f2) . c) by A9, FUNCT_1: 47

        .= ((f1 . c) * (f2 . c)) by VALUED_1: 5

        .= (((f1 | X) . c) * (f2 . c)) by A12, FUNCT_1: 47

        .= (((f1 | X) (#) f2) . c) by VALUED_1: 5;

      end;

      ( dom ((f1 (#) f2) | X)) = (( dom (f1 (#) f2)) /\ X) by RELAT_1: 61

      .= ((( dom f1) /\ ( dom f2)) /\ X) by VALUED_1:def 4

      .= ((( dom f1) /\ X) /\ ( dom f2)) by XBOOLE_1: 16

      .= (( dom (f1 | X)) /\ ( dom f2)) by RELAT_1: 61

      .= ( dom ((f1 | X) (#) f2)) by VALUED_1:def 4;

      hence ((f1 (#) f2) | X) = ((f1 | X) (#) f2) by A8, FUNCT_1: 2;

       A13:

      now

        let c be object;

        assume

         A14: c in ( dom ((f1 (#) f2) | X));

        then

         A15: c in (( dom (f1 (#) f2)) /\ X) by RELAT_1: 61;

        then c in ( dom (f1 (#) f2)) by XBOOLE_0:def 4;

        then c in (( dom f1) /\ ( dom f2)) by VALUED_1:def 4;

        then

         A16: c in ( dom f2) by XBOOLE_0:def 4;

        c in X by A15, XBOOLE_0:def 4;

        then c in (( dom f2) /\ X) by A16, XBOOLE_0:def 4;

        then

         A17: c in ( dom (f2 | X)) by RELAT_1: 61;



        thus (((f1 (#) f2) | X) . c) = ((f1 (#) f2) . c) by A14, FUNCT_1: 47

        .= ((f1 . c) * (f2 . c)) by VALUED_1: 5

        .= ((f1 . c) * ((f2 | X) . c)) by A17, FUNCT_1: 47

        .= ((f1 (#) (f2 | X)) . c) by VALUED_1: 5;

      end;

      ( dom ((f1 (#) f2) | X)) = (( dom (f1 (#) f2)) /\ X) by RELAT_1: 61

      .= ((( dom f1) /\ ( dom f2)) /\ X) by VALUED_1:def 4

      .= (( dom f1) /\ (( dom f2) /\ X)) by XBOOLE_1: 16

      .= (( dom f1) /\ ( dom (f2 | X))) by RELAT_1: 61

      .= ( dom (f1 (#) (f2 | X))) by VALUED_1:def 4;

      hence thesis by A13, FUNCT_1: 2;

    end;

    theorem :: RFUNCT_1:46



     Th46: (( - f) | X) = ( - (f | X)) & ((f ^ ) | X) = ((f | X) ^ ) & (( abs f) | X) = ( abs (f | X))

    proof

       A1:

      now

        let c be object;

        assume

         A2: c in ( dom (( - f) | X));

        then

         A3: c in (( dom ( - f)) /\ X) by RELAT_1: 61;

        then c in ( dom ( - f)) by XBOOLE_0:def 4;

        then

         A4: c in ( dom f) by VALUED_1: 8;

        c in X by A3, XBOOLE_0:def 4;

        then c in (( dom f) /\ X) by A4, XBOOLE_0:def 4;

        then

         A5: c in ( dom (f | X)) by RELAT_1: 61;



        thus ((( - f) | X) . c) = (( - f) . c) by A2, FUNCT_1: 47

        .= ( - (f . c)) by VALUED_1: 8

        .= ( - ((f | X) . c)) by A5, FUNCT_1: 47

        .= (( - (f | X)) . c) by VALUED_1: 8;

      end;

      ( dom (( - f) | X)) = (( dom ( - f)) /\ X) by RELAT_1: 61

      .= (( dom f) /\ X) by VALUED_1: 8

      .= ( dom (f | X)) by RELAT_1: 61

      .= ( dom ( - (f | X))) by VALUED_1: 8;

      hence (( - f) | X) = ( - (f | X)) by A1, FUNCT_1: 2;



       A6: ( dom ((f ^ ) | X)) = (( dom (f ^ )) /\ X) by RELAT_1: 61

      .= ((( dom f) \ (f " { 0 })) /\ X) by Def2

      .= ((( dom f) /\ X) \ ((f " { 0 }) /\ X)) by XBOOLE_1: 50

      .= (( dom (f | X)) \ (X /\ (f " { 0 }))) by RELAT_1: 61

      .= (( dom (f | X)) \ ((f | X) " { 0 })) by FUNCT_1: 70

      .= ( dom ((f | X) ^ )) by Def2;



       A7: ( dom ((f | X) ^ )) c= ( dom (f | X)) by Th1;

      now

        let c be object;

        assume

         A8: c in ( dom ((f ^ ) | X));

        then c in (( dom (f ^ )) /\ X) by RELAT_1: 61;

        then

         A9: c in ( dom (f ^ )) by XBOOLE_0:def 4;



        thus (((f ^ ) | X) . c) = ((f ^ ) . c) by A8, FUNCT_1: 47

        .= ((f . c) " ) by A9, Def2

        .= (((f | X) . c) " ) by A7, A6, A8, FUNCT_1: 47

        .= (((f | X) ^ ) . c) by A6, A8, Def2;

      end;

      hence ((f ^ ) | X) = ((f | X) ^ ) by A6, FUNCT_1: 2;



       A10: ( dom (( abs f) | X)) = (( dom ( abs f)) /\ X) by RELAT_1: 61

      .= (( dom f) /\ X) by VALUED_1:def 11

      .= ( dom (f | X)) by RELAT_1: 61

      .= ( dom ( abs (f | X))) by VALUED_1:def 11;

      now

        let c be object;

        assume

         A11: c in ( dom (( abs f) | X));

        then

         A12: c in ( dom (f | X)) by A10, VALUED_1:def 11;



        thus ((( abs f) | X) . c) = (( abs f) . c) by A11, FUNCT_1: 47

        .= |.(f . c).| by VALUED_1: 18

        .= |.((f | X) . c).| by A12, FUNCT_1: 47

        .= (( abs (f | X)) . c) by VALUED_1: 18;

      end;

      hence thesis by A10, FUNCT_1: 2;

    end;

    theorem :: RFUNCT_1:47

    ((f1 - f2) | X) = ((f1 | X) - (f2 | X)) & ((f1 - f2) | X) = ((f1 | X) - f2) & ((f1 - f2) | X) = (f1 - (f2 | X))

    proof



      thus ((f1 - f2) | X) = ((f1 | X) + (( - f2) | X)) by Th44

      .= ((f1 | X) - (f2 | X)) by Th46;

      thus ((f1 - f2) | X) = ((f1 | X) - f2) by Th44;



      thus ((f1 - f2) | X) = (f1 + (( - f2) | X)) by Th44

      .= (f1 - (f2 | X)) by Th46;

    end;

    theorem :: RFUNCT_1:48

    ((f1 / f2) | X) = ((f1 | X) / (f2 | X)) & ((f1 / f2) | X) = ((f1 | X) / f2) & ((f1 / f2) | X) = (f1 / (f2 | X))

    proof



      thus ((f1 / f2) | X) = ((f1 (#) (f2 ^ )) | X) by Th31

      .= ((f1 | X) (#) ((f2 ^ ) | X)) by Th45

      .= ((f1 | X) (#) ((f2 | X) ^ )) by Th46

      .= ((f1 | X) / (f2 | X)) by Th31;



      thus ((f1 / f2) | X) = ((f1 (#) (f2 ^ )) | X) by Th31

      .= ((f1 | X) (#) (f2 ^ )) by Th45

      .= ((f1 | X) / f2) by Th31;



      thus ((f1 / f2) | X) = ((f1 (#) (f2 ^ )) | X) by Th31

      .= (f1 (#) ((f2 ^ ) | X)) by Th45

      .= (f1 (#) ((f2 | X) ^ )) by Th46

      .= (f1 / (f2 | X)) by Th31;

    end;

    theorem :: RFUNCT_1:49



     Th49: ((r (#) f) | X) = (r (#) (f | X))

    proof

       A1:

      now

        let c be object;

        assume

         A2: c in ( dom ((r (#) f) | X));

        then

         A3: c in (( dom (r (#) f)) /\ X) by RELAT_1: 61;

        then

         A4: c in X by XBOOLE_0:def 4;



         A5: c in ( dom (r (#) f)) by A3, XBOOLE_0:def 4;

        then c in ( dom f) by VALUED_1:def 5;

        then c in (( dom f) /\ X) by A4, XBOOLE_0:def 4;

        then

         A6: c in ( dom (f | X)) by RELAT_1: 61;

        then

         A7: c in ( dom (r (#) (f | X))) by VALUED_1:def 5;



        thus (((r (#) f) | X) . c) = ((r (#) f) . c) by A2, FUNCT_1: 47

        .= (r * (f . c)) by A5, VALUED_1:def 5

        .= (r * ((f | X) . c)) by A6, FUNCT_1: 47

        .= ((r (#) (f | X)) . c) by A7, VALUED_1:def 5;

      end;

      ( dom ((r (#) f) | X)) = (( dom (r (#) f)) /\ X) by RELAT_1: 61

      .= (( dom f) /\ X) by VALUED_1:def 5

      .= ( dom (f | X)) by RELAT_1: 61

      .= ( dom (r (#) (f | X))) by VALUED_1:def 5;

      hence thesis by A1, FUNCT_1: 2;

    end;

    reserve r,r1,r2,p for Real;

    reserve f,f1,f2 for PartFunc of C, REAL ;

    theorem :: RFUNCT_1:50



     Th50: (f1 is total & f2 is total iff (f1 + f2) is total) & (f1 is total & f2 is total iff (f1 - f2) is total) & (f1 is total & f2 is total iff (f1 (#) f2) is total)

    proof

      thus f1 is total & f2 is total iff (f1 + f2) is total

      proof

        thus f1 is total & f2 is total implies (f1 + f2) is total;

        assume (f1 + f2) is total;

        then ( dom (f1 + f2)) = C;

        then

         A1: (( dom f1) /\ ( dom f2)) = C by VALUED_1:def 1;

        then

         A2: C c= ( dom f2) by XBOOLE_1: 17;

        C c= ( dom f1) by A1, XBOOLE_1: 17;

        hence ( dom f1) = C & ( dom f2) = C by A2;

      end;

      thus f1 is total & f2 is total iff (f1 - f2) is total

      proof

        thus f1 is total & f2 is total implies (f1 - f2) is total;

        assume (f1 - f2) is total;

        then ( dom (f1 - f2)) = C;

        then

         A3: (( dom f1) /\ ( dom f2)) = C by VALUED_1: 12;

        then

         A4: C c= ( dom f2) by XBOOLE_1: 17;

        C c= ( dom f1) by A3, XBOOLE_1: 17;

        hence ( dom f1) = C & ( dom f2) = C by A4;

      end;

      thus f1 is total & f2 is total implies (f1 (#) f2) is total;

      assume (f1 (#) f2) is total;

      then ( dom (f1 (#) f2)) = C;

      then

       A5: (( dom f1) /\ ( dom f2)) = C by VALUED_1:def 4;

      then

       A6: C c= ( dom f2) by XBOOLE_1: 17;

      C c= ( dom f1) by A5, XBOOLE_1: 17;

      hence ( dom f1) = C & ( dom f2) = C by A6;

    end;

    theorem :: RFUNCT_1:51



     Th51: f is total iff (r (#) f) is total by VALUED_1:def 5;

    theorem :: RFUNCT_1:52

    f is total iff ( - f) is total by Th51;

    theorem :: RFUNCT_1:53

    f is total iff ( abs f) is total by VALUED_1:def 11;

    theorem :: RFUNCT_1:54



     Th54: (f ^ ) is total iff (f " { 0 }) = {} & f is total

    proof

      thus (f ^ ) is total implies (f " { 0 }) = {} & f is total

      proof

        assume (f ^ ) is total;

        then

         A1: ( dom (f ^ )) = C;

        (f " { 0 }) c= C;

        then (f " { 0 }) c= (( dom f) \ (f " { 0 })) by A1, Def2;

        hence (f " { 0 }) = {} by XBOOLE_1: 38;

        then C = (( dom f) \ {} ) by A1, Def2;

        hence ( dom f) = C;

      end;

      assume that

       A2: (f " { 0 }) = {} and

       A3: f is total;



      thus ( dom (f ^ )) = (( dom f) \ (f " { 0 })) by Def2

      .= C by A2, A3;

    end;

    theorem :: RFUNCT_1:55



     Th55: f1 is total & (f2 " { 0 }) = {} & f2 is total iff (f1 / f2) is total

    proof

      thus f1 is total & (f2 " { 0 }) = {} & f2 is total implies (f1 / f2) is total

      proof

        assume that

         A1: f1 is total and

         A2: (f2 " { 0 }) = {} and

         A3: f2 is total;

        (f2 ^ ) is total by A2, A3, Th54;

        then (f1 (#) (f2 ^ )) is total by A1;

        hence thesis by Th31;

      end;

      assume (f1 / f2) is total;

      then

       A4: (f1 (#) (f2 ^ )) is total by Th31;

      hence f1 is total by Th50;

      (f2 ^ ) is total by A4, Th50;

      hence thesis by Th54;

    end;

    theorem :: RFUNCT_1:56

    f1 is total & f2 is total implies ((f1 + f2) . c) = ((f1 . c) + (f2 . c)) & ((f1 - f2) . c) = ((f1 . c) - (f2 . c)) & ((f1 (#) f2) . c) = ((f1 . c) * (f2 . c))

    proof

      assume that

       A1: f1 is total and

       A2: f2 is total;

      (f1 + f2) is total by A1, A2;

      then ( dom (f1 + f2)) = C;

      hence ((f1 + f2) . c) = ((f1 . c) + (f2 . c)) by VALUED_1:def 1;

      (f1 - f2) is total by A1, A2;

      then ( dom (f1 - f2)) = C;

      hence ((f1 - f2) . c) = ((f1 . c) - (f2 . c)) by VALUED_1: 13;

      thus thesis by VALUED_1: 5;

    end;

    theorem :: RFUNCT_1:57

    f is total implies ((r (#) f) . c) = (r * (f . c))

    proof

      assume f is total;

      then (r (#) f) is total;

      then ( dom (r (#) f)) = C;

      hence thesis by VALUED_1:def 5;

    end;

    theorem :: RFUNCT_1:58

    f is total implies (( - f) . c) = ( - (f . c)) & (( abs f) . c) = |.(f . c).| by VALUED_1: 8, VALUED_1: 18;

    theorem :: RFUNCT_1:59

    (f ^ ) is total implies ((f ^ ) . c) = ((f . c) " ) by Def2;

    theorem :: RFUNCT_1:60

    f1 is total & (f2 ^ ) is total implies ((f1 / f2) . c) = ((f1 . c) * ((f2 . c) " ))

    proof

      assume that

       A1: f1 is total and

       A2: (f2 ^ ) is total;



       A3: f2 is total by A2, Th54;

      (f2 " { 0 }) = {} by A2, Th54;

      then (f1 / f2) is total by A1, A3, Th55;

      then ( dom (f1 / f2)) = C;

      hence thesis by Def1;

    end;

    definition

      let X,C be set;

      :: original: chi

      redefine

      func chi (X,C) -> PartFunc of C, REAL ;

      coherence

      proof

        for x be object st x in ( rng ( chi (X,C))) holds x in REAL by XREAL_0:def 1;

        then

         A1: ( rng ( chi (X,C))) c= REAL ;

        ( dom ( chi (X,C))) = C by FUNCT_3:def 3;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    registration

      let X,C be set;

      cluster ( chi (X,C)) -> total;

      coherence by FUNCT_3:def 3;

    end

    theorem :: RFUNCT_1:61



     Th61: f = ( chi (X,C)) iff (( dom f) = C & for c holds (c in X implies (f . c) = 1) & ( not c in X implies (f . c) = 0 ))

    proof

      thus f = ( chi (X,C)) implies (( dom f) = C & for c holds (c in X implies (f . c) = 1) & ( not c in X implies (f . c) = 0 )) by FUNCT_3:def 3;

      assume that

       A1: ( dom f) = C and

       A2: for c holds (c in X implies (f . c) = 1) & ( not c in X implies (f . c) = 0 );

      for x st x in C holds (x in X implies (f qua Function . x) = 1) & ( not x in X implies (f qua Function . x) = 0 ) by A2;

      hence thesis by A1, FUNCT_3:def 3;

    end;

    theorem :: RFUNCT_1:62

    ( chi (X,C)) is total;

    theorem :: RFUNCT_1:63

    c in X iff (( chi (X,C)) . c) = 1 by Th61;

    theorem :: RFUNCT_1:64

     not c in X iff (( chi (X,C)) . c) = 0 by Th61;

    theorem :: RFUNCT_1:65

    c in (C \ X) iff (( chi (X,C)) . c) = 0

    proof

      thus c in (C \ X) implies (( chi (X,C)) . c) = 0

      proof

        assume c in (C \ X);

        then not c in X by XBOOLE_0:def 5;

        hence thesis by Th61;

      end;

      assume (( chi (X,C)) . c) = 0 ;

      then not c in X by Th61;

      hence thesis by XBOOLE_0:def 5;

    end;

    theorem :: RFUNCT_1:66

    (( chi (C,C)) . c) = 1 by Th61;

    theorem :: RFUNCT_1:67



     Th67: (( chi (X,C)) . c) <> 1 iff (( chi (X,C)) . c) = 0 by Th61;

    theorem :: RFUNCT_1:68

    X misses Y implies (( chi (X,C)) + ( chi (Y,C))) = ( chi ((X \/ Y),C))

    proof

      assume

       A1: (X /\ Y) = {} ;

       A2:

      now

        let c such that

         A3: c in ( dom (( chi (X,C)) + ( chi (Y,C))));

        now

          per cases ;

            suppose

             A4: c in X;

            then not c in Y by A1, XBOOLE_0:def 4;

            then

             A5: (( chi (Y,C)) . c) = 0 by Th61;



             A6: c in (X \/ Y) by A4, XBOOLE_0:def 3;

            (( chi (X,C)) . c) = 1 by A4, Th61;

            hence ((( chi (X,C)) . c) + (( chi (Y,C)) . c)) = (( chi ((X \/ Y),C)) . c) by A5, A6, Th61;

          end;

            suppose

             A7: not c in X;

            then

             A8: (( chi (X,C)) . c) = 0 by Th61;

            now

              per cases ;

                suppose

                 A9: c in Y;

                then

                 A10: c in (X \/ Y) by XBOOLE_0:def 3;

                (( chi (Y,C)) . c) = 1 by A9, Th61;

                hence ((( chi (X,C)) . c) + (( chi (Y,C)) . c)) = (( chi ((X \/ Y),C)) . c) by A8, A10, Th61;

              end;

                suppose

                 A11: not c in Y;

                then

                 A12: not c in (X \/ Y) by A7, XBOOLE_0:def 3;

                (( chi (Y,C)) . c) = 0 by A11, Th61;

                hence ((( chi (X,C)) . c) + (( chi (Y,C)) . c)) = (( chi ((X \/ Y),C)) . c) by A8, A12, Th61;

              end;

            end;

            hence ((( chi (X,C)) . c) + (( chi (Y,C)) . c)) = (( chi ((X \/ Y),C)) . c);

          end;

        end;

        hence ((( chi (X,C)) + ( chi (Y,C))) . c) = (( chi ((X \/ Y),C)) . c) by A3, VALUED_1:def 1;

      end;

      ( dom (( chi (X,C)) + ( chi (Y,C)))) = (( dom ( chi (X,C))) /\ ( dom ( chi (Y,C)))) by VALUED_1:def 1

      .= (C /\ ( dom ( chi (Y,C)))) by Th61

      .= (C /\ C) by Th61

      .= ( dom ( chi ((X \/ Y),C))) by Th61;

      hence thesis by A2, PARTFUN1: 5;

    end;

    theorem :: RFUNCT_1:69

    (( chi (X,C)) (#) ( chi (Y,C))) = ( chi ((X /\ Y),C))

    proof

       A1:

      now

        let c such that c in ( dom (( chi (X,C)) (#) ( chi (Y,C))));

        now

          per cases ;

            suppose

             A2: ((( chi (X,C)) . c) * (( chi (Y,C)) . c)) = 0 ;

            now

              per cases by A2;

                suppose (( chi (X,C)) . c) = 0 ;

                then not c in X by Th61;

                then not c in (X /\ Y) by XBOOLE_0:def 4;

                hence ((( chi (X,C)) . c) * (( chi (Y,C)) . c)) = (( chi ((X /\ Y),C)) . c) by A2, Th61;

              end;

                suppose (( chi (Y,C)) . c) = 0 ;

                then not c in Y by Th61;

                then not c in (X /\ Y) by XBOOLE_0:def 4;

                hence ((( chi (X,C)) . c) * (( chi (Y,C)) . c)) = (( chi ((X /\ Y),C)) . c) by A2, Th61;

              end;

            end;

            hence ((( chi (X,C)) . c) * (( chi (Y,C)) . c)) = (( chi ((X /\ Y),C)) . c);

          end;

            suppose

             A3: ((( chi (X,C)) . c) * (( chi (Y,C)) . c)) <> 0 ;

            then

             A4: (( chi (Y,C)) . c) <> 0 ;

            then

             A5: (( chi (Y,C)) . c) = 1 by Th67;



             A6: c in Y by A4, Th61;



             A7: (( chi (X,C)) . c) <> 0 by A3;

            then c in X by Th61;

            then

             A8: c in (X /\ Y) by A6, XBOOLE_0:def 4;

            (( chi (X,C)) . c) = 1 by A7, Th67;

            hence ((( chi (X,C)) . c) * (( chi (Y,C)) . c)) = (( chi ((X /\ Y),C)) . c) by A5, A8, Th61;

          end;

        end;

        hence ((( chi (X,C)) (#) ( chi (Y,C))) . c) = (( chi ((X /\ Y),C)) . c) by VALUED_1: 5;

      end;

      ( dom (( chi (X,C)) (#) ( chi (Y,C)))) = (( dom ( chi (X,C))) /\ ( dom ( chi (Y,C)))) by VALUED_1:def 4

      .= (C /\ ( dom ( chi (Y,C)))) by Th61

      .= (C /\ C) by Th61

      .= ( dom ( chi ((X /\ Y),C))) by Th61;

      hence thesis by A1, PARTFUN1: 5;

    end;

    reserve f for real-valued Function;

    theorem :: RFUNCT_1:70



     Th70: (f | Y) is bounded_above iff ex r st for c be object st c in (Y /\ ( dom f)) holds (f . c) <= r

    proof

      thus (f | Y) is bounded_above implies ex r st for c be object st c in (Y /\ ( dom f)) holds (f . c) <= r

      proof

        given r be Real such that

         A1: for p be object st p in ( dom (f | Y)) holds ((f | Y) . p) < r;

        take r;

        let c be object;

        assume c in (Y /\ ( dom f));

        then

         A2: c in ( dom (f | Y)) by RELAT_1: 61;

        then ((f | Y) . c) < r by A1;

        hence thesis by A2, FUNCT_1: 47;

      end;

      given r such that

       A3: for c be object st c in (Y /\ ( dom f)) holds (f . c) <= r;

      reconsider r1 = (r + 1) as Real;

      take r1;

      let p be object;

      assume

       A4: p in ( dom (f | Y));

      then p in (Y /\ ( dom f)) by RELAT_1: 61;

      then (f . p) <= r by A3;

      then

       A5: ((f | Y) . p) <= r by A4, FUNCT_1: 47;

      r < r1 by XREAL_1: 29;

      hence thesis by A5, XXREAL_0: 2;

    end;

    theorem :: RFUNCT_1:71



     Th71: (f | Y) is bounded_below iff ex r st for c be object st c in (Y /\ ( dom f)) holds r <= (f . c)

    proof

      thus (f | Y) is bounded_below implies ex r st for c be object st c in (Y /\ ( dom f)) holds r <= (f . c)

      proof

        given r be Real such that

         A1: for p be object st p in ( dom (f | Y)) holds r < ((f | Y) . p);

        take r;

        let c be object;

        assume c in (Y /\ ( dom f));

        then

         A2: c in ( dom (f | Y)) by RELAT_1: 61;

        then r < ((f | Y) . c) by A1;

        hence thesis by A2, FUNCT_1: 47;

      end;

      given r such that

       A3: for c be object st c in (Y /\ ( dom f)) holds r <= (f . c);

      reconsider r1 = (r - 1) as Real;

      take r1;

      let p be object;

      assume

       A4: p in ( dom (f | Y));

      then p in (Y /\ ( dom f)) by RELAT_1: 61;

      then r <= (f . p) by A3;

      then

       A5: r <= ((f | Y) . p) by A4, FUNCT_1: 47;

      r1 < r by XREAL_1: 44;

      hence thesis by A5, XXREAL_0: 2;

    end;

    theorem :: RFUNCT_1:72



     Th72: f is bounded iff ex r st for c be object st c in ( dom f) holds |.(f . c).| <= r

    proof

      thus f is bounded implies ex r st for c be object st c in ( dom f) holds |.(f . c).| <= r

      proof

        assume

         A1: f is bounded;

        then

        consider r1 such that

         A2: for c be object st c in ( dom f) holds (f . c) < r1 by SEQ_2:def 1;

        consider r2 such that

         A3: for c be object st c in ( dom f) holds r2 < (f . c) by A1, SEQ_2:def 2;

        take g = ( |.r1.| + |.r2.|);

        let c be object such that

         A4: c in ( dom f);



         A5: 0 <= |.r2.| by COMPLEX1: 46;

        r1 <= |.r1.| by ABSVALUE: 4;

        then (f . c) <= |.r1.| by A2, A4, XXREAL_0: 2;

        then

         A6: ((f . c) + 0 qua Real) <= ( |.r1.| + |.r2.|) by A5, XREAL_1: 7;



         A7: 0 <= |.r1.| by COMPLEX1: 46;

        ( - |.r2.|) <= r2 by ABSVALUE: 4;

        then ( - |.r2.|) <= (f . c) by A3, A4, XXREAL_0: 2;

        then

         A8: (( - |.r1.|) + ( - |.r2.|)) <= ( 0 qua Real + (f . c)) by A7, XREAL_1: 7;

        (( - |.r1.|) + ( - |.r2.|)) = ( - g);

        hence thesis by A6, A8, ABSVALUE: 5;

      end;

      given r such that

       A9: for c be object st c in ( dom f) holds |.(f . c).| <= r;

      thus f is bounded_above

      proof

        take (r + 1);

        let c be object;

        assume c in ( dom f);

        then

         A10: |.(f . c).| < (r + 1) by A9, XREAL_1: 39;

        (f . c) <= |.(f . c).| by ABSVALUE: 4;

        hence thesis by A10, XXREAL_0: 2;

      end;

      take ( - (r + 1));

      let c be object;

      assume c in ( dom f);

      then |.(f . c).| < (r + 1) by A9, XREAL_1: 39;

      then

       A11: ( - (r + 1)) < ( - |.(f . c).|) by XREAL_1: 24;

      ( - |.(f . c).|) <= (f . c) by ABSVALUE: 4;

      hence thesis by A11, XXREAL_0: 2;

    end;

    theorem :: RFUNCT_1:73

    (f | Y) is bounded iff ex r st for c be object st c in (Y /\ ( dom f)) holds |.(f . c).| <= r

    proof

      thus (f | Y) is bounded implies ex r st for c be object st c in (Y /\ ( dom f)) holds |.(f . c).| <= r

      proof

        assume

         A1: (f | Y) is bounded;

        then

        consider r1 such that

         A2: for c be object st c in (Y /\ ( dom f)) holds (f . c) <= r1 by Th70;

        consider r2 such that

         A3: for c be object st c in (Y /\ ( dom f)) holds r2 <= (f . c) by A1, Th71;

        take g = ( |.r1.| + |.r2.|);



         A4: r1 <= |.r1.| by ABSVALUE: 4;

        let c be object such that

         A5: c in (Y /\ ( dom f));

        (f . c) <= r1 by A2, A5;

        then

         A6: (f . c) <= |.r1.| by A4, XXREAL_0: 2;



         A7: ( - |.r2.|) <= r2 by ABSVALUE: 4;

        r2 <= (f . c) by A3, A5;

        then

         A8: ( - |.r2.|) <= (f . c) by A7, XXREAL_0: 2;

         0 <= |.r1.| by COMPLEX1: 46;

        then

         A9: (( - |.r1.|) + ( - |.r2.|)) <= ( 0 qua Real + (f . c)) by A8, XREAL_1: 7;

         0 <= |.r2.| by COMPLEX1: 46;

        then

         A10: ((f . c) + 0 qua Real) <= ( |.r1.| + |.r2.|) by A6, XREAL_1: 7;

        (( - |.r1.|) + ( - |.r2.|)) = ( - g);

        hence thesis by A10, A9, ABSVALUE: 5;

      end;

      given r such that

       A11: for c be object st c in (Y /\ ( dom f)) holds |.(f . c).| <= r;

      now

        let c be object;

        assume c in (Y /\ ( dom f));

        then |.(f . c).| <= r by A11;

        then

         A12: ( - r) <= ( - |.(f . c).|) by XREAL_1: 24;

        ( - |.(f . c).|) <= (f . c) by ABSVALUE: 4;

        hence ( - r) <= (f . c) by A12, XXREAL_0: 2;

      end;

      then

       A13: (f | Y) is bounded_below by Th71;

      now

        let c be object;

        assume c in (Y /\ ( dom f));

        then

         A14: |.(f . c).| <= r by A11;

        (f . c) <= |.(f . c).| by ABSVALUE: 4;

        hence (f . c) <= r by A14, XXREAL_0: 2;

      end;

      then (f | Y) is bounded_above by Th70;

      hence thesis by A13;

    end;

    theorem :: RFUNCT_1:74

    (Y c= X & (f | X) is bounded_above implies (f | Y) is bounded_above) & (Y c= X & (f | X) is bounded_below implies (f | Y) is bounded_below) & (Y c= X & (f | X) is bounded implies (f | Y) is bounded)

    proof

      thus

       A1: Y c= X & (f | X) is bounded_above implies (f | Y) is bounded_above

      proof

        assume that

         A2: Y c= X and

         A3: (f | X) is bounded_above;

        consider r such that

         A4: for c be object st c in (X /\ ( dom f)) holds (f . c) <= r by A3, Th70;

        now

          take r;

          let c be object;

          assume

           A5: c in (Y /\ ( dom f));

          then

           A6: c in ( dom f) by XBOOLE_0:def 4;

          c in Y by A5, XBOOLE_0:def 4;

          then c in (X /\ ( dom f)) by A2, A6, XBOOLE_0:def 4;

          hence (f . c) <= r by A4;

        end;

        hence thesis by Th70;

      end;

      thus

       A7: Y c= X & (f | X) is bounded_below implies (f | Y) is bounded_below

      proof

        assume that

         A8: Y c= X and

         A9: (f | X) is bounded_below;

        consider r such that

         A10: for c be object st c in (X /\ ( dom f)) holds r <= (f . c) by A9, Th71;

        now

          take r;

          let c be object;

          assume

           A11: c in (Y /\ ( dom f));

          then

           A12: c in ( dom f) by XBOOLE_0:def 4;

          c in Y by A11, XBOOLE_0:def 4;

          then c in (X /\ ( dom f)) by A8, A12, XBOOLE_0:def 4;

          hence r <= (f . c) by A10;

        end;

        hence thesis by Th71;

      end;

      assume that

       A13: Y c= X and

       A14: (f | X) is bounded;

      thus thesis by A1, A7, A13, A14;

    end;

    theorem :: RFUNCT_1:75

    (f | X) is bounded_above & (f | Y) is bounded_below implies (f | (X /\ Y)) is bounded

    proof

      assume that

       A1: (f | X) is bounded_above and

       A2: (f | Y) is bounded_below;

      consider r1 such that

       A3: for c be object st c in (X /\ ( dom f)) holds (f . c) <= r1 by A1, Th70;

      now

        let c be object;

        assume

         A4: c in ((X /\ Y) /\ ( dom f));

        then c in (X /\ Y) by XBOOLE_0:def 4;

        then

         A5: c in X by XBOOLE_0:def 4;

        c in ( dom f) by A4, XBOOLE_0:def 4;

        then c in (X /\ ( dom f)) by A5, XBOOLE_0:def 4;

        hence (f . c) <= r1 by A3;

      end;

      hence (f | (X /\ Y)) is bounded_above by Th70;

      consider r2 such that

       A6: for c be object st c in (Y /\ ( dom f)) holds r2 <= (f . c) by A2, Th71;

      now

        let c be object;

        assume

         A7: c in ((X /\ Y) /\ ( dom f));

        then c in (X /\ Y) by XBOOLE_0:def 4;

        then

         A8: c in Y by XBOOLE_0:def 4;

        c in ( dom f) by A7, XBOOLE_0:def 4;

        then c in (Y /\ ( dom f)) by A8, XBOOLE_0:def 4;

        hence r2 <= (f . c) by A6;

      end;

      hence thesis by Th71;

    end;

    registration

      cluster constant -> bounded for real-valued Function;

      coherence

      proof

        let f be real-valued Function;

        per cases ;

          suppose

           A1: f is empty;

          reconsider z = 0 as Real;

          assume f is constant;

          thus f is bounded_above

          proof

            take z;

            let x be object;

            thus thesis by A1;

          end;

          take z;

          let x be object;

          thus thesis by A1;

        end;

          suppose

           A2: not f is empty;

          assume f is constant;

          then

          consider r such that

           A3: for c be object st c in ( dom f) holds (f . c) = r by A2, VALUED_0: 15;

          thus f is bounded_above

          proof

            take (r + 1);

            let y be object;

            assume y in ( dom f);

            then (f . y) = r by A3;

            hence thesis by XREAL_1: 39;

          end;

          take (r - 1);

          let y be object;

          assume y in ( dom f);

          then (f . y) = r by A3;

          hence thesis by XREAL_1: 231;

        end;

      end;

    end

    theorem :: RFUNCT_1:76

    X misses ( dom f) implies (f | X) is bounded

    proof

      assume (X /\ ( dom f)) = {} ;

      then ( dom (f | X)) = {} by RELAT_1: 61;

      then (f | X) = {} ;

      hence thesis;

    end;

    theorem :: RFUNCT_1:77

    (( 0 (#) f) | Y) is bounded

    proof

      reconsider p1 = 0 as Real;

      set r = 0 ;

      now

        take p = p1;

        let c be object;

        assume c in (Y /\ ( dom (r (#) f)));

        then

         A1: c in ( dom (r (#) f)) by XBOOLE_0:def 4;

        (r * (f . c)) <= 0 ;

        hence ((r (#) f) . c) <= p by A1, VALUED_1:def 5;

      end;

      hence ((r (#) f) | Y) is bounded_above by Th70;

      now

        take p = p1;

        let c be object;

        assume c in (Y /\ ( dom (r (#) f)));

        then

         A2: c in ( dom (r (#) f)) by XBOOLE_0:def 4;

         0 <= (r * (f . c));

        hence p <= ((r (#) f) . c) by A2, VALUED_1:def 5;

      end;

      hence thesis by Th71;

    end;

    registration

      let f be bounded_above real-valued Function, X be set;

      cluster (f | X) -> bounded_above;

      coherence

      proof

        consider r such that

         A1: for y be object st y in ( dom f) holds (f . y) < r by SEQ_2:def 1;

        (f | X) is bounded_above

        proof

          take r;

          let y be object;

          assume

           A2: y in ( dom (f | X));

          then y in ( dom f) by RELAT_1: 57;

          then (f . y) < r by A1;

          hence thesis by A2, FUNCT_1: 47;

        end;

        hence thesis;

      end;

    end

    registration

      let f be bounded_below real-valued Function, X be set;

      cluster (f | X) -> bounded_below;

      coherence

      proof

        consider r such that

         A1: for y be object st y in ( dom f) holds r < (f . y) by SEQ_2:def 2;

        (f | X) is bounded_below

        proof

          take r;

          let y be object;

          assume

           A2: y in ( dom (f | X));

          then y in ( dom f) by RELAT_1: 57;

          then r < (f . y) by A1;

          hence thesis by A2, FUNCT_1: 47;

        end;

        hence thesis;

      end;

    end

    registration

      let f be bounded_above real-valued Function;

      let r be non negative Real;

      cluster (r (#) f) -> bounded_above;

      coherence

      proof

        consider r1 such that

         A1: for c be object st c in ( dom f) holds (f . c) < r1 by SEQ_2:def 1;

        now

          take p = ((r * |.r1.|) + 1);

          let c be object;



           A2: r1 <= |.r1.| by ABSVALUE: 4;

          assume

           A3: c in ( dom (r (#) f));

          then c in ( dom f) by VALUED_1:def 5;

          then (f . c) < |.r1.| by A1, A2, XXREAL_0: 2;

          then (r * (f . c)) <= ( |.r1.| * r) by XREAL_1: 64;

          then ((r (#) f) . c) <= ( |.r1.| * r) by A3, VALUED_1:def 5;

          hence ((r (#) f) . c) < p by XREAL_1: 39;

        end;

        hence thesis;

      end;

    end

    registration

      let f be bounded_below real-valued Function;

      let r be non negative Real;

      cluster (r (#) f) -> bounded_below;

      coherence

      proof

        consider r1 such that

         A1: for c be object st c in ( dom f) holds r1 < (f . c) by SEQ_2:def 2;

        now

          take p = ((r * ( - |.r1.|)) - 1);

          let c be object;



           A2: ( - |.r1.|) <= r1 by ABSVALUE: 4;

          assume

           A3: c in ( dom (r (#) f));

          then c in ( dom f) by VALUED_1:def 5;

          then (f . c) >= ( - |.r1.|) by A1, A2, XXREAL_0: 2;

          then (r * (f . c)) >= (( - |.r1.|) * r) by XREAL_1: 64;

          then ((r (#) f) . c) >= (( - |.r1.|) * r) by A3, VALUED_1:def 5;

          hence ((r (#) f) . c) > p by XREAL_1: 231;

        end;

        hence thesis;

      end;

    end

    registration

      let f be bounded_above real-valued Function;

      let r be non positive Real;

      cluster (r (#) f) -> bounded_below;

      coherence

      proof

        consider r1 such that

         A1: for c be object st c in ( dom f) holds (f . c) < r1 by SEQ_2:def 1;

        now

          take p = ((r * |.r1.|) - 1);

          let c be object;



           A2: r1 <= |.r1.| by ABSVALUE: 4;

          assume

           A3: c in ( dom (r (#) f));

          then c in ( dom f) by VALUED_1:def 5;

          then (f . c) <= |.r1.| by A1, A2, XXREAL_0: 2;

          then (r * |.r1.|) <= (r * (f . c)) by XREAL_1: 65;

          then (r * |.r1.|) <= ((r (#) f) . c) by A3, VALUED_1:def 5;

          hence p < ((r (#) f) . c) by XREAL_1: 231;

        end;

        hence thesis;

      end;

    end

    registration

      let f be bounded_below real-valued Function;

      let r be non positive Real;

      cluster (r (#) f) -> bounded_above;

      coherence

      proof

        consider r1 such that

         A1: for c be object st c in ( dom f) holds r1 < (f . c) by SEQ_2:def 2;

        now

          take p = ((r * ( - |.r1.|)) + 1);

          let c be object;



           A2: ( - |.r1.|) <= r1 by ABSVALUE: 4;

          assume

           A3: c in ( dom (r (#) f));

          then c in ( dom f) by VALUED_1:def 5;

          then ( - |.r1.|) <= (f . c) by A1, A2, XXREAL_0: 2;

          then (r * (f . c)) <= (r * ( - |.r1.|)) by XREAL_1: 65;

          then ((r (#) f) . c) <= (r * ( - |.r1.|)) by A3, VALUED_1:def 5;

          hence ((r (#) f) . c) < p by XREAL_1: 39;

        end;

        hence thesis;

      end;

    end

    theorem :: RFUNCT_1:78



     Th78: ((f | Y) is bounded_above & 0 <= r implies ((r (#) f) | Y) is bounded_above) & ((f | Y) is bounded_above & r <= 0 implies ((r (#) f) | Y) is bounded_below)

    proof

      ((r (#) f) | Y) = (r (#) (f | Y)) by Th49;

      hence thesis;

    end;

    theorem :: RFUNCT_1:79



     Th79: ((f | Y) is bounded_below & 0 <= r implies ((r (#) f) | Y) is bounded_below) & ((f | Y) is bounded_below & r <= 0 implies ((r (#) f) | Y) is bounded_above)

    proof

      ((r (#) f) | Y) = (r (#) (f | Y)) by Th49;

      hence thesis;

    end;

    theorem :: RFUNCT_1:80



     Th80: (f | Y) is bounded implies ((r (#) f) | Y) is bounded

    proof

      assume

       A1: (f | Y) is bounded;

      per cases ;

        suppose

         A2: 0 <= r;

        hence ((r (#) f) | Y) is bounded_above by A1, Th78;

        thus thesis by A1, A2, Th79;

      end;

        suppose

         A3: r <= 0 ;

        hence ((r (#) f) | Y) is bounded_above by A1, Th79;

        thus thesis by A1, A3, Th78;

      end;

    end;

    registration

      let f;

      cluster ( abs f) -> bounded_below;

      coherence

      proof

        now

          reconsider p = ( - 1) as Real;

          take p;

          let c be object;

          assume c in ( dom ( abs f));

           0 <= |.(f . c).| by COMPLEX1: 46;

          hence p < (( abs f) . c) by VALUED_1: 18;

        end;

        hence thesis;

      end;

    end

    theorem :: RFUNCT_1:81

    (( abs f) | X) is bounded_below;

    registration

      let f be bounded real-valued Function;

      cluster ( abs f) -> bounded;

      coherence

      proof

        consider r1 such that

         A1: for c be object st c in ( dom f) holds |.(f . c).| <= r1 by Th72;

        now

          take r1;

          let c be object;

          assume c in ( dom ( abs f));

          then c in ( dom f) by VALUED_1:def 11;

          then |. |.(f . c).|.| <= r1 by A1;

          hence |.(( abs f) . c).| <= r1 by VALUED_1: 18;

        end;

        hence thesis by Th72;

      end;

    end

    registration

      let f be bounded_above real-valued Function;

      cluster ( - f) -> bounded_below;

      coherence ;

    end

    theorem :: RFUNCT_1:82



     Th82: (f | Y) is bounded implies (( abs f) | Y) is bounded & (( - f) | Y) is bounded

    proof

      assume

       A1: (f | Y) is bounded;

      (( abs f) | Y) = ( abs (f | Y)) by Th46;

      hence (( abs f) | Y) is bounded by A1;

      thus thesis by A1, Th80;

    end;

    reserve f1,f2 for real-valued Function;

    registration

      let f1,f2 be bounded_above real-valued Function;

      cluster (f1 + f2) -> bounded_above;

      coherence

      proof

        consider r2 such that

         A1: for c be object st c in ( dom f2) holds (f2 . c) < r2 by SEQ_2:def 1;

        consider r1 such that

         A2: for c be object st c in ( dom f1) holds (f1 . c) < r1 by SEQ_2:def 1;

        now

          take r = (r1 + r2);

          let c be object;

          assume

           A3: c in ( dom (f1 + f2));

          then

           A4: c in (( dom f1) /\ ( dom f2)) by VALUED_1:def 1;

          then c in ( dom f1) by XBOOLE_0:def 4;

          then

           A5: (f1 . c) < r1 by A2;

          c in ( dom f2) by A4, XBOOLE_0:def 4;

          then ((f1 . c) + (f2 . c)) < r by A1, A5, XREAL_1: 8;

          hence ((f1 + f2) . c) < r by A3, VALUED_1:def 1;

        end;

        hence thesis;

      end;

    end

    registration

      let f1,f2 be bounded_below real-valued Function;

      cluster (f1 + f2) -> bounded_below;

      coherence

      proof

        consider r2 such that

         A1: for c be object st c in ( dom f2) holds (f2 . c) > r2 by SEQ_2:def 2;

        consider r1 such that

         A2: for c be object st c in ( dom f1) holds (f1 . c) > r1 by SEQ_2:def 2;

        now

          take r = (r1 + r2);

          let c be object;

          assume

           A3: c in ( dom (f1 + f2));

          then

           A4: c in (( dom f1) /\ ( dom f2)) by VALUED_1:def 1;

          then c in ( dom f1) by XBOOLE_0:def 4;

          then

           A5: (f1 . c) > r1 by A2;

          c in ( dom f2) by A4, XBOOLE_0:def 4;

          then ((f1 . c) + (f2 . c)) > r by A1, A5, XREAL_1: 8;

          hence ((f1 + f2) . c) > r by A3, VALUED_1:def 1;

        end;

        hence thesis;

      end;

    end

    theorem :: RFUNCT_1:83



     Th83: ((f1 | X) is bounded_above & (f2 | Y) is bounded_above implies ((f1 + f2) | (X /\ Y)) is bounded_above) & ((f1 | X) is bounded_below & (f2 | Y) is bounded_below implies ((f1 + f2) | (X /\ Y)) is bounded_below) & ((f1 | X) is bounded & (f2 | Y) is bounded implies ((f1 + f2) | (X /\ Y)) is bounded)

    proof

      ((f1 + f2) | (X /\ Y)) = ((f1 | (X /\ Y)) + (f2 | (X /\ Y))) by Th44

      .= ((f1 | (X /\ Y)) + ((f2 | Y) | X)) by RELAT_1: 71

      .= (((f1 | X) | Y) + ((f2 | Y) | X)) by RELAT_1: 71;

      hence thesis;

    end;

    registration

      let f1,f2 be bounded real-valued Function;

      cluster (f1 (#) f2) -> bounded;

      coherence

      proof

        consider r2 such that

         A1: for c be object st c in ( dom f2) holds |.(f2 . c).| <= r2 by Th72;

        consider r1 such that

         A2: for c be object st c in ( dom f1) holds |.(f1 . c).| <= r1 by Th72;

        now

          take r = (r1 * r2);

          let c be object;



           A3: 0 <= |.(f2 . c).| by COMPLEX1: 46;

          assume c in ( dom (f1 (#) f2));

          then

           A4: c in (( dom f1) /\ ( dom f2)) by VALUED_1:def 4;

          then c in ( dom f1) by XBOOLE_0:def 4;

          then

           A5: |.(f1 . c).| <= r1 by A2;

          c in ( dom f2) by A4, XBOOLE_0:def 4;

          then

           A6: |.(f2 . c).| <= r2 by A1;

           0 <= |.(f1 . c).| by COMPLEX1: 46;

          then ( |.(f1 . c).| * |.(f2 . c).|) <= r by A5, A6, A3, XREAL_1: 66;

          then |.((f1 . c) * (f2 . c)).| <= r by COMPLEX1: 65;

          hence |.((f1 (#) f2) . c).| <= r by VALUED_1: 5;

        end;

        hence thesis by Th72;

      end;

    end

    theorem :: RFUNCT_1:84



     Th84: (f1 | X) is bounded & (f2 | Y) is bounded implies ((f1 (#) f2) | (X /\ Y)) is bounded & ((f1 - f2) | (X /\ Y)) is bounded

    proof

      assume that

       A1: (f1 | X) is bounded and

       A2: (f2 | Y) is bounded;

      ((f1 (#) f2) | (X /\ Y)) = ((f1 | (X /\ Y)) (#) (f2 | (X /\ Y))) by Th45

      .= ((f1 | (X /\ Y)) (#) ((f2 | Y) | X)) by RELAT_1: 71

      .= (((f1 | X) | Y) (#) ((f2 | Y) | X)) by RELAT_1: 71;

      hence ((f1 (#) f2) | (X /\ Y)) is bounded by A1, A2;

      (( - f2) | Y) is bounded by A2, Th82;

      hence thesis by A1, Th83;

    end;

    theorem :: RFUNCT_1:85



     Th85: (f | X) is bounded_above & (f | Y) is bounded_above implies (f | (X \/ Y)) is bounded_above

    proof

      assume that

       A1: (f | X) is bounded_above and

       A2: (f | Y) is bounded_above;

      consider r1 such that

       A3: for c be object st c in (X /\ ( dom f)) holds (f . c) <= r1 by A1, Th70;

      consider r2 such that

       A4: for c be object st c in (Y /\ ( dom f)) holds (f . c) <= r2 by A2, Th70;

      now

        take r = ( |.r1.| + |.r2.|);

        let c be object;

        assume

         A5: c in ((X \/ Y) /\ ( dom f));

        then

         A6: c in ( dom f) by XBOOLE_0:def 4;



         A7: c in (X \/ Y) by A5, XBOOLE_0:def 4;

        now

          per cases by A7, XBOOLE_0:def 3;

            suppose c in X;

            then c in (X /\ ( dom f)) by A6, XBOOLE_0:def 4;

            then

             A8: (f . c) <= r1 by A3;



             A9: 0 <= |.r2.| by COMPLEX1: 46;

            r1 <= |.r1.| by ABSVALUE: 4;

            then (f . c) <= |.r1.| by A8, XXREAL_0: 2;

            then ((f . c) + 0 qua Real) <= r by A9, XREAL_1: 7;

            hence (f . c) <= r;

          end;

            suppose c in Y;

            then c in (Y /\ ( dom f)) by A6, XBOOLE_0:def 4;

            then

             A10: (f . c) <= r2 by A4;



             A11: 0 <= |.r1.| by COMPLEX1: 46;

            r2 <= |.r2.| by ABSVALUE: 4;

            then (f . c) <= |.r2.| by A10, XXREAL_0: 2;

            then ( 0 qua Real + (f . c)) <= r by A11, XREAL_1: 7;

            hence (f . c) <= r;

          end;

        end;

        hence (f . c) <= r;

      end;

      hence thesis by Th70;

    end;

    theorem :: RFUNCT_1:86



     Th86: (f | X) is bounded_below & (f | Y) is bounded_below implies (f | (X \/ Y)) is bounded_below

    proof

      assume that

       A1: (f | X) is bounded_below and

       A2: (f | Y) is bounded_below;

      consider r1 such that

       A3: for c be object st c in (X /\ ( dom f)) holds r1 <= (f . c) by A1, Th71;

      consider r2 such that

       A4: for c be object st c in (Y /\ ( dom f)) holds r2 <= (f . c) by A2, Th71;

      now

        take r = (( - |.r1.|) - |.r2.|);

        let c be object;

        assume

         A5: c in ((X \/ Y) /\ ( dom f));

        then

         A6: c in ( dom f) by XBOOLE_0:def 4;



         A7: c in (X \/ Y) by A5, XBOOLE_0:def 4;

        now

          per cases by A7, XBOOLE_0:def 3;

            suppose c in X;

            then c in (X /\ ( dom f)) by A6, XBOOLE_0:def 4;

            then

             A8: r1 <= (f . c) by A3;



             A9: 0 <= |.r2.| by COMPLEX1: 46;

            ( - |.r1.|) <= r1 by ABSVALUE: 4;

            then ( - |.r1.|) <= (f . c) by A8, XXREAL_0: 2;

            then r <= ((f . c) - 0 ) by A9, XREAL_1: 13;

            hence r <= (f . c);

          end;

            suppose c in Y;

            then c in (Y /\ ( dom f)) by A6, XBOOLE_0:def 4;

            then

             A10: r2 <= (f . c) by A4;



             A11: 0 <= |.r1.| by COMPLEX1: 46;

            ( - |.r2.|) <= r2 by ABSVALUE: 4;

            then ( - |.r2.|) <= (f . c) by A10, XXREAL_0: 2;

            then (( - |.r2.|) - |.r1.|) <= ((f . c) - 0 ) by A11, XREAL_1: 13;

            hence r <= (f . c);

          end;

        end;

        hence r <= (f . c);

      end;

      hence thesis by Th71;

    end;

    theorem :: RFUNCT_1:87

    (f | X) is bounded & (f | Y) is bounded implies (f | (X \/ Y)) is bounded by Th85, Th86;

    reserve f,f1,f2 for PartFunc of C, REAL ;

    registration

      let C;

      let f1,f2 be constant PartFunc of C, REAL ;

      cluster (f1 + f2) -> constant;

      coherence

      proof

        consider r2 be Element of REAL such that

         A1: for c st c in ( dom f2) holds (f2 . c) = r2 by PARTFUN2:def 1;

        consider r1 be Element of REAL such that

         A2: for c st c in ( dom f1) holds (f1 . c) = r1 by PARTFUN2:def 1;

        now

          let c;

          assume

           A3: c in ( dom (f1 + f2));

          then

           A4: c in (( dom f1) /\ ( dom f2)) by VALUED_1:def 1;

          then

           A5: c in ( dom f1) by XBOOLE_0:def 4;



           A6: c in ( dom f2) by A4, XBOOLE_0:def 4;



          thus ((f1 + f2) . c) = ((f1 . c) + (f2 . c)) by A3, VALUED_1:def 1

          .= ((f1 . c) + r2) by A1, A6

          .= (r1 + r2) by A2, A5;

        end;

        hence thesis by PARTFUN2:def 1;

      end;

      cluster (f1 - f2) -> constant;

      coherence

      proof

        consider r2 be Element of REAL such that

         A7: for c st c in ( dom f2) holds (f2 . c) = r2 by PARTFUN2:def 1;

        consider r1 be Element of REAL such that

         A8: for c st c in ( dom f1) holds (f1 . c) = r1 by PARTFUN2:def 1;

        now

          let c;

          assume

           A9: c in ( dom (f1 - f2));

          then

           A10: c in (( dom f1) /\ ( dom f2)) by VALUED_1: 12;

          then

           A11: c in ( dom f1) by XBOOLE_0:def 4;



           A12: c in ( dom f2) by A10, XBOOLE_0:def 4;



          thus ((f1 - f2) . c) = ((f1 . c) - (f2 . c)) by A9, VALUED_1: 13

          .= ((f1 . c) - r2) by A7, A12

          .= (r1 - r2) by A8, A11;

        end;

        hence thesis by PARTFUN2:def 1;

      end;

      cluster (f1 (#) f2) -> constant;

      coherence

      proof

        consider r2 be Element of REAL such that

         A13: for c st c in ( dom f2) holds (f2 . c) = r2 by PARTFUN2:def 1;

        consider r1 be Element of REAL such that

         A14: for c st c in ( dom f1) holds (f1 . c) = r1 by PARTFUN2:def 1;

        now

          let c;

          assume

           A15: c in ( dom (f1 (#) f2));

          then

           A16: c in (( dom f1) /\ ( dom f2)) by VALUED_1:def 4;

          then

           A17: c in ( dom f1) by XBOOLE_0:def 4;



           A18: c in ( dom f2) by A16, XBOOLE_0:def 4;



          thus ((f1 (#) f2) . c) = ((f1 . c) * (f2 . c)) by A15, VALUED_1:def 4

          .= ((f1 . c) * r2) by A13, A18

          .= (r1 * r2) by A14, A17;

        end;

        hence thesis by PARTFUN2:def 1;

      end;

    end

    theorem :: RFUNCT_1:88

    (f1 | X) is constant & (f2 | Y) is constant implies ((f1 + f2) | (X /\ Y)) is constant & ((f1 - f2) | (X /\ Y)) is constant & ((f1 (#) f2) | (X /\ Y)) is constant

    proof

      assume that

       A1: (f1 | X) is constant and

       A2: (f2 | Y) is constant;

      consider r1 be Element of REAL such that

       A3: for c st c in (X /\ ( dom f1)) holds (f1 . c) = r1 by A1, PARTFUN2: 57;

      consider r2 be Element of REAL such that

       A4: for c st c in (Y /\ ( dom f2)) holds (f2 . c) = r2 by A2, PARTFUN2: 57;

      now

        let c;

        assume

         A5: c in ((X /\ Y) /\ ( dom (f1 + f2)));

        then

         A6: c in (X /\ Y) by XBOOLE_0:def 4;

        then

         A7: c in X by XBOOLE_0:def 4;



         A8: c in ( dom (f1 + f2)) by A5, XBOOLE_0:def 4;

        then

         A9: c in (( dom f1) /\ ( dom f2)) by VALUED_1:def 1;

        then c in ( dom f1) by XBOOLE_0:def 4;

        then

         A10: c in (X /\ ( dom f1)) by A7, XBOOLE_0:def 4;



         A11: c in Y by A6, XBOOLE_0:def 4;

        c in ( dom f2) by A9, XBOOLE_0:def 4;

        then

         A12: c in (Y /\ ( dom f2)) by A11, XBOOLE_0:def 4;



        thus ((f1 + f2) . c) = ((f1 . c) + (f2 . c)) by A8, VALUED_1:def 1

        .= (r1 + (f2 . c)) by A3, A10

        .= (r1 + r2) by A4, A12;

      end;

      hence ((f1 + f2) | (X /\ Y)) is constant by PARTFUN2: 57;

      now

        let c;

        assume

         A13: c in ((X /\ Y) /\ ( dom (f1 - f2)));

        then

         A14: c in (X /\ Y) by XBOOLE_0:def 4;

        then

         A15: c in X by XBOOLE_0:def 4;



         A16: c in ( dom (f1 - f2)) by A13, XBOOLE_0:def 4;

        then

         A17: c in (( dom f1) /\ ( dom f2)) by VALUED_1: 12;

        then c in ( dom f1) by XBOOLE_0:def 4;

        then

         A18: c in (X /\ ( dom f1)) by A15, XBOOLE_0:def 4;



         A19: c in Y by A14, XBOOLE_0:def 4;

        c in ( dom f2) by A17, XBOOLE_0:def 4;

        then

         A20: c in (Y /\ ( dom f2)) by A19, XBOOLE_0:def 4;



        thus ((f1 - f2) . c) = ((f1 . c) - (f2 . c)) by A16, VALUED_1: 13

        .= (r1 - (f2 . c)) by A3, A18

        .= (r1 - r2) by A4, A20;

      end;

      hence ((f1 - f2) | (X /\ Y)) is constant by PARTFUN2: 57;

      now

        let c;

        assume

         A21: c in ((X /\ Y) /\ ( dom (f1 (#) f2)));

        then

         A22: c in (X /\ Y) by XBOOLE_0:def 4;

        c in ( dom (f1 (#) f2)) by A21, XBOOLE_0:def 4;

        then

         A23: c in (( dom f1) /\ ( dom f2)) by VALUED_1:def 4;

        then

         A24: c in ( dom f1) by XBOOLE_0:def 4;



         A25: c in ( dom f2) by A23, XBOOLE_0:def 4;

        c in Y by A22, XBOOLE_0:def 4;

        then

         A26: c in (Y /\ ( dom f2)) by A25, XBOOLE_0:def 4;

        c in X by A22, XBOOLE_0:def 4;

        then

         A27: c in (X /\ ( dom f1)) by A24, XBOOLE_0:def 4;



        thus ((f1 (#) f2) . c) = ((f1 . c) * (f2 . c)) by VALUED_1: 5

        .= (r1 * (f2 . c)) by A3, A27

        .= (r1 * r2) by A4, A26;

      end;

      hence thesis by PARTFUN2: 57;

    end;

    registration

      let C;

      let f be constant PartFunc of C, REAL ;

      cluster ( - f) -> constant;

      coherence

      proof

        consider r be Element of REAL such that

         A1: for c be Element of C st c in ( dom f) holds (f . c) = r by PARTFUN2:def 1;

        now

          take p = ( - r);

          let c be Element of C;

          assume c in ( dom ( - f));

          then c in ( dom f) by VALUED_1: 8;

          then ( - (f . c)) = p by A1;

          hence (( - f) . c) = p by VALUED_1: 8;

        end;

        hence thesis by PARTFUN2:def 1;

      end;

      cluster ( abs f) -> constant;

      coherence

      proof

        consider r be Element of REAL such that

         A2: for c be Element of C st c in ( dom f) holds (f . c) = r by PARTFUN2:def 1;

        now

          reconsider p = |.r.| as Element of REAL by XREAL_0:def 1;

          take p;

          let c be Element of C;

          assume c in ( dom ( abs f));

          then c in ( dom f) by VALUED_1:def 11;

          then |.(f . c).| = p by A2;

          hence (( abs f) . c) = p by VALUED_1: 18;

        end;

        hence thesis by PARTFUN2:def 1;

      end;

      let p;

      cluster (p (#) f) -> constant;

      coherence

      proof

        consider r be Element of REAL such that

         A3: for c be Element of C st c in ( dom f) holds (f . c) = r by PARTFUN2:def 1;

        now

          reconsider r1 = (p * r) as Element of REAL by XREAL_0:def 1;

          take r1;

          let c be Element of C;

          assume c in ( dom (p (#) f));

          then c in ( dom f) by VALUED_1:def 5;

          then (p * (f . c)) = r1 by A3;

          hence ((p (#) f) . c) = r1 by VALUED_1: 6;

        end;

        hence thesis by PARTFUN2:def 1;

      end;

    end

    theorem :: RFUNCT_1:89



     Th89: (f | Y) is constant implies ((p (#) f) | Y) is constant

    proof

      ((p (#) f) | Y) = (p (#) (f | Y)) by Th49;

      hence thesis;

    end;

    theorem :: RFUNCT_1:90



     Th90: (f | Y) is constant implies (( - f) | Y) is constant

    proof

      (( - f) | Y) = ( - (f | Y)) by Th46;

      hence thesis;

    end;

    theorem :: RFUNCT_1:91



     Th91: (f | Y) is constant implies (( abs f) | Y) is constant

    proof

      (( abs f) | Y) = ( abs (f | Y)) by Th46;

      hence thesis;

    end;

    theorem :: RFUNCT_1:92

    (f | Y) is constant implies (for r holds ((r (#) f) | Y) is bounded) & (( - f) | Y) is bounded & (( abs f) | Y) is bounded

    proof

      assume

       A1: (f | Y) is constant;

      hereby

        let r;

        ((r (#) f) | Y) is constant by A1, Th89;

        hence ((r (#) f) | Y) is bounded;

      end;

      (( - f) | Y) is constant by A1, Th90;

      hence (( - f) | Y) is bounded;

      (( abs f) | Y) is constant by A1, Th91;

      hence thesis;

    end;

    theorem :: RFUNCT_1:93

    ((f1 | X) is bounded_above & (f2 | Y) is constant implies ((f1 + f2) | (X /\ Y)) is bounded_above) & ((f1 | X) is bounded_below & (f2 | Y) is constant implies ((f1 + f2) | (X /\ Y)) is bounded_below) & ((f1 | X) is bounded & (f2 | Y) is constant implies ((f1 + f2) | (X /\ Y)) is bounded) by Th83;

    theorem :: RFUNCT_1:94

    ((f1 | X) is bounded_above & (f2 | Y) is constant implies ((f1 - f2) | (X /\ Y)) is bounded_above) & ((f1 | X) is bounded_below & (f2 | Y) is constant implies ((f1 - f2) | (X /\ Y)) is bounded_below) & ((f1 | X) is bounded & (f2 | Y) is constant implies ((f1 - f2) | (X /\ Y)) is bounded & ((f2 - f1) | (X /\ Y)) is bounded & ((f1 (#) f2) | (X /\ Y)) is bounded)

    proof

      thus (f1 | X) is bounded_above & (f2 | Y) is constant implies ((f1 - f2) | (X /\ Y)) is bounded_above

      proof

        assume that

         A1: (f1 | X) is bounded_above and

         A2: (f2 | Y) is constant;

        (( - f2) | Y) is constant by A2, Th90;

        hence thesis by A1, Th83;

      end;

      thus (f1 | X) is bounded_below & (f2 | Y) is constant implies ((f1 - f2) | (X /\ Y)) is bounded_below

      proof

        assume that

         A3: (f1 | X) is bounded_below and

         A4: (f2 | Y) is constant;

        (( - f2) | Y) is constant by A4, Th90;

        hence thesis by A3, Th83;

      end;

      assume that

       A5: (f1 | X) is bounded and

       A6: (f2 | Y) is constant;

      (( - f2) | Y) is constant by A6, Th90;

      hence ((f1 - f2) | (X /\ Y)) is bounded by A5, Th83;

      thus ((f2 - f1) | (X /\ Y)) is bounded by A5, A6, Th84;

      thus thesis by A5, A6, Th84;

    end;