cfunct_1.miz

    begin

    reserve x,y,X,Y for set;

    reserve C for non empty set;

    reserve c for Element of C;

    reserve f,f1,f2,f3,g,g1 for PartFunc of C, COMPLEX ;

    reserve r1,r2,p1 for Real;

    reserve r,q,cr1,cr2 for Complex;

    definition

      let C, f1, f2;

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

      :: CFUNCT_1:def1

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

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

      existence

      proof

        deffunc F( set) = ( In (((f1 /. $1) * ((f2 /. $1) " )), COMPLEX ));

        defpred P[ set] means $1 in (( dom f1) /\ (( dom f2) \ (f2 " { 0c })));

        consider F be PartFunc of C, COMPLEX such that

         A1: for c holds c in ( dom F) iff P[c] and

         A2: for c st c in ( dom F) holds (F /. c) = F(c) from PARTFUN2:sch 2;

        take F;

        thus ( dom F) = (( dom f1) /\ (( dom f2) \ (f2 " { 0 }))) by A1, SUBSET_1: 3;

        let c;

        assume c in ( dom F);

        then (F /. c) = F(c) by A2;

        hence thesis;

      end;

      uniqueness

      proof

        set X = (( dom f1) /\ (( dom f2) \ (f2 " { 0 })));

        let f,g be PartFunc of C, COMPLEX such that

         A3: ( dom f) = X and

         A4: for c be Element of C st c in ( dom f) holds (f /. c) = F(c) and

         A5: ( dom g) = X and

         A6: for c be Element of C st c in ( dom g) holds (g /. c) = F(c);

        now

          let c be Element of C;

          assume

           A7: c in ( dom f);



          hence (f /. c) = F(c) by A4

          .= (g /. c) by A7, A3, A5, A6;

        end;

        hence f = g by A3, A5, PARTFUN2: 1;

      end;

    end

    definition

      let C, f;

      deffunc F( set) = ((f /. $1) " );

      :: CFUNCT_1:def2

      func f ^ -> PartFunc of C, COMPLEX means

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

      existence

      proof

        deffunc F( set) = ( In (((f /. $1) " ), COMPLEX ));

        defpred P[ set] means $1 in (( dom f) \ (f " { 0c }));

        consider F be PartFunc of C, COMPLEX such that

         A1: for c holds c in ( dom F) iff P[c] and

         A2: for c st c in ( dom F) holds (F /. c) = F(c) from PARTFUN2:sch 2;

        take F;

        thus ( dom F) = (( dom f) \ (f " { 0 })) by A1, SUBSET_1: 3;

        let c;

        assume c in ( dom F);

        then (F /. c) = F(c) by A2;

        hence thesis;

      end;

      uniqueness

      proof

        set X = (( dom f) \ (f " { 0 }));

        let f1,g1 be PartFunc of C, COMPLEX such that

         A3: ( dom f1) = X and

         A4: for c be Element of C st c in ( dom f1) holds (f1 /. c) = F(c) and

         A5: ( dom g1) = X and

         A6: for c be Element of C st c in ( dom g1) holds (g1 /. c) = F(c);

        now

          let c be Element of C;

          assume

           A7: c in ( dom f1);



          hence (f1 /. c) = F(c) by A4

          .= (g1 /. c) by A7, A3, A5, A6;

        end;

        hence f1 = g1 by A3, A5, PARTFUN2: 1;

      end;

    end

    theorem :: CFUNCT_1:1



     Th1: ( dom (f1 + f2)) = (( dom f1) /\ ( dom f2)) & for c st c in ( dom (f1 + f2)) holds ((f1 + f2) /. c) = ((f1 /. c) + (f2 /. c))

    proof

      thus

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

      now

        let c;

        assume

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

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

        then

         A3: (f1 . c) = (f1 /. c) by PARTFUN1:def 6;

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

        then

         A4: (f2 . c) = (f2 /. c) by PARTFUN1:def 6;



        thus ((f1 + f2) /. c) = ((f1 + f2) . c) by A2, PARTFUN1:def 6

        .= ((f1 /. c) + (f2 /. c)) by A2, A3, A4, VALUED_1:def 1;

      end;

      hence thesis;

    end;

    theorem :: CFUNCT_1:2



     Th2: ( dom (f1 - f2)) = (( dom f1) /\ ( dom f2)) & for c st c in ( dom (f1 - f2)) holds ((f1 - f2) /. c) = ((f1 /. c) - (f2 /. c))

    proof



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

      hence ( dom (f1 - f2)) = (( dom f1) /\ ( dom f2)) by VALUED_1: 8;

      now

        let c;

        assume

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

        then

         A3: ( dom ( - f2)) = ( dom f2) & c in ( dom ( - f2)) by A1, VALUED_1: 8, XBOOLE_0:def 4;

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

        then

         A4: (f1 /. c) = (f1 . c) by PARTFUN1:def 6;



        thus ((f1 - f2) /. c) = ((f1 - f2) . c) by A2, PARTFUN1:def 6

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

        .= ((f1 /. c) - (f2 /. c)) by A3, A4, PARTFUN1:def 6;

      end;

      hence thesis;

    end;

    theorem :: CFUNCT_1:3



     Th3: ( dom (f1 (#) f2)) = (( dom f1) /\ ( dom f2)) & for c st c in ( dom (f1 (#) f2)) holds ((f1 (#) f2) /. c) = ((f1 /. c) * (f2 /. c))

    proof

      thus

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

      now

        let c;

        assume

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

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

        then

         A3: (f1 . c) = (f1 /. c) by PARTFUN1:def 6;

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

        then

         A4: (f2 . c) = (f2 /. c) by PARTFUN1:def 6;



        thus ((f1 (#) f2) /. c) = ((f1 (#) f2) . c) by A2, PARTFUN1:def 6

        .= ((f1 /. c) * (f2 /. c)) by A2, A3, A4, VALUED_1:def 4;

      end;

      hence thesis;

    end;

    theorem :: CFUNCT_1:4



     Th4: ( dom (r (#) f)) = ( dom f) & for c st c in ( dom (r (#) f)) holds ((r (#) f) /. c) = (r * (f /. c))

    proof

      thus

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

      now

        let c;

        assume

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



        hence ((r (#) f) /. c) = ((r (#) f) . c) by PARTFUN1:def 6

        .= (r * (f . c)) by VALUED_1: 6

        .= (r * (f /. c)) by A1, A2, PARTFUN1:def 6;

      end;

      hence thesis;

    end;

    theorem :: CFUNCT_1:5



     Th5: ( dom ( - f)) = ( dom f) & for c st c in ( dom ( - f)) holds (( - f) /. c) = ( - (f /. c))

    proof

      thus

       A1: ( dom ( - f)) = ( dom f) by VALUED_1: 8;

      now

        let c;

        assume

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



        hence (( - f) /. c) = (( - f) . c) by PARTFUN1:def 6

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

        .= ( - (f /. c)) by A1, A2, PARTFUN1:def 6;

      end;

      hence thesis;

    end;



     Lm1: x in (f " Y) iff x in ( dom f) & (f /. x) in Y by PARTFUN2: 26;

    theorem :: CFUNCT_1:6



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

    proof

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

      hence ( dom (g ^ )) c= ( dom g) by XBOOLE_1: 36;

      thus thesis by XBOOLE_1: 28, XBOOLE_1: 36;

    end;

    theorem :: CFUNCT_1:7



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

         A2: x in ( dom (f1 (#) f2)) by XBOOLE_0:def 5;

        reconsider x1 = x as Element of C by A1;

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

        then not ((f1 (#) f2) /. x1) in { 0c } by A2, PARTFUN2: 26;

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

        then

         A3: ((f1 /. x1) * (f2 /. x1)) <> 0c by A2, Th3;

        then (f2 /. x1) <> 0c ;

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

        then

         A4: not x1 in (f2 " { 0c }) by PARTFUN2: 26;



         A5: x1 in (( dom f1) /\ ( dom f2)) by A2, Th3;

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

        then

         A6: x in (( dom f2) \ (f2 " { 0c })) by A4, XBOOLE_0:def 5;

        (f1 /. x1) <> 0c by A3;

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

        then

         A7: not x1 in (f1 " { 0c }) by PARTFUN2: 26;

        x1 in ( dom f1) by A5, XBOOLE_0:def 4;

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

        hence thesis by A6, 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

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

        then

        reconsider x1 = x as Element of C;



         A9: x in (( dom f2) \ (f2 " { 0c })) by A8, XBOOLE_0:def 4;

        then

         A10: x in ( dom f2) by XBOOLE_0:def 5;

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

        then not (f2 /. x1) in { 0c } by A10, PARTFUN2: 26;

        then

         A11: (f2 /. x1) <> 0c by TARSKI:def 1;



         A12: x in (( dom f1) \ (f1 " { 0c })) by A8, XBOOLE_0:def 4;

        then

         A13: x in ( dom f1) by XBOOLE_0:def 5;

        then x1 in (( dom f1) /\ ( dom f2)) by A10, XBOOLE_0:def 4;

        then

         A14: x1 in ( dom (f1 (#) f2)) by Th3;

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

        then not (f1 /. x1) in { 0c } by A13, PARTFUN2: 26;

        then (f1 /. x1) <> 0c by TARSKI:def 1;

        then ((f1 /. x1) * (f2 /. x1)) <> 0c by A11, XCMPLX_1: 6;

        then ((f1 (#) f2) /. x1) <> 0c by A14, Th3;

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

        then not x in ((f1 (#) f2) " { 0c }) by PARTFUN2: 26;

        hence thesis by A14, XBOOLE_0:def 5;

      end;

    end;

    theorem :: CFUNCT_1:8



     Th8: 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 " { 0c })) by A1, Def2;

      then

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

      now

        per cases by A4, PARTFUN2: 26;

          suppose not c in ( dom f);

          hence contradiction by A3, XBOOLE_0:def 5;

        end;

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

          hence contradiction by A2, TARSKI:def 1;

        end;

      end;

      hence contradiction;

    end;

    theorem :: CFUNCT_1:9



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

    proof

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

      assume

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

      then

       A2: x in ( dom (f ^ )) by Lm1;



       A3: ((f ^ ) /. x) in { 0c } by A1, Lm1;

      reconsider x as Element of C by A2;

      x in (( dom f) \ (f " { 0c })) by A2, Def2;

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

      then

       A4: not (f /. x) in { 0c } by PARTFUN2: 26;

      ((f ^ ) /. x) = 0c by A3, TARSKI:def 1;

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

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

    end;

    theorem :: CFUNCT_1:10



     Th10: ( |.f.| " { 0 }) = (f " { 0 }) & (( - f) " { 0 }) = (f " { 0 })

    proof



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

      now

        let c;

        thus c in ( |.f.| " { 0 }) implies c in (f " { 0c })

        proof

          assume

           A2: c in ( |.f.| " { 0 });

          then c in ( dom |.f.|) by FUNCT_1:def 7;

          then

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

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

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

          then

           A4: |.(f . c).| = 0 by VALUED_1: 18;

          c in ( dom |.f.|) by A2, FUNCT_1:def 7;

          then (f . c) = (f /. c) by A1, PARTFUN1:def 6;

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

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

          hence thesis by A3, PARTFUN2: 26;

        end;

        assume

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

        then (f /. c) in { 0c } by PARTFUN2: 26;

        then

         A6: |.(f /. c).| = 0 by COMPLEX1: 44, TARSKI:def 1;



         A7: c in ( dom f) by A5, PARTFUN2: 26;

        then (f . c) = (f /. c) by PARTFUN1:def 6;

        then ( |.f.| . c) = 0 by A6, VALUED_1: 18;

        then

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

        c in ( dom |.f.|) by A7, VALUED_1:def 11;

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

      end;

      hence ( |.f.| " { 0 }) = (f " { 0 }) by SUBSET_1: 3;

      now

        let c;

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

        proof

          assume

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

          then

           A10: c in ( dom ( - f)) by PARTFUN2: 26;

          (( - f) /. c) in { 0c } by A9, PARTFUN2: 26;

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

          then ( - ( - (f /. c))) = ( - 0c ) by A10, Th5;

          then

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

          c in ( dom f) by A10, Th5;

          hence thesis by A11, PARTFUN2: 26;

        end;

        assume

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

        then (f /. c) in { 0c } by PARTFUN2: 26;

        then

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



         A14: c in ( dom f) by A12, PARTFUN2: 26;

        then c in ( dom ( - f)) by Th5;

        then (( - f) /. c) = ( - 0c ) by A13, Th5;

        then

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

        c in ( dom ( - f)) by A14, Th5;

        hence c in (( - f) " { 0c }) by A15, PARTFUN2: 26;

      end;

      hence thesis by SUBSET_1: 3;

    end;

    theorem :: CFUNCT_1:11



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

    proof



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



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

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

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

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

    end;

    theorem :: CFUNCT_1:12



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

    proof

      assume

       A1: r <> 0 ;

      now

        let c;

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

        proof

          assume

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

          then

           A3: c in ( dom (r (#) f)) by PARTFUN2: 26;

          ((r (#) f) /. c) in { 0c } by A2, PARTFUN2: 26;

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

          then (r * (f /. c)) = 0c by A3, Th4;

          then (f /. c) = 0c by A1, XCMPLX_1: 6;

          then

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

          c in ( dom f) by A3, Th4;

          hence thesis by A4, PARTFUN2: 26;

        end;

        assume

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

        then (f /. c) in { 0c } by PARTFUN2: 26;

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

        then

         A6: (r * (f /. c)) = 0c ;



         A7: c in ( dom f) by A5, PARTFUN2: 26;

        then c in ( dom (r (#) f)) by Th4;

        then ((r (#) f) /. c) = 0c by A6, Th4;

        then

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

        c in ( dom (r (#) f)) by A7, Th4;

        hence c in ((r (#) f) " { 0c }) by A8, PARTFUN2: 26;

      end;

      hence thesis by SUBSET_1: 3;

    end;

    begin

    theorem :: CFUNCT_1:13

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

        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, Th1

        .= (((f1 /. c) + (f2 /. c)) + (f3 /. c)) by A3, Th1

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

        .= ((f1 /. c) + ((f2 + f3) /. c)) by A4, Th1

        .= ((f1 + (f2 + f3)) /. c) by A1, A2, Th1;

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: CFUNCT_1:14



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

    proof



       A1: ( dom ((f1 (#) f2) (#) f3)) = (( dom (f1 (#) f2)) /\ ( dom f3)) by Th3

      .= ((( dom f1) /\ ( dom f2)) /\ ( dom f3)) by Th3

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

      .= (( dom f1) /\ ( dom (f2 (#) f3))) by Th3

      .= ( dom (f1 (#) (f2 (#) f3))) by Th3;

      now

        let c;

        assume

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

        then c in (( dom (f1 (#) f2)) /\ ( dom f3)) by Th3;

        then

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

        c in (( dom f1) /\ ( dom (f2 (#) f3))) by A1, A2, Th3;

        then

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



        thus (((f1 (#) f2) (#) f3) /. c) = (((f1 (#) f2) /. c) * (f3 /. c)) by A2, Th3

        .= (((f1 /. c) * (f2 /. c)) * (f3 /. c)) by A3, Th3

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

        .= ((f1 /. c) * ((f2 (#) f3) /. c)) by A4, Th3

        .= ((f1 (#) (f2 (#) f3)) /. c) by A1, A2, Th3;

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: CFUNCT_1:15



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

    proof



       A1: ( dom ((f1 + f2) (#) f3)) = (( dom (f1 + f2)) /\ ( dom f3)) by Th3

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

      .= (( dom (f1 (#) f3)) /\ ( dom (f2 (#) f3))) by Th3

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

      now

        let c;

        assume

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

        then

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

        then

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

        c in (( dom (f1 + f2)) /\ ( dom f3)) by A2, Th3;

        then

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



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



        thus (((f1 + f2) (#) f3) /. c) = (((f1 + f2) /. c) * (f3 /. c)) by A2, Th3

        .= (((f1 /. c) + (f2 /. c)) * (f3 /. c)) by A5, Th1

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

        .= (((f1 (#) f3) /. c) + ((f2 /. c) * (f3 /. c))) by A4, Th3

        .= (((f1 (#) f3) /. c) + ((f2 (#) f3) /. c)) by A6, Th3

        .= (((f1 (#) f3) + (f2 (#) f3)) /. c) by A1, A2, Th1;

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: CFUNCT_1:16

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

    theorem :: CFUNCT_1:17



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

    proof



       A1: ( dom (r (#) (f1 (#) f2))) = ( dom (f1 (#) f2)) by Th4

      .= (( dom f1) /\ ( dom f2)) by Th3

      .= (( dom (r (#) f1)) /\ ( dom f2)) by Th4

      .= ( dom ((r (#) f1) (#) f2)) by Th3;

      now

        let c;

        assume

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

        then

         A3: c in ( dom (f1 (#) f2)) by Th4;

        c in (( dom (r (#) f1)) /\ ( dom f2)) by A1, A2, Th3;

        then

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



        thus ((r (#) (f1 (#) f2)) /. c) = (r * ((f1 (#) f2) /. c)) by A2, Th4

        .= (r * ((f1 /. c) * (f2 /. c))) by A3, Th3

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

        .= (((r (#) f1) /. c) * (f2 /. c)) by A4, Th4

        .= (((r (#) f1) (#) f2) /. c) by A1, A2, Th3;

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: CFUNCT_1:18



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

    proof



       A1: ( dom (r (#) (f1 (#) f2))) = ( dom (f1 (#) f2)) by Th4

      .= (( dom f1) /\ ( dom f2)) by Th3

      .= (( dom f1) /\ ( dom (r (#) f2))) by Th4

      .= ( dom (f1 (#) (r (#) f2))) by Th3;

      now

        let c;

        assume

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

        then

         A3: c in ( dom (f1 (#) f2)) by Th4;

        c in (( dom f1) /\ ( dom (r (#) f2))) by A1, A2, Th3;

        then

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



        thus ((r (#) (f1 (#) f2)) /. c) = (r * ((f1 (#) f2) /. c)) by A2, Th4

        .= (r * ((f1 /. c) * (f2 /. c))) by A3, Th3

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

        .= ((f1 /. c) * ((r (#) f2) /. c)) by A4, Th4

        .= ((f1 (#) (r (#) f2)) /. c) by A1, A2, Th3;

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: CFUNCT_1:19



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

    proof



       A1: ( dom ((f1 - f2) (#) f3)) = (( dom (f1 - f2)) /\ ( dom f3)) by Th3

      .= ((( dom f1) /\ ( dom f2)) /\ (( dom f3) /\ ( dom f3))) by Th2

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

      .= (( dom (f1 (#) f3)) /\ ( dom (f2 (#) f3))) by Th3

      .= ( dom ((f1 (#) f3) - (f2 (#) f3))) by Th2;

      now

        let c;

        assume

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

        then c in (( dom (f1 - f2)) /\ ( dom f3)) by Th3;

        then

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



         A4: c in (( dom (f1 (#) f3)) /\ ( dom (f2 (#) f3))) by A1, A2, Th2;

        then

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



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



        thus (((f1 - f2) (#) f3) /. c) = (((f1 - f2) /. c) * (f3 /. c)) by A2, Th3

        .= (((f1 /. c) - (f2 /. c)) * (f3 /. c)) by A3, Th2

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

        .= (((f1 (#) f3) /. c) - ((f2 /. c) * (f3 /. c))) by A5, Th3

        .= (((f1 (#) f3) /. c) - ((f2 (#) f3) /. c)) by A6, Th3

        .= (((f1 (#) f3) - (f2 (#) f3)) /. c) by A1, A2, Th2;

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: CFUNCT_1:20

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

    theorem :: CFUNCT_1:21

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

    proof



       A1: ( dom (r (#) (f1 + f2))) = ( dom (f1 + f2)) by Th4

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

      .= (( dom f1) /\ ( dom (r (#) f2))) by Th4

      .= (( dom (r (#) f1)) /\ ( dom (r (#) f2))) by Th4

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

      now

        let c;

        assume

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

        then

         A3: c in ( dom (f1 + f2)) by Th4;



         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, Th4

        .= (r * ((f1 /. c) + (f2 /. c))) by A3, Th1

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

        .= (((r (#) f1) /. c) + (r * (f2 /. c))) by A5, Th4

        .= (((r (#) f1) /. c) + ((r (#) f2) /. c)) by A6, Th4

        .= (((r (#) f1) + (r (#) f2)) /. c) by A1, A2, Th1;

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: CFUNCT_1:22

    ((r * q) (#) f) = (r (#) (q (#) f))

    proof



       A1: ( dom ((r * q) (#) f)) = ( dom f) by Th4

      .= ( dom (q (#) f)) by Th4

      .= ( dom (r (#) (q (#) f))) by Th4;

      now

        let c;

        assume

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

        then

         A3: c in ( dom (q (#) f)) by A1, Th4;



        thus (((r * q) (#) f) /. c) = ((r * q) * (f /. c)) by A2, Th4

        .= (r * (q * (f /. c)))

        .= (r * ((q (#) f) /. c)) by A3, Th4

        .= ((r (#) (q (#) f)) /. c) by A1, A2, Th4;

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: CFUNCT_1:23

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

    proof



       A1: ( dom (r (#) (f1 - f2))) = ( dom (f1 - f2)) by Th4

      .= (( dom f1) /\ ( dom f2)) by Th2

      .= (( dom f1) /\ ( dom (r (#) f2))) by Th4

      .= (( dom (r (#) f1)) /\ ( dom (r (#) f2))) by Th4

      .= ( dom ((r (#) f1) - (r (#) f2))) by Th2;

      now

        let c;

        assume

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

        then

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



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

        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, Th4

        .= (r * ((f1 /. c) - (f2 /. c))) by A3, Th2

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

        .= (((r (#) f1) /. c) - (r * (f2 /. c))) by A5, Th4

        .= (((r (#) f1) /. c) - ((r (#) f2) /. c)) by A6, Th4

        .= (((r (#) f1) - (r (#) f2)) /. c) by A1, A2, Th2;

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: CFUNCT_1:24

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

    proof



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

      .= ( dom (f2 - f1)) by Th2

      .= ( dom (( - 1r ) (#) (f2 - f1))) by Th4;

      now



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

        .= ( dom (f2 - f1)) by Th2;

        let c such that

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



        thus ((f1 - f2) /. c) = ((f1 /. c) - (f2 /. c)) by A3, Th2

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

        .= (( - 1r ) * ((f2 - f1) /. c)) by A3, A2, Th2, COMPLEX1:def 4

        .= ((( - 1r ) (#) (f2 - f1)) /. c) by A1, A3, Th4;

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: CFUNCT_1:25

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

    proof



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

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

      .= ( dom ((f1 - f2) - f3)) by Th2;

      now

        let c;

        assume

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

        then c in (( dom f1) /\ ( dom (f2 + f3))) by Th2;

        then

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

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

        then

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



        thus ((f1 - (f2 + f3)) /. c) = ((f1 /. c) - ((f2 + f3) /. c)) by A2, Th2

        .= ((f1 /. c) - ((f2 /. c) + (f3 /. c))) by A3, Th1

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

        .= (((f1 - f2) /. c) - (f3 /. c)) by A4, Th2

        .= (((f1 - f2) - f3) /. c) by A1, A2, Th2;

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: CFUNCT_1:26

    ( 1r (#) f) = f

    proof

       A1:

      now

        let c;

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



        hence (( 1r (#) f) /. c) = ( 1r * (f /. c)) by Th4

        .= (f /. c) by COMPLEX1:def 4;

      end;

      ( dom ( 1r (#) f)) = ( dom f) by Th4;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: CFUNCT_1:27

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

    proof



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

      .= (( dom f1) /\ (( dom f2) /\ ( dom f3))) by Th2

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

      .= (( dom (f1 - f2)) /\ ( dom f3)) by Th2

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

      now

        let c;

        assume

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

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

        then

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

        c in (( dom f1) /\ ( dom (f2 - f3))) by A2, Th2;

        then

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



        thus ((f1 - (f2 - f3)) /. c) = ((f1 /. c) - ((f2 - f3) /. c)) by A2, Th2

        .= ((f1 /. c) - ((f2 /. c) - (f3 /. c))) by A4, Th2

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

        .= (((f1 - f2) /. c) + (f3 /. c)) by A3, Th2

        .= (((f1 - f2) + f3) /. c) by A1, A2, Th1;

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: CFUNCT_1:28

    (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 Th2

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

      now

        let c;

        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, Th2;

        then

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



        thus ((f1 + (f2 - f3)) /. c) = ((f1 /. c) + ((f2 - f3) /. c)) by A2, Th1

        .= ((f1 /. c) + ((f2 /. c) - (f3 /. c))) by A3, Th2

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

        .= (((f1 + f2) /. c) - (f3 /. c)) by A4, Th1

        .= (((f1 + f2) - f3) /. c) by A1, A2, Th2;

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: CFUNCT_1:29



     Th29: |.(f1 (#) f2).| = ( |.f1.| (#) |.f2.|)

    proof



       A1: ( dom |.(f1 (#) f2).|) = ( dom (f1 (#) f2)) by VALUED_1:def 11

      .= (( dom f1) /\ ( dom f2)) by Th3

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

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

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

      now



         A2: ( dom |.f2.|) = ( dom f2) by VALUED_1:def 11;

        let c;



         A3: ( dom |.f1.|) = ( dom f1) by VALUED_1:def 11;

        assume

         A4: c in ( dom |.(f1 (#) f2).|);

        then

         A5: c in ( dom (f1 (#) f2)) by VALUED_1:def 11;



         A6: c in (( dom |.f1.|) /\ ( dom |.f2.|)) by A1, A4, VALUED_1:def 4;

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

        then

         A7: (f1 . c) = (f1 /. c) by A3, PARTFUN1:def 6;

        c in ( dom |.f2.|) by A6, XBOOLE_0:def 4;

        then

         A8: (f2 /. c) = (f2 . c) by A2, PARTFUN1:def 6;



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

        .= |.((f1 (#) f2) /. c).| by A5, PARTFUN1:def 6

        .= |.((f1 /. c) * (f2 /. c)).| by A5, Th3

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

        .= (( |.f1.| . c) * |.(f2 /. c).|) by A7, VALUED_1: 18

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

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

      end;

      hence thesis by A1, PARTFUN1: 5;

    end;

    theorem :: CFUNCT_1:30



     Th30: |.(r (#) f).| = ( |.r.| (#) |.f.|)

    proof



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



       A2: ( dom |.(r (#) f).|) = ( dom (r (#) f)) by VALUED_1:def 11

      .= ( dom f) by Th4

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

      now

        let c;

        assume

         A3: c in ( dom |.(r (#) f).|);

        then

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



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



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

        .= |.((r (#) f) /. c).| by A4, PARTFUN1:def 6

        .= |.(r * (f /. c)).| by A4, Th4

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

        .= ( |.r.| * |.(f . c).|) by A1, A5, PARTFUN1:def 6

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

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

      end;

      hence thesis by A2, PARTFUN1: 5;

    end;

    theorem :: CFUNCT_1:31

    ( - f) = (( - 1r ) (#) f) by COMPLEX1:def 4;

    ::$Canceled

    theorem :: CFUNCT_1:33

    (f1 - ( - f2)) = (f1 + f2);

    theorem :: CFUNCT_1:34



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

    proof



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

      now

        let c;

        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, PARTFUN2: 15;

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: CFUNCT_1:35



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

    proof



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

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

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

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

      .= ( dom ((f1 ^ ) (#) (f2 ^ ))) by Th3;

      now

        let c;

        assume

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

        then c in (( dom (f1 (#) f2)) \ ((f1 (#) f2) " { 0c })) by Def2;

        then

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



         A4: c in (( dom (f1 ^ )) /\ ( dom (f2 ^ ))) by A1, A2, Th3;

        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 (#) f2) /. c) " ) by A2, Def2

        .= (((f1 /. c) * (f2 /. c)) " ) by A3, Th3

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

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

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

        .= (((f1 ^ ) (#) (f2 ^ )) /. c) by A1, A2, Th3;

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: CFUNCT_1:36



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

    proof

      assume

       A1: r <> 0 ;



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

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

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

      .= ( dom (f ^ )) by Def2

      .= ( dom ((r " ) (#) (f ^ ))) by Th4;

      now

        let c;

        assume

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

        then

         A4: c in ( dom (f ^ )) by A2, Th4;

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

        then

         A5: c in ( dom (r (#) f)) by XBOOLE_0:def 5;



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

        .= ((r * (f /. c)) " ) by A5, Th4

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

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

        .= (((r " ) (#) (f ^ )) /. c) by A2, A3, Th4;

      end;

      hence thesis by A2, PARTFUN2: 1;

    end;



     Lm2: (( - 1r ) " ) = ( - 1r ) by COMPLEX1:def 4;

    theorem :: CFUNCT_1:37

    (( - f) ^ ) = (( - 1r ) (#) (f ^ )) by Lm2, Th35, COMPLEX1:def 4;

    theorem :: CFUNCT_1:38



     Th37: ( |.f.| ^ ) = |.(f ^ ).|

    proof



       A1: ( dom ( |.f.| ^ )) = (( dom |.f.|) \ ( |.f.| " { 0 })) by RFUNCT_1:def 2

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

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

      .= ( dom (f ^ )) by Def2

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

      now

        let c;



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

        assume

         A3: c in ( dom ( |.f.| ^ ));

        then

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

        c in (( dom |.f.|) \ ( |.f.| " { 0 })) by A3, RFUNCT_1:def 2;

        then

         A5: c in ( dom |.f.|) by XBOOLE_0:def 5;



        thus (( |.f.| ^ ) . c) = (( |.f.| . c) " ) by A3, RFUNCT_1:def 2

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

        .= ( |.(f /. c).| " ) by A5, A2, PARTFUN1:def 6

        .= ( |. 1r .| / |.(f /. c).|) by COMPLEX1: 48, XCMPLX_1: 215

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

        .= |.((f /. c) " ).| by COMPLEX1:def 4, XCMPLX_1: 215

        .= |.((f ^ ) /. c).| by A4, Def2

        .= |.((f ^ ) . c).| by A4, PARTFUN1:def 6

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

      end;

      hence thesis by A1, PARTFUN1: 5;

    end;

    theorem :: CFUNCT_1:39



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

    proof

       A1:

      now

        let c;

        assume

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

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

        then

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

        then

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



         A5: c in ( dom (f (#) (g ^ ))) by A3, Th3;



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

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

        .= ((f (#) (g ^ )) /. c) by A5, Th3;

      end;

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

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

      .= ( dom (f (#) (g ^ ))) by Th3;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: CFUNCT_1:40



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

    proof



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

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

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

    end;

    theorem :: CFUNCT_1:41

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

    proof



       A1: ( dom ((f / g) (#) g)) = (( dom (f / g)) /\ ( dom g)) by Th3

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

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

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

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

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

      now

        let c;

        assume

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

        then

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

        then

         A4: c in ( dom (f (#) (g ^ ))) by Th3;



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

        then

         A6: (g /. c) <> 0c by Th8;



        thus (((f / g) (#) g) /. c) = (((f / g) /. c) * (g /. c)) by A2, Th3

        .= (((f (#) (g ^ )) /. c) * (g /. c)) by Th38

        .= (((f /. c) * ((g ^ ) /. c)) * (g /. c)) by A4, Th3

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

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

        .= ((f /. c) * 1r ) by A6, COMPLEX1:def 4, XCMPLX_0:def 7

        .= ((f | ( dom (g ^ ))) /. c) by A1, A2, COMPLEX1:def 4, PARTFUN2: 15;

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: CFUNCT_1:42



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

    proof

       A1:

      now

        let c;

        assume

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

        then c in (( dom (f / g)) /\ ( dom (f1 / g1))) by Th3;

        then

         A3: c in (( dom (f (#) (g ^ ))) /\ ( dom (f1 / g1))) by Th38;

        then

         A4: c in ( dom (f (#) (g ^ ))) by XBOOLE_0:def 4;

        then

         A5: c in (( dom f) /\ ( dom (g ^ ))) by Th3;

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

        then

         A6: c in ( dom (f1 (#) (g1 ^ ))) by XBOOLE_0:def 4;

        then

         A7: c in (( dom f1) /\ ( dom (g1 ^ ))) by Th3;

        then

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

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

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

        then

         A9: c in ( dom (f (#) f1)) by Th3;



         A10: c in ( dom (g1 ^ )) by A7, XBOOLE_0:def 4;

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

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

        then

         A11: c in ( dom ((g ^ ) (#) (g1 ^ ))) by Th3;

        then c in ( dom ((g (#) g1) ^ )) by Th34;

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

        then

         A12: c in ( dom ((f (#) f1) (#) ((g (#) g1) ^ ))) by Th3;



        thus (((f / g) (#) (f1 / g1)) /. c) = (((f / g) /. c) * ((f1 / g1) /. c)) by A2, Th3

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

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

        .= (((f /. c) * ((g ^ ) /. c)) * ((f1 (#) (g1 ^ )) /. c)) by A4, Th3

        .= (((f /. c) * ((g ^ ) /. c)) * ((f1 /. c) * ((g1 ^ ) /. c))) by A6, Th3

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

        .= ((f /. c) * ((f1 /. c) * (((g ^ ) (#) (g1 ^ )) /. c))) by A11, Th3

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

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

        .= (((f (#) f1) /. c) * (((g (#) g1) ^ ) /. c)) by A9, Th3

        .= (((f (#) f1) (#) ((g (#) g1) ^ )) /. c) by A12, Th3

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

      end;

      ( dom ((f / g) (#) (f1 / g1))) = (( dom (f / g)) /\ ( dom (f1 / g1))) by Th3

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

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

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

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

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

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

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

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

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: CFUNCT_1:43



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

    proof



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

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

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

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

    end;

    theorem :: CFUNCT_1:44



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

    proof



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

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

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

    end;

    theorem :: CFUNCT_1:45

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

    proof



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

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

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

    end;

    theorem :: CFUNCT_1:46

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

    proof



      thus ( - (f / g)) = (( - 1r ) (#) (f / g)) by COMPLEX1:def 4

      .= (( - f) / g) by Th39, COMPLEX1:def 4;



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

      .= (f (#) (( - 1r ) (#) (g ^ ))) by Lm2, Th35, COMPLEX1:def 4

      .= ( - (f (#) (g ^ ))) by Th18, COMPLEX1:def 4

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

    end;

    theorem :: CFUNCT_1:47

    ((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 Th38

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

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

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



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

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

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

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

    end;

    theorem :: CFUNCT_1:48



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

    proof

       A1:

      now

        let c;



         A2: ( dom (f ^ )) c= ( dom f) by Th6;

        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: c in (( dom (f1 (#) (f ^ ))) /\ ( dom (g1 / g))) by A4, Th38;

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

        then

         A8: c in (( dom f1) /\ ( dom (f ^ ))) by Th3;

        then

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

        then

         A10: (f /. c) <> 0c by Th8;

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

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

        then

         A11: c in (( dom g1) /\ ( dom (g ^ ))) by Th3;

        then

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

        then

         A13: (g /. c) <> 0c by Th8;

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

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

        then

         A14: c in ( dom (g1 (#) f)) by Th3;



         A15: ( dom (g ^ )) c= ( dom g) by Th6;

        then c in (( dom f) /\ ( dom g)) by A9, A12, A2, XBOOLE_0:def 4;

        then

         A16: c in ( dom (f (#) g)) by Th3;

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

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

        then

         A17: c in ( dom (f1 (#) g)) by Th3;

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

        then

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

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

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

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

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

        then c in ( dom (((f1 (#) g) + (g1 (#) f)) (#) ((f (#) g) ^ ))) by Th3;

        then

         A19: c in ( dom (((f1 (#) g) + (g1 (#) f)) / (f (#) g))) by Th38;



        thus (((f1 / f) + (g1 / g)) /. c) = (((f1 / f) /. c) + ((g1 / g) /. c)) by A3, Th1

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

        .= (((f1 /. c) * ( 1r * ((f /. c) " ))) + (((g1 /. c) * 1r ) * ((g /. c) " ))) by A6, Def1, COMPLEX1:def 4

        .= (((f1 /. c) * (((g /. c) * ((g /. c) " )) * ((f /. c) " ))) + ((g1 /. c) * ( 1r * ((g /. c) " )))) by A13, COMPLEX1:def 4, XCMPLX_0:def 7

        .= (((f1 /. c) * ((g /. c) * (((g /. c) " ) * ((f /. c) " )))) + ((g1 /. c) * (((f /. c) * ((f /. c) " )) * ((g /. c) " )))) by A10, COMPLEX1:def 4, 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 A16, Th3

        .= ((((f1 /. c) * (g /. c)) * (((f (#) g) /. c) " )) + ((g1 /. c) * ((f /. c) * (((f (#) g) /. c) " )))) by A16, Th3

        .= ((((f1 (#) g) /. c) * (((f (#) g) /. c) " )) + (((g1 /. c) * (f /. c)) * (((f (#) g) /. c) " ))) by A17, Th3

        .= ((((f1 (#) g) /. c) * (((f (#) g) /. c) " )) + (((g1 (#) f) /. c) * (((f (#) g) /. c) " ))) by A14, Th3

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

        .= ((((f1 (#) g) + (g1 (#) f)) /. c) * (((f (#) g) /. c) " )) by A18, Th1

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

      end;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: CFUNCT_1:49

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

    proof



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

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

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

    end;

    theorem :: CFUNCT_1:50

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

    proof



      thus ((f1 / f) - (g1 / g)) = ((f1 / f) + ((( - 1r ) (#) g1) / g)) by Th39, COMPLEX1:def 4

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

      .= (((f1 (#) g) - (g1 (#) f)) / (f (#) g)) by Th17, COMPLEX1:def 4;

    end;

    theorem :: CFUNCT_1:51

     |.(f1 / f2).| = ( |.f1.| / |.f2.|)

    proof



      thus |.(f1 / f2).| = |.(f1 (#) (f2 ^ )).| by Th38

      .= ( |.f1.| (#) |.(f2 ^ ).|) by Th29

      .= ( |.f1.| (#) ( |.f2.| ^ )) by Th37

      .= ( |.f1.| / |.f2.|) by RFUNCT_1: 31;

    end;

    theorem :: CFUNCT_1:52



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

    proof

       A1:

      now

        let c;

        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, PARTFUN2: 15

        .= ((f1 /. c) + (f2 /. c)) by A5, Th1

        .= (((f1 | X) /. c) + (f2 /. c)) by A8, PARTFUN2: 15

        .= (((f1 | X) /. c) + ((f2 | X) /. c)) by A7, PARTFUN2: 15

        .= (((f1 | X) + (f2 | X)) /. c) by A9, Th1;

      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, PARTFUN2: 1;

       A10:

      now

        let c;

        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, PARTFUN2: 15

        .= ((f1 /. c) + (f2 /. c)) by A14, Th1

        .= (((f1 | X) /. c) + (f2 /. c)) by A16, PARTFUN2: 15

        .= (((f1 | X) + f2) /. c) by A17, Th1;

      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, PARTFUN2: 1;

       A18:

      now

        let c;

        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, PARTFUN2: 15

        .= ((f1 /. c) + (f2 /. c)) by A22, Th1

        .= ((f1 /. c) + ((f2 | X) /. c)) by A24, PARTFUN2: 15

        .= ((f1 + (f2 | X)) /. c) by A25, Th1;

      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, PARTFUN2: 1;

    end;

    theorem :: CFUNCT_1:53



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

    proof

       A1:

      now

        let c;

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

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



        thus (((f1 (#) f2) | X) /. c) = ((f1 (#) f2) /. c) by A2, PARTFUN2: 15

        .= ((f1 /. c) * (f2 /. c)) by A5, Th3

        .= (((f1 | X) /. c) * (f2 /. c)) by A8, PARTFUN2: 15

        .= (((f1 | X) /. c) * ((f2 | X) /. c)) by A7, PARTFUN2: 15

        .= (((f1 | X) (#) (f2 | X)) /. c) by A9, Th3;

      end;

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

      .= ((( dom f1) /\ ( dom f2)) /\ (X /\ X)) by Th3

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

      hence ((f1 (#) f2) | X) = ((f1 | X) (#) (f2 | X)) by A1, PARTFUN2: 1;

       A10:

      now

        let c;

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

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



        thus (((f1 (#) f2) | X) /. c) = ((f1 (#) f2) /. c) by A11, PARTFUN2: 15

        .= ((f1 /. c) * (f2 /. c)) by A14, Th3

        .= (((f1 | X) /. c) * (f2 /. c)) by A16, PARTFUN2: 15

        .= (((f1 | X) (#) f2) /. c) by A17, Th3;

      end;

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

      .= ((( dom f1) /\ ( dom f2)) /\ X) by Th3

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

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

      .= ( dom ((f1 | X) (#) f2)) by Th3;

      hence ((f1 (#) f2) | X) = ((f1 | X) (#) f2) by A10, PARTFUN2: 1;

       A18:

      now

        let c;

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

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



        thus (((f1 (#) f2) | X) /. c) = ((f1 (#) f2) /. c) by A19, PARTFUN2: 15

        .= ((f1 /. c) * (f2 /. c)) by A22, Th3

        .= ((f1 /. c) * ((f2 | X) /. c)) by A24, PARTFUN2: 15

        .= ((f1 (#) (f2 | X)) /. c) by A25, Th3;

      end;

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

      .= ((( dom f1) /\ ( dom f2)) /\ X) by Th3

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

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

      .= ( dom (f1 (#) (f2 | X))) by Th3;

      hence thesis by A18, PARTFUN2: 1;

    end;

    theorem :: CFUNCT_1:54



     Th53: (( - f) | X) = ( - (f | X)) & ((f ^ ) | X) = ((f | X) ^ ) & ( |.f.| | X) = |.(f | X).|

    proof



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

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

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

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

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

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

       A2:

      now

        let c;

        assume

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

        then

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

        then

         A5: c in X by XBOOLE_0:def 4;



         A6: c in ( dom ( - f)) by A4, XBOOLE_0:def 4;

        then c in ( dom f) by Th5;

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

        then

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

        then

         A8: c in ( dom ( - (f | X))) by Th5;



        thus ((( - f) | X) /. c) = (( - f) /. c) by A3, PARTFUN2: 15

        .= ( - (f /. c)) by A6, Th5

        .= ( - ((f | X) /. c)) by A7, PARTFUN2: 15

        .= (( - (f | X)) /. c) by A8, Th5;

      end;

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

      .= (( dom f) /\ X) by Th5

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

      .= ( dom ( - (f | X))) by Th5;

      hence (( - f) | X) = ( - (f | X)) by A2, PARTFUN2: 1;



       A9: ( dom ((f | X) ^ )) c= ( dom (f | X)) by Th6;

      now

        let c;

        assume

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

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

        then

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



        thus (((f ^ ) | X) /. c) = ((f ^ ) /. c) by A10, PARTFUN2: 15

        .= ((f /. c) " ) by A11, Def2

        .= (((f | X) /. c) " ) by A9, A1, A10, PARTFUN2: 15

        .= (((f | X) ^ ) /. c) by A1, A10, Def2;

      end;

      hence ((f ^ ) | X) = ((f | X) ^ ) by A1, PARTFUN2: 1;



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

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

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

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

      now

        let c;



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

        assume

         A14: c in ( dom ( |.f.| | X));

        then

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

        c in (( dom |.f.|) /\ X) by A14, RELAT_1: 61;

        then

         A16: c in ( dom |.f.|) by XBOOLE_0:def 4;



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

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

        .= |.(f /. c).| by A16, A13, PARTFUN1:def 6

        .= |.((f | X) /. c).| by A15, PARTFUN2: 15

        .= |.((f | X) . c).| by A15, PARTFUN1:def 6

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

      end;

      hence thesis by A12, PARTFUN1: 5;

    end;

    theorem :: CFUNCT_1:55

    ((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 Th51

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



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

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



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

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

    end;

    theorem :: CFUNCT_1:56

    ((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 Th38

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

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

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



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

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

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



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

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

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

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

    end;

    theorem :: CFUNCT_1:57

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

    proof

       A1:

      now

        let c;

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

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



        thus (((r (#) f) | X) /. c) = ((r (#) f) /. c) by A2, PARTFUN2: 15

        .= (r * (f /. c)) by A5, Th4

        .= (r * ((f | X) /. c)) by A6, PARTFUN2: 15

        .= ((r (#) (f | X)) /. c) by A7, Th4;

      end;

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

      .= (( dom f) /\ X) by Th4

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

      .= ( dom (r (#) (f | X))) by Th4;

      hence thesis by A1, PARTFUN2: 1;

    end;

    begin

    theorem :: CFUNCT_1:58



     Th57: (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

        proof

          assume f1 is total & f2 is total;

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



          hence ( dom (f1 + f2)) = (C /\ C) by VALUED_1:def 1

          .= C;

        end;

        assume (f1 + f2) is total;

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

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

        then C c= ( dom f1) & C c= ( dom f2) by XBOOLE_1: 17;

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

      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

        proof

          assume f1 is total & f2 is total;

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



          hence ( dom (f1 - f2)) = (C /\ C) by Th2

          .= C;

        end;

        assume (f1 - f2) is total;

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

        then (( dom f1) /\ ( dom f2)) = C by Th2;

        then C c= ( dom f1) & C c= ( dom f2) by XBOOLE_1: 17;

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

      end;

      thus f1 is total & f2 is total implies (f1 (#) f2) is total

      proof

        assume f1 is total & f2 is total;

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



        hence ( dom (f1 (#) f2)) = (C /\ C) by Th3

        .= C;

      end;

      assume (f1 (#) f2) is total;

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

      then (( dom f1) /\ ( dom f2)) = C by Th3;

      then C c= ( dom f1) & C c= ( dom f2) by XBOOLE_1: 17;

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

    end;

    theorem :: CFUNCT_1:59



     Th58: f is total iff (r (#) f) is total by Th4;

    theorem :: CFUNCT_1:60



     Th59: f is total iff ( - f) is total by Th58;

    theorem :: CFUNCT_1:61



     Th60: f is total iff |.f.| is total by VALUED_1:def 11;

    theorem :: CFUNCT_1:62



     Th61: (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 " { 0c }) c= C;

        then (f " { 0c }) c= (( dom f) \ (f " { 0c })) by A1, Def2;

        hence (f " { 0 }) = {} by XBOOLE_1: 38;

        then C = (( dom f) \ {} ) by A1, Def2;

        hence ( dom f) = C;

      end;

      assume

       A2: (f " { 0 }) = {} & f is total;



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

      .= C by A2;

    end;

    theorem :: CFUNCT_1:63



     Th62: 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 }) = {} & f2 is total;

        (f2 ^ ) is total by A2, Th61;

        then (f1 (#) (f2 ^ )) is total by A1, Th57;

        hence thesis by Th38;

      end;

      assume (f1 / f2) is total;

      then

       A3: (f1 (#) (f2 ^ )) is total by Th38;

      hence f1 is total by Th57;

      (f2 ^ ) is total by A3, Th57;

      hence thesis by Th61;

    end;

    theorem :: CFUNCT_1:64

    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

       A1: f1 is total & f2 is total;

      then (f1 + f2) is total by Th57;

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

      hence ((f1 + f2) /. c) = ((f1 /. c) + (f2 /. c)) by Th1;

      (f1 - f2) is total by A1, Th57;

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

      hence ((f1 - f2) /. c) = ((f1 /. c) - (f2 /. c)) by Th2;

      (f1 (#) f2) is total by A1, Th57;

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

      hence thesis by Th3;

    end;

    theorem :: CFUNCT_1:65

    f is total implies ((r (#) f) /. c) = (r * (f /. c))

    proof

      assume f is total;

      then (r (#) f) is total by Th58;

      then ( dom (r (#) f)) = C;

      hence thesis by Th4;

    end;

    theorem :: CFUNCT_1:66

    f is total implies (( - f) /. c) = ( - (f /. c)) & ( |.f.| . c) = |.(f /. c).|

    proof

      assume

       A1: f is total;

      then |.f.| is total by Th60;

      then

       A2: ( dom |.f.|) = ( dom f) & ( dom |.f.|) = C by VALUED_1:def 11;

      ( - f) is total by A1, Th59;

      then ( dom ( - f)) = C;

      hence (( - f) /. c) = ( - (f /. c)) by Th5;



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

      .= |.(f /. c).| by A2, PARTFUN1:def 6;

    end;

    theorem :: CFUNCT_1:67

    (f ^ ) is total implies ((f ^ ) /. c) = ((f /. c) " ) by Def2;

    theorem :: CFUNCT_1:68

    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;

      (f2 " { 0c }) = {} & f2 is total by A2, Th61;

      then (f1 / f2) is total by A1, Th62;

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

      hence thesis by Def1;

    end;

    begin



     Lm3: |.f.| is bounded iff f is bounded

    proof



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

      thus |.f.| is bounded implies f is bounded

      proof

        assume |.f.| is bounded;

        then

        consider r1 be Real such that

         A2: for y st y in ( dom |.f.|) holds |.(( abs f) . y).| < r1;

        take r1;

        let y;

        assume

         A3: y in ( dom f);

        then |.(( abs f) . y).| < r1 by A1, A2;

        then |. |.(f . y).|.| < r1 by A1, A3, VALUED_1:def 11;

        hence thesis;

      end;

      given r1 such that

       A4: for y st y in ( dom f) holds |.(f . y).| < r1;

      now

        take r1;

        let y;

        assume

         A5: y in ( dom |.f.|);

        then |. |.(f . y).|.| < r1 by A1, A4;

        hence |.(( abs f) . y).| < r1 by A5, VALUED_1:def 11;

      end;

      hence thesis;

    end;

    theorem :: CFUNCT_1:69



     Th68: (f | Y) is bounded iff ex p be Real st for c st c in (Y /\ ( dom f)) holds |.(f /. c).| <= p

    proof



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



       A2: ( dom ( |.f.| | Y)) = (Y /\ ( dom |.f.|)) by RELAT_1: 61;



       A3: ( |.f.| | Y) = |.(f | Y).| by RFUNCT_1: 46;

      hereby

        assume (f | Y) is bounded;

        then ( |.f.| | Y) is bounded by A3, Lm3;

        then

        consider p be Real such that

         A4: for c be object st c in ( dom ( |.f.| | Y)) holds |.(( |.f.| | Y) . c).| <= p by RFUNCT_1: 72;

        now

          let c such that

           A5: c in (Y /\ ( dom f));

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

          then

           A6: (f . c) = (f /. c) by PARTFUN1:def 6;

           |.(( |.f.| | Y) . c).| = |.( |.f.| . c).| by A1, A2, A5, FUNCT_1: 47

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

          hence |.(f /. c).| <= p by A1, A2, A4, A5, A6;

        end;

        hence ex p be Real st for c st c in (Y /\ ( dom f)) holds |.(f /. c).| <= p;

      end;

      given p be Real such that

       A7: for c st c in (Y /\ ( dom f)) holds |.(f /. c).| <= p;



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

      now

        let c be object such that

         A9: c in ( dom ( |.f.| | Y));



         A10: c in ( dom |.f.|) by A9, RELAT_1: 57;

         |.(( |.f.| | Y) . c).| = |.( |.f.| . c).| by A9, FUNCT_1: 47

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

        .= |. |.(f /. c).|.| by A1, A10, PARTFUN1:def 6;

        hence |.(( |.f.| | Y) . c).| <= p by A2, A7, A8, A9;

      end;

      then ( |.f.| | Y) is bounded by RFUNCT_1: 72;

      hence thesis by A3, Lm3;

    end;

    theorem :: CFUNCT_1:70

    Y c= X & (f | X) is bounded implies (f | Y) is bounded

    proof

      assume that

       A1: Y c= X and

       A2: (f | X) is bounded;

      ( |.f.| | X) = |.(f | X).| by RFUNCT_1: 46;

      then ( |.f.| | X) is bounded by A2, Lm3;

      then ( |.f.| | Y) = |.(f | Y).| & ( |.f.| | Y) is bounded by A1, RFUNCT_1: 46, RFUNCT_1: 74;

      hence thesis by Lm3;

    end;

    theorem :: CFUNCT_1:71

    X misses ( dom f) implies (f | X) is bounded

    proof

      assume (X /\ ( dom f)) = {} ;

      then for c holds c in (X /\ ( dom f)) implies |.(f /. c).| <= 0 ;

      hence thesis by Th68;

    end;

    theorem :: CFUNCT_1:72



     Th71: (f | Y) is bounded implies ((r (#) f) | Y) is bounded

    proof

      assume

       A1: (f | Y) is bounded;

      ( |.f.| | Y) = |.(f | Y).| by RFUNCT_1: 46;

      then ( |.f.| | Y) is bounded by A1, Lm3;

      then (( |.r.| (#) |.f.|) | Y) is bounded by RFUNCT_1: 80;

      then ( |.(r (#) f).| | Y) = |.((r (#) f) | Y).| & ( |.(r (#) f).| | Y) is bounded by Th30, RFUNCT_1: 46;

      hence thesis by Lm3;

    end;

    theorem :: CFUNCT_1:73

    ( |.f.| | X) is bounded_below

    proof

      now

        take z = 0 ;

        let c be object;



         A1: z <= |.(f /. c).| by COMPLEX1: 46;

        assume c in (X /\ ( dom |.f.|));

        then

         A2: c in ( dom |.f.|) by XBOOLE_0:def 4;

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

        then (f . c) = (f /. c) by A2, PARTFUN1:def 6;

        hence z <= ( |.f.| . c) by A1, VALUED_1: 18;

      end;

      hence thesis by RFUNCT_1: 71;

    end;

    theorem :: CFUNCT_1:74



     Th73: (f | Y) is bounded implies ( |.f.| | Y) is bounded & (( - f) | Y) is bounded

    proof

      assume

       A1: (f | Y) is bounded;

      ( |.f.| | Y) = |.(f | Y).| by RFUNCT_1: 46;

      hence ( |.f.| | Y) is bounded by A1, Lm3;

      thus thesis by A1, Th71;

    end;

    theorem :: CFUNCT_1:75



     Th74: (f1 | X) is bounded & (f2 | Y) is bounded implies ((f1 + f2) | (X /\ Y)) is bounded

    proof

      assume that

       A1: (f1 | X) is bounded and

       A2: (f2 | Y) is bounded;

      consider r1 such that

       A3: for c st c in (X /\ ( dom f1)) holds |.(f1 /. c).| <= r1 by A1, Th68;

      consider r2 such that

       A4: for c st c in (Y /\ ( dom f2)) holds |.(f2 /. c).| <= r2 by A2, Th68;

      ex p1 st for c st c in ((X /\ Y) /\ ( dom (f1 + f2))) holds |.((f1 + f2) /. c).| <= p1

      proof

        take r0 = (r1 + r2);

        let c;



         A5: |.((f1 /. c) + (f2 /. c)).| <= ( |.(f1 /. c).| + |.(f2 /. c).|) by COMPLEX1: 56;

        assume

         A6: c in ((X /\ Y) /\ ( dom (f1 + f2)));

        then

         A7: c in (X /\ Y) by XBOOLE_0:def 4;

        then

         A8: c in X by XBOOLE_0:def 4;



         A9: c in Y by A7, XBOOLE_0:def 4;



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

        then

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

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

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

        then

         A12: |.(f2 /. c).| <= r2 by A4;

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

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

        then |.(f1 /. c).| <= r1 by A3;

        then ( |.(f1 /. c).| + |.(f2 /. c).|) <= r0 by A12, XREAL_1: 7;

        then |.((f1 /. c) + (f2 /. c)).| <= r0 by A5, XXREAL_0: 2;

        hence thesis by A10, Th1;

      end;

      hence thesis by Th68;

    end;

    theorem :: CFUNCT_1:76



     Th75: (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;

      consider r1 such that

       A3: for c st c in (X /\ ( dom f1)) holds |.(f1 /. c).| <= r1 by A1, Th68;

      consider r2 such that

       A4: for c st c in (Y /\ ( dom f2)) holds |.(f2 /. c).| <= r2 by A2, Th68;

      now

        take r = (r1 * r2);

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

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

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

        then

         A10: |.(f1 /. c).| <= r1 by A3;



         A11: c in Y by A6, XBOOLE_0:def 4;

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

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

        then

         A12: |.(f2 /. c).| <= r2 by A4;

         0 <= |.(f1 /. c).| & 0 <= |.(f2 /. c).| by COMPLEX1: 46;

        then ( |.(f1 /. c).| * |.(f2 /. c).|) <= r by A10, A12, XREAL_1: 66;

        then |.((f1 /. c) * (f2 /. c)).| <= r by COMPLEX1: 65;

        hence |.((f1 (#) f2) /. c).| <= r by A8, Th3;

      end;

      hence ((f1 (#) f2) | (X /\ Y)) is bounded by Th68;

      (( - f2) | Y) is bounded by A2, Th73;

      hence thesis by A1, Th74;

    end;

    theorem :: CFUNCT_1:77

    (f | X) is bounded & (f | Y) is bounded implies (f | (X \/ Y)) is bounded

    proof

      assume that

       A1: (f | X) is bounded and

       A2: (f | Y) is bounded;

      ( |.f.| | Y) = |.(f | Y).| by RFUNCT_1: 46;

      then

       A3: ( |.f.| | Y) is bounded by A2, Lm3;

      ( |.f.| | X) = |.(f | X).| by RFUNCT_1: 46;

      then ( |.f.| | X) is bounded by A1, Lm3;

      then ( |.f.| | (X \/ Y)) = |.(f | (X \/ Y)).| & ( |.f.| | (X \/ Y)) is bounded by A3, RFUNCT_1: 46, RFUNCT_1: 87;

      hence thesis by Lm3;

    end;

    theorem :: CFUNCT_1:78

    (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 cr1 be Element of COMPLEX such that

       A3: for c st c in (X /\ ( dom f1)) holds (f1 /. c) = cr1 by A1, PARTFUN2: 35;

      consider cr2 be Element of COMPLEX such that

       A4: for c st c in (Y /\ ( dom f2)) holds (f2 /. c) = cr2 by A2, PARTFUN2: 35;



       A5: (cr1 + cr2) in COMPLEX by XCMPLX_0:def 2;

      now

        let c;

        assume

         A6: c in ((X /\ Y) /\ ( dom (f1 + f2)));

        then

         A7: c in (X /\ Y) by XBOOLE_0:def 4;

        then

         A8: c in X by XBOOLE_0:def 4;



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

        then

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

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

        then

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



         A12: c in Y by A7, XBOOLE_0:def 4;

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

        then

         A13: c in (Y /\ ( dom f2)) by A12, XBOOLE_0:def 4;



        thus ((f1 + f2) /. c) = ((f1 /. c) + (f2 /. c)) by A9, Th1

        .= (cr1 + (f2 /. c)) by A3, A11

        .= (cr1 + cr2) by A4, A13;

      end;

      hence ((f1 + f2) | (X /\ Y)) is constant by A5, PARTFUN2: 35;



       A14: (cr1 - cr2) in COMPLEX by XCMPLX_0:def 2;

      now

        let c;

        assume

         A15: c in ((X /\ Y) /\ ( dom (f1 - f2)));

        then

         A16: c in (X /\ Y) by XBOOLE_0:def 4;

        then

         A17: c in X by XBOOLE_0:def 4;



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

        then

         A19: c in (( dom f1) /\ ( dom f2)) by Th2;

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

        then

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



         A21: c in Y by A16, XBOOLE_0:def 4;

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

        then

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



        thus ((f1 - f2) /. c) = ((f1 /. c) - (f2 /. c)) by A18, Th2

        .= (cr1 - (f2 /. c)) by A3, A20

        .= (cr1 - cr2) by A4, A22;

      end;

      hence ((f1 - f2) | (X /\ Y)) is constant by A14, PARTFUN2: 35;



       A23: (cr1 * cr2) in COMPLEX by XCMPLX_0:def 2;

      now

        let c;

        assume

         A24: c in ((X /\ Y) /\ ( dom (f1 (#) f2)));

        then

         A25: c in (X /\ Y) by XBOOLE_0:def 4;

        then

         A26: c in X by XBOOLE_0:def 4;



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

        then

         A28: c in (( dom f1) /\ ( dom f2)) by Th3;

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

        then

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



         A30: c in Y by A25, XBOOLE_0:def 4;

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

        then

         A31: c in (Y /\ ( dom f2)) by A30, XBOOLE_0:def 4;



        thus ((f1 (#) f2) /. c) = ((f1 /. c) * (f2 /. c)) by A27, Th3

        .= (cr1 * (f2 /. c)) by A3, A29

        .= (cr1 * cr2) by A4, A31;

      end;

      hence thesis by A23, PARTFUN2: 35;

    end;

    theorem :: CFUNCT_1:79



     Th78: (f | Y) is constant implies ((q (#) f) | Y) is constant

    proof

      assume (f | Y) is constant;

      then

      consider r be Element of COMPLEX such that

       A1: for c st c in (Y /\ ( dom f)) holds (f /. c) = r by PARTFUN2: 35;



       A2: (q * r) in COMPLEX by XCMPLX_0:def 2;

      now

        let c;

        assume

         A3: c in (Y /\ ( dom (q (#) f)));

        then

         A4: c in Y by XBOOLE_0:def 4;



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

        then c in ( dom f) by Th4;

        then

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



        thus ((q (#) f) /. c) = (q * (f /. c)) by A5, Th4

        .= (q * r) by A1, A6;

      end;

      hence thesis by A2, PARTFUN2: 35;

    end;

    theorem :: CFUNCT_1:80



     Th79: (f | Y) is constant implies ( |.f.| | Y) is constant & (( - f) | Y) is constant

    proof

      assume (f | Y) is constant;

      then

      consider r be Element of COMPLEX such that

       A1: for c st c in (Y /\ ( dom f)) holds (f /. c) = r by PARTFUN2: 35;

      reconsider rr = |.r.| as Element of REAL by XREAL_0:def 1;

      now

        let c;

        assume

         A2: c in (Y /\ ( dom |.f.|));

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

        then

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

        c in Y by A2, XBOOLE_0:def 4;

        then

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

        (f . c) = (f /. c) by A3, PARTFUN1:def 6;



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

        .= rr by A1, A4;

      end;

      hence ( |.f.| | Y) is constant by PARTFUN2: 57;



       A5: ( - r) in COMPLEX by XCMPLX_0:def 2;

      now

        let c;

        assume

         A6: c in (Y /\ ( dom ( - f)));

        then c in (Y /\ ( dom f)) by Th5;

        then

         A7: ( - (f /. c)) = ( - r) by A1;

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

        hence (( - f) /. c) = ( - r) by A7, Th5;

      end;

      hence thesis by A5, PARTFUN2: 35;

    end;

    theorem :: CFUNCT_1:81



     Th80: (f | Y) is constant implies (f | Y) is bounded

    proof

      assume (f | Y) is constant;

      then

      consider r be Element of COMPLEX such that

       A1: for c st c in (Y /\ ( dom f)) holds (f /. c) = r by PARTFUN2: 35;

      now

        take p = |.r.|;

        let c;

        assume c in (Y /\ ( dom f));

        hence |.(f /. c).| <= p by A1;

      end;

      hence thesis by Th68;

    end;

    theorem :: CFUNCT_1:82

    (f | Y) is constant implies (for r holds ((r (#) f) | Y) is bounded) & (( - f) | Y) is bounded & ( |.f.| | Y) is bounded

    proof

      assume

       A1: (f | Y) is constant;

      hence for r holds ((r (#) f) | Y) is bounded by Th78, Th80;

      thus (( - f) | Y) is bounded by A1, Th79, Th80;

      ( |.f.| | Y) is constant by A1, Th79;

      hence thesis;

    end;

    theorem :: CFUNCT_1:83



     Th82: (f1 | X) is bounded & (f2 | Y) is constant implies ((f1 + f2) | (X /\ Y)) is bounded

    proof

      assume that

       A1: (f1 | X) is bounded and

       A2: (f2 | Y) is constant;

      (f2 | Y) is bounded by A2, Th80;

      hence thesis by A1, Th74;

    end;

    theorem :: CFUNCT_1:84

    (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

      assume that

       A1: (f1 | X) is bounded and

       A2: (f2 | Y) is constant;

      (( - f2) | Y) is constant by A2, Th79;

      hence ((f1 - f2) | (X /\ Y)) is bounded by A1, Th82;



       A3: (f2 | Y) is bounded by A2, Th80;

      hence ((f2 - f1) | (X /\ Y)) is bounded by A1, Th75;

      thus thesis by A1, A3, Th75;

    end;

    theorem :: CFUNCT_1:85

     |.f.| is bounded iff f is bounded by Lm3;

    registration

      let D be non empty set;

      let f be Function of COMPLEX , D;

      let c be Complex;

      identify f . c with f /. c;

      correctness

      proof

        reconsider c as Element of COMPLEX by XCMPLX_0:def 2;

        (f /. c) = (f . c) by FUNCT_2: 99;

        hence thesis;

      end;

    end