vfunct_2.miz



    begin

    reserve M for non empty set;

    reserve V for ComplexNormSpace;

    reserve f,f1,f2,f3 for PartFunc of M, V;

    reserve z,z1,z2 for Complex;

    definition

      let M be non empty set;

      let V be ComplexNormSpace;

      let f1 be PartFunc of M, COMPLEX ;

      let f2 be PartFunc of M, V;

      deffunc F( Element of M) = ((f1 /. $1) * (f2 /. $1));

      defpred P[ set] means $1 in (( dom f1) /\ ( dom f2));

      set X = (( dom f1) /\ ( dom f2));

      :: VFUNCT_2:def1

      func f1 (#) f2 -> PartFunc of M, V means

      : Def1: ( dom it ) = (( dom f1) /\ ( dom f2)) & for c be Element of M st c in ( dom it ) holds (it /. c) = ((f1 /. c) * (f2 /. c));

      existence

      proof

        consider F be PartFunc of M, V such that

         A1: for c be Element of M holds c in ( dom F) iff P[c] and

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

        take F;

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

        let c be Element of M;

        assume c in ( dom F);

        hence thesis by A2;

      end;

      uniqueness

      proof

        thus for f,g be PartFunc of M, V st (( dom f) = X & for c be Element of M st c in ( dom f) holds (f /. c) = F(c)) & (( dom g) = X & for c be Element of M st c in ( dom g) holds (g /. c) = F(c)) holds f = g from PARTFUN2:sch 3;

      end;

    end

    definition

      let X be non empty set;

      let V be ComplexNormSpace;

      let f be PartFunc of X, V;

      let z be Complex;

      deffunc F( Element of X) = (z * (f /. $1));

      defpred P[ set] means $1 in ( dom f);

      set M = ( dom f);

      :: VFUNCT_2:def2

      func z (#) f -> PartFunc of X, V means

      : Def2: ( dom it ) = ( dom f) & for x be Element of X st x in ( dom it ) holds (it /. x) = (z * (f /. x));

      existence

      proof

        consider F be PartFunc of X, V such that

         A1: for x be Element of X holds x in ( dom F) iff P[x] and

         A2: for x be Element of X st x in ( dom F) holds (F /. x) = F(x) from PARTFUN2:sch 2;

        take F;

        thus ( dom F) = ( dom f) by A1, SUBSET_1: 3;

        let x be Element of X;

        assume x in ( dom F);

        hence thesis by A2;

      end;

      uniqueness

      proof

        thus for f,g be PartFunc of X, V st (( dom f) = M & for x be Element of X st x in ( dom f) holds (f /. x) = F(x)) & (( dom g) = M & for x be Element of X st x in ( dom g) holds (g /. x) = F(x)) holds f = g from PARTFUN2:sch 3;

      end;

    end

    theorem :: VFUNCT_2:1

    for f1 be PartFunc of M, COMPLEX , f2 be PartFunc of M, V holds (( dom (f1 (#) f2)) \ ((f1 (#) f2) " {( 0. V)})) = ((( dom f1) \ (f1 " { 0 })) /\ (( dom f2) \ (f2 " {( 0. V)})))

    proof

      let f1 be PartFunc of M, COMPLEX ;

      let f2 be PartFunc of M, V;

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

      proof

        let x be object;

        assume

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

        then

        reconsider x1 = x as Element of M;

        

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

        then

         A3: x1 in (( dom f1) /\ ( dom f2)) by Def1;

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

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

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

        then

         A4: ((f1 /. x1) * (f2 /. x1)) <> ( 0. V) by A2, Def1;

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

        then

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

        (f2 /. x1) <> ( 0. V) by A4, CLVECT_1: 1;

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

        then

         A6: not x1 in (f2 " {( 0. V)}) by PARTFUN2: 26;

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

        then

         A7: x in (( dom f2) \ (f2 " {( 0. V)})) by A6, XBOOLE_0:def 5;

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

        then not (f1 . x1) in { 0 } by A5, PARTFUN1:def 6;

        then

         A8: not x1 in (f1 " { 0 }) by FUNCT_1:def 7;

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

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

        hence thesis by A7, XBOOLE_0:def 4;

      end;

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

      proof

        let x be object;

        assume

         A9: x in ((( dom f1) \ (f1 " { 0 })) /\ (( dom f2) \ (f2 " {( 0. V)})));

        then

        reconsider x1 = x as Element of M;

        

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

        then

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

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

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

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

        then

         A12: (f1 /. x1) <> 0 by A11, PARTFUN1:def 6;

        

         A13: x in (( dom f2) \ (f2 " {( 0. V)})) by A9, XBOOLE_0:def 4;

        then

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

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

        then

         A15: x1 in ( dom (f1 (#) f2)) by Def1;

         not x in (f2 " {( 0. V)}) by A13, XBOOLE_0:def 5;

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

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

        then ((f1 /. x1) * (f2 /. x1)) <> ( 0. V) by A12, CLVECT_1: 2;

        then ((f1 (#) f2) /. x1) <> ( 0. V) by A15, Def1;

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

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

        hence thesis by A15, XBOOLE_0:def 5;

      end;

    end;

    theorem :: VFUNCT_2:2

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

    proof

      now

        let c be Element of M;

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

        proof

          assume

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

          then

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

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

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

          then ||.(f /. c).|| = 0 by A2, NORMSP_0:def 3;

          then (f /. c) = ( 0. V) by NORMSP_0:def 5;

          then

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

          c in ( dom f) by A2, NORMSP_0:def 3;

          hence thesis by A3, PARTFUN2: 26;

        end;

        assume

         A4: c in (f " {( 0. V)});

        then c in ( dom f) by PARTFUN2: 26;

        then

         A5: c in ( dom ||.f.||) by NORMSP_0:def 3;

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

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

        then ||.(f /. c).|| = 0 by NORMSP_0:def 6;

        then ( ||.f.|| . c) = 0 by A5, NORMSP_0:def 3;

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

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

      end;

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

      now

        let c be Element of M;

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

        proof

          assume

           A6: c in (( - f) " {( 0. V)});

          then

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

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

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

          then ( - ( - (f /. c))) = ( - ( 0. V)) by A7, VFUNCT_1:def 5;

          then ( - ( - (f /. c))) = ( 0. V) by RLVECT_1: 12;

          then (f /. c) = ( 0. V) by RLVECT_1: 17;

          then

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

          c in ( dom f) by A7, VFUNCT_1:def 5;

          hence thesis by A8, PARTFUN2: 26;

        end;

        assume

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

        then c in ( dom f) by PARTFUN2: 26;

        then

         A10: c in ( dom ( - f)) by VFUNCT_1:def 5;

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

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

        then (( - f) /. c) = ( - ( 0. V)) by A10, VFUNCT_1:def 5;

        then (( - f) /. c) = ( 0. V) by RLVECT_1: 12;

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

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

      end;

      hence thesis by SUBSET_1: 3;

    end;

    theorem :: VFUNCT_2:3

    z <> 0c implies ((z (#) f) " {( 0. V)}) = (f " {( 0. V)})

    proof

      assume

       A1: z <> 0c ;

      now

        let x be Element of M;

        thus x in ((z (#) f) " {( 0. V)}) implies x in (f " {( 0. V)})

        proof

          assume

           A2: x in ((z (#) f) " {( 0. V)});

          then

           A3: x in ( dom (z (#) f)) by PARTFUN2: 26;

          ((z (#) f) /. x) in {( 0. V)} by A2, PARTFUN2: 26;

          then ((z (#) f) /. x) = ( 0. V) by TARSKI:def 1;

          then (z * (f /. x)) = ( 0. V) by A3, Def2;

          then (z * (f /. x)) = (z * ( 0. V)) by CLVECT_1: 1;

          then (f /. x) = ( 0. V) by A1, CLVECT_1: 11;

          then

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

          x in ( dom f) by A3, Def2;

          hence thesis by A4, PARTFUN2: 26;

        end;

        assume

         A5: x in (f " {( 0. V)});

        then x in ( dom f) by PARTFUN2: 26;

        then

         A6: x in ( dom (z (#) f)) by Def2;

        (f /. x) in {( 0. V)} by A5, PARTFUN2: 26;

        then (z * (f /. x)) = (z * ( 0. V)) by TARSKI:def 1;

        then (z * (f /. x)) = ( 0. V) by CLVECT_1: 1;

        then ((z (#) f) /. x) = ( 0. V) by A6, Def2;

        then ((z (#) f) /. x) in {( 0. V)} by TARSKI:def 1;

        hence x in ((z (#) f) " {( 0. V)}) by A6, PARTFUN2: 26;

      end;

      hence thesis by SUBSET_1: 3;

    end;

    theorem :: VFUNCT_2:4

    

     Th4: (f1 + f2) = (f2 + f1);

    definition

      let M, V;

      let f1, f2;

      :: original: +

      redefine

      func f1 + f2;

      commutativity by Th4;

    end

    theorem :: VFUNCT_2:5

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

    proof

      

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

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

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

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

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

      now

        let x be Element of M;

        assume

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

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

        then

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

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

        then

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

        

        thus (((f1 + f2) + f3) /. x) = (((f1 + f2) /. x) + (f3 /. x)) by A2, VFUNCT_1:def 1

        .= (((f1 /. x) + (f2 /. x)) + (f3 /. x)) by A3, VFUNCT_1:def 1

        .= ((f1 /. x) + ((f2 /. x) + (f3 /. x))) by RLVECT_1:def 3

        .= ((f1 /. x) + ((f2 + f3) /. x)) by A4, VFUNCT_1:def 1

        .= ((f1 + (f2 + f3)) /. x) by A1, A2, VFUNCT_1:def 1;

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_2:6

    for f1,f2 be PartFunc of M, COMPLEX , f3 be PartFunc of M, V holds ((f1 (#) f2) (#) f3) = (f1 (#) (f2 (#) f3))

    proof

      let f1,f2 be PartFunc of M, COMPLEX ;

      let f3 be PartFunc of M, V;

      

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

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

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

      now

        let x be Element of M;

        assume

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

        then x in (( dom (f1 (#) f2)) /\ ( dom f3)) by Def1;

        then

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

        

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

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

        then

         A5: (f1 . x) = (f1 /. x) by PARTFUN1:def 6;

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

        then

         A6: (f2 . x) = (f2 /. x) by PARTFUN1:def 6;

        

         A7: ((f1 (#) f2) /. x) = ((f1 (#) f2) . x) by A3, PARTFUN1:def 6

        .= ((f1 /. x) * (f2 /. x)) by A3, A5, A6, VALUED_1:def 4;

        x in (( dom f1) /\ ( dom (f2 (#) f3))) by A1, A2, Def1;

        then

         A8: x in ( dom (f2 (#) f3)) by XBOOLE_0:def 4;

        

        thus (((f1 (#) f2) (#) f3) /. x) = (((f1 (#) f2) /. x) * (f3 /. x)) by A2, Def1

        .= ((f1 /. x) * ((f2 /. x) * (f3 /. x))) by A7, CLVECT_1:def 4

        .= ((f1 /. x) * ((f2 (#) f3) /. x)) by A8, Def1

        .= ((f1 (#) (f2 (#) f3)) /. x) by A1, A2, Def1;

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_2:7

    for f1,f2 be PartFunc of M, COMPLEX holds ((f1 + f2) (#) f3) = ((f1 (#) f3) + (f2 (#) f3))

    proof

      let f1,f2 be PartFunc of M, COMPLEX ;

      

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

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

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

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

      

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

      now

        let x be Element of M;

        assume

         A3: x in ( dom ((f1 + f2) (#) f3));

        then

         A4: x in (( dom (f1 (#) f3)) /\ ( dom (f2 (#) f3))) by A1, VFUNCT_1:def 1;

        then

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

        x in (( dom (f1 + f2)) /\ ( dom f3)) by A3, Def1;

        then

         A6: x in ( dom (f1 + f2)) by XBOOLE_0:def 4;

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

        then

         A7: (f1 /. x) = (f1 . x) by PARTFUN1:def 6;

        x in ( dom f2) by A2, A6, XBOOLE_0:def 4;

        then

         A8: (f2 /. x) = (f2 . x) by PARTFUN1:def 6;

        

         A9: ((f1 + f2) /. x) = ((f1 + f2) . x) by A6, PARTFUN1:def 6

        .= ((f1 /. x) + (f2 /. x)) by A6, A7, A8, VALUED_1:def 1;

        

         A10: x in ( dom (f2 (#) f3)) by A4, XBOOLE_0:def 4;

        

        thus (((f1 + f2) (#) f3) /. x) = (((f1 + f2) /. x) * (f3 /. x)) by A3, Def1

        .= (((f1 /. x) * (f3 /. x)) + ((f2 /. x) * (f3 /. x))) by A9, CLVECT_1:def 3

        .= (((f1 (#) f3) /. x) + ((f2 /. x) * (f3 /. x))) by A5, Def1

        .= (((f1 (#) f3) /. x) + ((f2 (#) f3) /. x)) by A10, Def1

        .= (((f1 (#) f3) + (f2 (#) f3)) /. x) by A1, A3, VFUNCT_1:def 1;

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_2:8

    for f3 be PartFunc of M, COMPLEX holds (f3 (#) (f1 + f2)) = ((f3 (#) f1) + (f3 (#) f2))

    proof

      let f3 be PartFunc of M, COMPLEX ;

      

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

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

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

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

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

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

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

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

      now

        let x be Element of M;

        assume

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

        then x in (( dom f3) /\ ( dom (f1 + f2))) by Def1;

        then

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

        

         A4: x in (( dom (f3 (#) f1)) /\ ( dom (f3 (#) f2))) by A1, A2, VFUNCT_1:def 1;

        then

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

        

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

        

        thus ((f3 (#) (f1 + f2)) /. x) = ((f3 /. x) * ((f1 + f2) /. x)) by A2, Def1

        .= ((f3 /. x) * ((f1 /. x) + (f2 /. x))) by A3, VFUNCT_1:def 1

        .= (((f3 /. x) * (f1 /. x)) + ((f3 /. x) * (f2 /. x))) by CLVECT_1:def 2

        .= (((f3 (#) f1) /. x) + ((f3 /. x) * (f2 /. x))) by A5, Def1

        .= (((f3 (#) f1) /. x) + ((f3 (#) f2) /. x)) by A6, Def1

        .= (((f3 (#) f1) + (f3 (#) f2)) /. x) by A1, A2, VFUNCT_1:def 1;

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_2:9

    for f1 be PartFunc of M, COMPLEX holds (z (#) (f1 (#) f2)) = ((z (#) f1) (#) f2)

    proof

      let f1 be PartFunc of M, COMPLEX ;

      

       A1: ( dom (f1 (#) f2)) = (( dom f1) /\ ( dom f2)) by Def1;

      

       A2: ( dom (z (#) (f1 (#) f2))) = ( dom (f1 (#) f2)) by Def2

      .= (( dom (z (#) f1)) /\ ( dom f2)) by A1, VALUED_1:def 5

      .= ( dom ((z (#) f1) (#) f2)) by Def1;

      now

        let x be Element of M;

        assume

         A3: x in ( dom (z (#) (f1 (#) f2)));

        then x in (( dom (z (#) f1)) /\ ( dom f2)) by A2, Def1;

        then x in ( dom (z (#) f1)) by XBOOLE_0:def 4;

        then

         A4: ((z (#) f1) /. x) = ((z (#) f1) . x) by PARTFUN1:def 6;

        

         A5: x in ( dom (f1 (#) f2)) by A3, Def2;

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

        then

         A6: (f1 /. x) = (f1 . x) by PARTFUN1:def 6;

        

        thus ((z (#) (f1 (#) f2)) /. x) = (z * ((f1 (#) f2) /. x)) by A3, Def2

        .= (z * ((f1 /. x) * (f2 /. x))) by A5, Def1

        .= ((z * (f1 /. x)) * (f2 /. x)) by CLVECT_1:def 4

        .= (((z (#) f1) /. x) * (f2 /. x)) by A4, A6, VALUED_1: 6

        .= (((z (#) f1) (#) f2) /. x) by A2, A3, Def1;

      end;

      hence thesis by A2, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_2:10

    for f1 be PartFunc of M, COMPLEX holds (z (#) (f1 (#) f2)) = (f1 (#) (z (#) f2))

    proof

      let f1 be PartFunc of M, COMPLEX ;

      

       A1: ( dom (z (#) (f1 (#) f2))) = ( dom (f1 (#) f2)) by Def2

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

      .= (( dom f1) /\ ( dom (z (#) f2))) by Def2

      .= ( dom (f1 (#) (z (#) f2))) by Def1;

      now

        let x be Element of M;

        assume

         A2: x in ( dom (z (#) (f1 (#) f2)));

        then

         A3: x in ( dom (f1 (#) f2)) by Def2;

        x in (( dom f1) /\ ( dom (z (#) f2))) by A1, A2, Def1;

        then

         A4: x in ( dom (z (#) f2)) by XBOOLE_0:def 4;

        

        thus ((z (#) (f1 (#) f2)) /. x) = (z * ((f1 (#) f2) /. x)) by A2, Def2

        .= (z * ((f1 /. x) * (f2 /. x))) by A3, Def1

        .= (((f1 /. x) * z) * (f2 /. x)) by CLVECT_1:def 4

        .= ((f1 /. x) * (z * (f2 /. x))) by CLVECT_1:def 4

        .= ((f1 /. x) * ((z (#) f2) /. x)) by A4, Def2

        .= ((f1 (#) (z (#) f2)) /. x) by A1, A2, Def1;

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_2:11

    for f1,f2 be PartFunc of M, COMPLEX holds ((f1 - f2) (#) f3) = ((f1 (#) f3) - (f2 (#) f3))

    proof

      let f1,f2 be PartFunc of M, COMPLEX ;

      

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

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

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

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

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

      .= ( dom ((f1 (#) f3) - (f2 (#) f3))) by VFUNCT_1:def 2;

      now

        let x be Element of M;

        assume

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

        then

         A3: x in (( dom (f1 (#) f3)) /\ ( dom (f2 (#) f3))) by A1, VFUNCT_1:def 2;

        then

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

        x in (( dom (f1 - f2)) /\ ( dom f3)) by A2, Def1;

        then

         A5: x in ( dom (f1 - f2)) by XBOOLE_0:def 4;

        then

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

        then

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

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

        then

         A8: (f1 /. x) = (f1 . x) by PARTFUN1:def 6;

        ((f1 + ( - f2)) /. x) = ((f1 + ( - f2)) . x) by A5, PARTFUN1:def 6;

        

        then

         A9: ((f1 + ( - f2)) /. x) = ((f1 . x) + (( - f2) . x)) by A5, VALUED_1:def 1

        .= ((f1 /. x) + (( - f2) /. x)) by A7, A8, PARTFUN1:def 6;

        ( dom ( - f2)) = ( dom f2) by VALUED_1: 8;

        then

         A10: (( - f2) . x) = ( - (f2 . x)) & (f2 /. x) = (f2 . x) by A7, PARTFUN1:def 6, VALUED_1: 8;

        

         A11: x in ( dom (f2 (#) f3)) by A3, XBOOLE_0:def 4;

        (( - f2) /. x) = (( - f2) . x) by A7, PARTFUN1:def 6;

        

        hence (((f1 - f2) (#) f3) /. x) = (((f1 /. x) - (f2 /. x)) * (f3 /. x)) by A2, A10, A9, Def1

        .= (((f1 /. x) * (f3 /. x)) - ((f2 /. x) * (f3 /. x))) by CLVECT_1: 10

        .= (((f1 (#) f3) /. x) - ((f2 /. x) * (f3 /. x))) by A4, Def1

        .= (((f1 (#) f3) /. x) - ((f2 (#) f3) /. x)) by A11, Def1

        .= (((f1 (#) f3) - (f2 (#) f3)) /. x) by A1, A2, VFUNCT_1:def 2;

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_2:12

    for f3 be PartFunc of M, COMPLEX holds ((f3 (#) f1) - (f3 (#) f2)) = (f3 (#) (f1 - f2))

    proof

      let f3 be PartFunc of M, COMPLEX ;

      

       A1: ( dom ((f3 (#) f1) - (f3 (#) f2))) = (( dom (f3 (#) f1)) /\ ( dom (f3 (#) f2))) by VFUNCT_1:def 2

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

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

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

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

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

      .= (( dom f3) /\ ( dom (f1 - f2))) by VFUNCT_1:def 2

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

      now

        let x be Element of M;

        assume

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

        then x in (( dom f3) /\ ( dom (f1 - f2))) by Def1;

        then

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

        

         A4: x in (( dom (f3 (#) f1)) /\ ( dom (f3 (#) f2))) by A1, A2, VFUNCT_1:def 2;

        then

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

        

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

        

        thus ((f3 (#) (f1 - f2)) /. x) = ((f3 /. x) * ((f1 - f2) /. x)) by A2, Def1

        .= ((f3 /. x) * ((f1 /. x) - (f2 /. x))) by A3, VFUNCT_1:def 2

        .= (((f3 /. x) * (f1 /. x)) - ((f3 /. x) * (f2 /. x))) by CLVECT_1: 9

        .= (((f3 (#) f1) /. x) - ((f3 /. x) * (f2 /. x))) by A5, Def1

        .= (((f3 (#) f1) /. x) - ((f3 (#) f2) /. x)) by A6, Def1

        .= (((f3 (#) f1) - (f3 (#) f2)) /. x) by A1, A2, VFUNCT_1:def 2;

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_2:13

    (z (#) (f1 + f2)) = ((z (#) f1) + (z (#) f2))

    proof

      

       A1: ( dom (z (#) (f1 + f2))) = ( dom (f1 + f2)) by Def2

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

      .= (( dom f1) /\ ( dom (z (#) f2))) by Def2

      .= (( dom (z (#) f1)) /\ ( dom (z (#) f2))) by Def2

      .= ( dom ((z (#) f1) + (z (#) f2))) by VFUNCT_1:def 1;

      now

        let x be Element of M;

        assume

         A2: x in ( dom (z (#) (f1 + f2)));

        then

         A3: x in ( dom (f1 + f2)) by Def2;

        

         A4: x in (( dom (z (#) f1)) /\ ( dom (z (#) f2))) by A1, A2, VFUNCT_1:def 1;

        then

         A5: x in ( dom (z (#) f1)) by XBOOLE_0:def 4;

        

         A6: x in ( dom (z (#) f2)) by A4, XBOOLE_0:def 4;

        

        thus ((z (#) (f1 + f2)) /. x) = (z * ((f1 + f2) /. x)) by A2, Def2

        .= (z * ((f1 /. x) + (f2 /. x))) by A3, VFUNCT_1:def 1

        .= ((z * (f1 /. x)) + (z * (f2 /. x))) by CLVECT_1:def 2

        .= (((z (#) f1) /. x) + (z * (f2 /. x))) by A5, Def2

        .= (((z (#) f1) /. x) + ((z (#) f2) /. x)) by A6, Def2

        .= (((z (#) f1) + (z (#) f2)) /. x) by A1, A2, VFUNCT_1:def 1;

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_2:14

    

     Th14: ((z1 * z2) (#) f) = (z1 (#) (z2 (#) f))

    proof

      

       A1: ( dom ((z1 * z2) (#) f)) = ( dom f) by Def2

      .= ( dom (z2 (#) f)) by Def2

      .= ( dom (z1 (#) (z2 (#) f))) by Def2;

      now

        let x be Element of M;

        assume

         A2: x in ( dom ((z1 * z2) (#) f));

        then

         A3: x in ( dom (z2 (#) f)) by A1, Def2;

        

        thus (((z1 * z2) (#) f) /. x) = ((z1 * z2) * (f /. x)) by A2, Def2

        .= (z1 * (z2 * (f /. x))) by CLVECT_1:def 4

        .= (z1 * ((z2 (#) f) /. x)) by A3, Def2

        .= ((z1 (#) (z2 (#) f)) /. x) by A1, A2, Def2;

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_2:15

    (z (#) (f1 - f2)) = ((z (#) f1) - (z (#) f2))

    proof

      

       A1: ( dom (z (#) (f1 - f2))) = ( dom (f1 - f2)) by Def2

      .= (( dom f1) /\ ( dom f2)) by VFUNCT_1:def 2

      .= (( dom f1) /\ ( dom (z (#) f2))) by Def2

      .= (( dom (z (#) f1)) /\ ( dom (z (#) f2))) by Def2

      .= ( dom ((z (#) f1) - (z (#) f2))) by VFUNCT_1:def 2;

      now

        let x be Element of M;

        assume

         A2: x in ( dom (z (#) (f1 - f2)));

        then

         A3: x in ( dom (f1 - f2)) by Def2;

        

         A4: x in (( dom (z (#) f1)) /\ ( dom (z (#) f2))) by A1, A2, VFUNCT_1:def 2;

        then

         A5: x in ( dom (z (#) f1)) by XBOOLE_0:def 4;

        

         A6: x in ( dom (z (#) f2)) by A4, XBOOLE_0:def 4;

        

        thus ((z (#) (f1 - f2)) /. x) = (z * ((f1 - f2) /. x)) by A2, Def2

        .= (z * ((f1 /. x) - (f2 /. x))) by A3, VFUNCT_1:def 2

        .= ((z * (f1 /. x)) - (z * (f2 /. x))) by CLVECT_1: 9

        .= (((z (#) f1) /. x) - (z * (f2 /. x))) by A5, Def2

        .= (((z (#) f1) /. x) - ((z (#) f2) /. x)) by A6, Def2

        .= (((z (#) f1) - (z (#) f2)) /. x) by A1, A2, VFUNCT_1:def 2;

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_2:16

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

    proof

      

       A1: ( dom (f1 - f2)) = (( dom f2) /\ ( dom f1)) by VFUNCT_1:def 2

      .= ( dom (f2 - f1)) by VFUNCT_1:def 2

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

      now

        

         A2: ( dom (f1 - f2)) = (( dom f2) /\ ( dom f1)) by VFUNCT_1:def 2

        .= ( dom (f2 - f1)) by VFUNCT_1:def 2;

        let x be Element of M such that

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

        

        thus ((f1 - f2) /. x) = ((f1 /. x) - (f2 /. x)) by A3, VFUNCT_1:def 2

        .= ( - ((f2 /. x) - (f1 /. x))) by RLVECT_1: 33

        .= (( - 1r ) * ((f2 /. x) - (f1 /. x))) by CLVECT_1: 3

        .= (( - 1r ) * ((f2 - f1) /. x)) by A3, A2, VFUNCT_1:def 2

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

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_2:17

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

    proof

      

       A1: ( dom (f1 - (f2 + f3))) = (( dom f1) /\ ( dom (f2 + f3))) by VFUNCT_1:def 2

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

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

      .= (( dom (f1 - f2)) /\ ( dom f3)) by VFUNCT_1:def 2

      .= ( dom ((f1 - f2) - f3)) by VFUNCT_1:def 2;

      now

        let x be Element of M;

        assume

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

        then x in (( dom f1) /\ ( dom (f2 + f3))) by VFUNCT_1:def 2;

        then

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

        x in (( dom (f1 - f2)) /\ ( dom f3)) by A1, A2, VFUNCT_1:def 2;

        then

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

        

        thus ((f1 - (f2 + f3)) /. x) = ((f1 /. x) - ((f2 + f3) /. x)) by A2, VFUNCT_1:def 2

        .= ((f1 /. x) - ((f2 /. x) + (f3 /. x))) by A3, VFUNCT_1:def 1

        .= (((f1 /. x) - (f2 /. x)) - (f3 /. x)) by RLVECT_1: 27

        .= (((f1 - f2) /. x) - (f3 /. x)) by A4, VFUNCT_1:def 2

        .= (((f1 - f2) - f3) /. x) by A1, A2, VFUNCT_1:def 2;

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_2:18

    

     Th18: ( 1r (#) f) = f

    proof

       A1:

      now

        let c be Element of M;

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

        

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

        .= (f /. c) by CLVECT_1:def 5;

      end;

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

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_2:19

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

    proof

      

       A1: ( dom (f1 - (f2 - f3))) = (( dom f1) /\ ( dom (f2 - f3))) by VFUNCT_1:def 2

      .= (( dom f1) /\ (( dom f2) /\ ( dom f3))) by VFUNCT_1:def 2

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

      .= (( dom (f1 - f2)) /\ ( dom f3)) by VFUNCT_1:def 2

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

      now

        let c be Element of M;

        assume

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

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

        then

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

        c in (( dom (f1 - f2)) /\ ( dom f3)) by A1, A2, VFUNCT_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, VFUNCT_1:def 2

        .= ((f1 /. c) - ((f2 /. c) - (f3 /. c))) by A3, VFUNCT_1:def 2

        .= (((f1 /. c) - (f2 /. c)) + (f3 /. c)) by RLVECT_1: 29

        .= (((f1 - f2) /. c) + (f3 /. c)) by A4, VFUNCT_1:def 2

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

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_2:20

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

    proof

      

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

      .= (( dom f1) /\ (( dom f2) /\ ( dom f3))) by VFUNCT_1:def 2

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

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

      .= ( dom ((f1 + f2) - f3)) by VFUNCT_1:def 2;

      now

        let c be Element of M;

        assume

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

        then c in (( dom f1) /\ ( dom (f2 - f3))) by VFUNCT_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, VFUNCT_1:def 2;

        then

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

        

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

        .= ((f1 /. c) + ((f2 /. c) - (f3 /. c))) by A3, VFUNCT_1:def 2

        .= (((f1 /. c) + (f2 /. c)) - (f3 /. c)) by RLVECT_1:def 3

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

        .= (((f1 + f2) - f3) /. c) by A1, A2, VFUNCT_1:def 2;

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_2:21

    for f1 be PartFunc of M, COMPLEX holds ||.(f1 (#) f2).|| = ( |.f1.| (#) ||.f2.||)

    proof

      let f1 be PartFunc of M, COMPLEX ;

      

       A1: ( dom (f1 (#) f2)) = (( dom f1) /\ ( dom f2)) by Def1;

      

       A2: (( dom f1) /\ ( dom f2)) = (( dom f1) /\ ( dom ||.f2.||)) by NORMSP_0:def 3

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

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

      

       A3: ( dom ||.(f1 (#) f2).||) = ( dom (f1 (#) f2)) by NORMSP_0:def 3;

      now

        let c be Element of M;

        assume

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

        then c in (( dom |.f1.|) /\ ( dom ||.f2.||)) by A3, A1, A2, VALUED_1:def 4;

        then

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

        

         A6: c in ( dom (f1 (#) f2)) by A4, NORMSP_0:def 3;

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

        then

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

        

        thus ( ||.(f1 (#) f2).|| . c) = ||.((f1 (#) f2) /. c).|| by A4, NORMSP_0:def 3

        .= ||.((f1 /. c) * (f2 /. c)).|| by A6, Def1

        .= ( |.(f1 /. c).| * ||.(f2 /. c).||) by CLVECT_1:def 13

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

        .= (( |.f1.| . c) * ( ||.f2.|| . c)) by A5, NORMSP_0:def 3

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

      end;

      hence thesis by A3, A1, A2, PARTFUN1: 5;

    end;

    theorem :: VFUNCT_2:22

     ||.(z (#) f).|| = ( |.z.| (#) ||.f.||)

    proof

      

       A1: ( dom ||.(z (#) f).||) = ( dom (z (#) f)) by NORMSP_0:def 3

      .= ( dom f) by Def2

      .= ( dom ||.f.||) by NORMSP_0:def 3

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

      now

        let c be Element of M;

        assume

         A2: c in ( dom ||.(z (#) f).||);

        then

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

        

         A4: c in ( dom (z (#) f)) by A2, NORMSP_0:def 3;

        

        thus ( ||.(z (#) f).|| . c) = ||.((z (#) f) /. c).|| by A2, NORMSP_0:def 3

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

        .= ( |.z.| * ||.(f /. c).||) by CLVECT_1:def 13

        .= ( |.z.| * ( ||.f.|| . c)) by A3, NORMSP_0:def 3

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

      end;

      hence thesis by A1, PARTFUN1: 5;

    end;

    theorem :: VFUNCT_2:23

    

     Th23: ( - f) = (( - 1r ) (#) f)

    proof

      

       A1: ( dom ( - f)) = ( dom f) by VFUNCT_1:def 5

      .= ( dom (( - 1r ) (#) f)) by Def2;

      now

        let c be Element of M;

        assume

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

        

        hence (( - f) /. c) = ( - (f /. c)) by A1, VFUNCT_1:def 5

        .= (( - 1r ) * (f /. c)) by CLVECT_1: 3

        .= ((( - 1r ) (#) f) /. c) by A2, Def2;

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_2:24

    

     Th24: ( - ( - f)) = f

    proof

      

      thus ( - ( - f)) = (( - 1r ) (#) ( - f)) by Th23

      .= (( - 1r ) (#) (( - 1r ) (#) f)) by Th23

      .= ((( - 1r ) * ( - 1r )) (#) f) by Th14

      .= f by Th18, COMPLEX1:def 4;

    end;

    theorem :: VFUNCT_2:25

    

     Th25: (f1 - f2) = (f1 + ( - f2))

    proof

      

       A1: ( dom (f1 - f2)) = (( dom f1) /\ ( dom f2)) by VFUNCT_1:def 2

      .= (( dom f1) /\ ( dom ( - f2))) by VFUNCT_1:def 5

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

      now

        let c be Element of M;

        assume

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

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

        then

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

        

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

        .= ((f1 /. c) - (f2 /. c)) by A3, VFUNCT_1:def 5

        .= ((f1 - f2) /. c) by A1, A2, VFUNCT_1:def 2;

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_2:26

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

    proof

      

      thus (f1 - ( - f2)) = (f1 + ( - ( - f2))) by Th25

      .= (f1 + f2) by Th24;

    end;

    reserve X,Y for set;

    theorem :: VFUNCT_2:27

    

     Th27: ((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 Element of M;

        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 VFUNCT_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 VFUNCT_1:def 1;

        

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

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

        .= (((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, VFUNCT_1:def 1;

      end;

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

      .= ((( dom f1) /\ ( dom f2)) /\ (X /\ X)) by VFUNCT_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 VFUNCT_1:def 1;

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

       A10:

      now

        let c be Element of M;

        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 VFUNCT_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 VFUNCT_1:def 1;

        

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

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

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

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

      end;

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

      .= ((( dom f1) /\ ( dom f2)) /\ X) by VFUNCT_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 VFUNCT_1:def 1;

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

       A18:

      now

        let c be Element of M;

        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 VFUNCT_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 VFUNCT_1:def 1;

        

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

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

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

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

      end;

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

      .= ((( dom f1) /\ ( dom f2)) /\ X) by VFUNCT_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 VFUNCT_1:def 1;

      hence thesis by A18, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_2:28

    for f1 be PartFunc of M, COMPLEX holds ((f1 (#) f2) | X) = ((f1 | X) (#) (f2 | X)) & ((f1 (#) f2) | X) = ((f1 | X) (#) f2) & ((f1 (#) f2) | X) = (f1 (#) (f2 | X))

    proof

      let f1 be PartFunc of M, COMPLEX ;

       A1:

      now

        let c be Element of M;

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

        then

         A7: c in ( dom f1) by 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

         A9: ((f1 | X) /. c) = ((f1 | X) . c) by PARTFUN1:def 6

        .= (f1 . c) by A8, FUNCT_1: 47

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

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

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

        then

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

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

        then

         A11: c in ( dom ((f1 | X) (#) (f2 | X))) by Def1;

        

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

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

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

        .= (((f1 | X) (#) (f2 | X)) /. c) by A11, Def1;

      end;

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

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

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

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

       A12:

      now

        let c be Element of M;

        assume

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

        then

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

        then

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

        then

         A16: c in (( dom f1) /\ ( dom f2)) by Def1;

        then

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

        c in X by A14, XBOOLE_0:def 4;

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

        then

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

        

        then

         A19: ((f1 | X) /. c) = ((f1 | X) . c) by PARTFUN1:def 6

        .= (f1 . c) by A18, FUNCT_1: 47;

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

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

        then

         A20: c in ( dom ((f1 | X) (#) f2)) by Def1;

        

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

        .= ((f1 /. c) * (f2 /. c)) by A15, Def1

        .= (((f1 | X) /. c) * (f2 /. c)) by A17, A19, PARTFUN1:def 6

        .= (((f1 | X) (#) f2) /. c) by A20, Def1;

      end;

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

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

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

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

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

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

       A21:

      now

        let c be Element of M;

        assume

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

        then

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

        then

         A24: c in X by XBOOLE_0:def 4;

        

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

        then

         A26: c in (( dom f1) /\ ( dom f2)) by Def1;

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

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

        then

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

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

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

        then

         A28: c in ( dom (f1 (#) (f2 | X))) by Def1;

        

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

        .= ((f1 /. c) * (f2 /. c)) by A25, Def1

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

        .= ((f1 (#) (f2 | X)) /. c) by A28, Def1;

      end;

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

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

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

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

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

      hence thesis by A21, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_2:29

    

     Th29: (( - f) | X) = ( - (f | X)) & ( ||.f.|| | X) = ||.(f | X).||

    proof

       A1:

      now

        let c be Element of M;

        assume

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

        then

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

        then

         A4: c in X by XBOOLE_0:def 4;

        

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

        then c in ( dom f) by VFUNCT_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 ( - (f | X))) by VFUNCT_1:def 5;

        

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

        .= ( - (f /. c)) by A5, VFUNCT_1:def 5

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

        .= (( - (f | X)) /. c) by A7, VFUNCT_1:def 5;

      end;

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

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

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

      .= ( dom ( - (f | X))) by VFUNCT_1:def 5;

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

      

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

      .= (( dom f) /\ X) by NORMSP_0:def 3

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

      .= ( dom ||.(f | X).||) by NORMSP_0:def 3;

      now

        let c be Element of M;

        assume

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

        then

         A10: c in ( dom (f | X)) by A8, NORMSP_0:def 3;

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

        then

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

        

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

        .= ||.(f /. c).|| by A11, NORMSP_0:def 3

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

        .= ( ||.(f | X).|| . c) by A8, A9, NORMSP_0:def 3;

      end;

      hence thesis by A8, PARTFUN1: 5;

    end;

    theorem :: VFUNCT_2:30

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

      .= ((f1 | X) + (( - f2) | X)) by Th27

      .= ((f1 | X) + ( - (f2 | X))) by Th29

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

      

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

      .= ((f1 | X) + ( - f2)) by Th27

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

      

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

      .= (f1 + (( - f2) | X)) by Th27

      .= (f1 + ( - (f2 | X))) by Th29

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

    end;

    theorem :: VFUNCT_2:31

    ((z (#) f) | X) = (z (#) (f | X))

    proof

       A1:

      now

        let c be Element of M;

        assume

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

        then

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

        then

         A4: c in X by XBOOLE_0:def 4;

        

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

        then c in ( dom f) by Def2;

        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 (z (#) (f | X))) by Def2;

        

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

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

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

        .= ((z (#) (f | X)) /. c) by A7, Def2;

      end;

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

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

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

      .= ( dom (z (#) (f | X))) by Def2;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_2:32

    

     Th32: (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) = M & ( dom f2) = M;

          

          hence ( dom (f1 + f2)) = (M /\ M) by VFUNCT_1:def 1

          .= M;

        end;

        assume (f1 + f2) is total;

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

        then (( dom f1) /\ ( dom f2)) = M by VFUNCT_1:def 1;

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

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

      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) = M & ( dom f2) = M;

          

          hence ( dom (f1 - f2)) = (M /\ M) by VFUNCT_1:def 2

          .= M;

        end;

        assume (f1 - f2) is total;

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

        then (( dom f1) /\ ( dom f2)) = M by VFUNCT_1:def 2;

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

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

      end;

    end;

    theorem :: VFUNCT_2:33

    

     Th33: for f1 be PartFunc of M, COMPLEX holds (f1 is total & f2 is total iff (f1 (#) f2) is total)

    proof

      let f1 be PartFunc of M, COMPLEX ;

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

      proof

        assume f1 is total & f2 is total;

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

        

        hence ( dom (f1 (#) f2)) = (M /\ M) by Def1

        .= M;

      end;

      assume (f1 (#) f2) is total;

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

      then (( dom f1) /\ ( dom f2)) = M by Def1;

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

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

    end;

    theorem :: VFUNCT_2:34

    

     Th34: f is total iff (z (#) f) is total by Def2;

    theorem :: VFUNCT_2:35

    

     Th35: f is total iff ( - f) is total

    proof

      thus f is total implies ( - f) is total

      proof

        assume

         A1: f is total;

        ( - f) = (( - 1r ) (#) f) by Th23;

        hence thesis by A1, Th34;

      end;

      assume

       A2: ( - f) is total;

      ( - f) = (( - 1r ) (#) f) by Th23;

      hence thesis by A2, Th34;

    end;

    theorem :: VFUNCT_2:36

    

     Th36: f is total iff ||.f.|| is total by NORMSP_0:def 3;

    theorem :: VFUNCT_2:37

    for x be Element of M st f1 is total & f2 is total holds ((f1 + f2) /. x) = ((f1 /. x) + (f2 /. x)) & ((f1 - f2) /. x) = ((f1 /. x) - (f2 /. x))

    proof

      let x be Element of M;

      assume

       A1: f1 is total & f2 is total;

      then (f1 + f2) is total by Th32;

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

      hence ((f1 + f2) /. x) = ((f1 /. x) + (f2 /. x)) by VFUNCT_1:def 1;

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

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

      hence thesis by VFUNCT_1:def 2;

    end;

    theorem :: VFUNCT_2:38

    for f1 be PartFunc of M, COMPLEX , x be Element of M holds f1 is total & f2 is total implies ((f1 (#) f2) /. x) = ((f1 /. x) * (f2 /. x))

    proof

      let f1 be PartFunc of M, COMPLEX ;

      let x be Element of M;

      assume f1 is total & f2 is total;

      then (f1 (#) f2) is total by Th33;

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

      hence thesis by Def1;

    end;

    theorem :: VFUNCT_2:39

    for x be Element of M st f is total holds ((z (#) f) /. x) = (z * (f /. x))

    proof

      let x be Element of M;

      assume f is total;

      then (z (#) f) is total by Th34;

      then ( dom (z (#) f)) = M;

      hence thesis by Def2;

    end;

    theorem :: VFUNCT_2:40

    for x be Element of M st f is total holds (( - f) /. x) = ( - (f /. x)) & ( ||.f.|| . x) = ||.(f /. x).||

    proof

      let x be Element of M;

      assume

       A1: f is total;

      then ( - f) is total by Th35;

      then ( dom ( - f)) = M;

      hence (( - f) /. x) = ( - (f /. x)) by VFUNCT_1:def 5;

       ||.f.|| is total by A1, Th36;

      then ( dom ||.f.||) = M;

      hence thesis by NORMSP_0:def 3;

    end;

    definition

      let M;

      let V;

      let f, Y;

      :: VFUNCT_2:def3

      pred f is_bounded_on Y means ex r be Real st for x be Element of M st x in (Y /\ ( dom f)) holds ||.(f /. x).|| <= r;

    end

    theorem :: VFUNCT_2:41

    Y c= X & f is_bounded_on X implies f is_bounded_on Y

    proof

      assume that

       A1: Y c= X and

       A2: f is_bounded_on X;

      consider r be Real such that

       A3: for x be Element of M st x in (X /\ ( dom f)) holds ||.(f /. x).|| <= r by A2;

      take r;

      let x be Element of M;

      assume x in (Y /\ ( dom f));

      then x in Y & x in ( dom f) by XBOOLE_0:def 4;

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

      hence thesis by A3;

    end;

    theorem :: VFUNCT_2:42

    X misses ( dom f) implies f is_bounded_on X

    proof

      assume (X /\ ( dom f)) = {} ;

      then for x be Element of M holds x in (X /\ ( dom f)) implies ||.(f /. x).|| <= 0 ;

      hence thesis;

    end;

    theorem :: VFUNCT_2:43

    ( 0c (#) f) is_bounded_on Y

    proof

      now

        take p = 0 ;

        let c be Element of M;

        ( |. 0c .| * ||.(f /. c).||) <= 0 by COMPLEX1: 44;

        then

         A1: ||.( 0c * (f /. c)).|| <= 0 by CLVECT_1:def 13;

        assume c in (Y /\ ( dom ( 0c (#) f)));

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

        hence ||.(( 0c (#) f) /. c).|| <= p by A1, Def2;

      end;

      hence thesis;

    end;

    theorem :: VFUNCT_2:44

    

     Th44: f is_bounded_on Y implies (z (#) f) is_bounded_on Y

    proof

      assume f is_bounded_on Y;

      then

      consider r1 be Real such that

       A1: for c be Element of M st c in (Y /\ ( dom f)) holds ||.(f /. c).|| <= r1;

      reconsider p = ( |.z.| * |.r1.|) as Real;

      take p;

      let c be Element of M;

      assume

       A2: c in (Y /\ ( dom (z (#) f)));

      then

       A3: c in Y by XBOOLE_0:def 4;

      

       A4: c in ( dom (z (#) f)) by A2, XBOOLE_0:def 4;

      then c in ( dom f) by Def2;

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

      then

       A5: ||.(f /. c).|| <= r1 by A1;

      r1 <= |.r1.| by ABSVALUE: 4;

      then |.z.| >= 0 & ||.(f /. c).|| <= |.r1.| by A5, COMPLEX1: 46, XXREAL_0: 2;

      then ( |.z.| * ||.(f /. c).||) <= ( |.z.| * |.r1.|) by XREAL_1: 64;

      then ||.(z * (f /. c)).|| <= p by CLVECT_1:def 13;

      hence thesis by A4, Def2;

    end;

    theorem :: VFUNCT_2:45

    

     Th45: f is_bounded_on Y implies ( ||.f.|| | Y) is bounded & ( - f) is_bounded_on Y

    proof

      assume

       A1: f is_bounded_on Y;

      then

      consider r1 be Real such that

       A2: for c be Element of M st c in (Y /\ ( dom f)) holds ||.(f /. c).|| <= r1;

      now

        let c be object;

        assume

         A3: c in (Y /\ ( dom ||.f.||));

        then

         A4: c in Y by XBOOLE_0:def 4;

        

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

        then c in ( dom f) by NORMSP_0:def 3;

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

        then ||.(f /. c).|| >= 0 & ||.(f /. c).|| <= r1 by A2, CLVECT_1: 105;

        then |. ||.(f /. c).||.| <= r1 by ABSVALUE:def 1;

        hence |.( ||.f.|| . c).| <= r1 by A5, NORMSP_0:def 3;

      end;

      hence ( ||.f.|| | Y) is bounded by RFUNCT_1: 73;

      (( - 1r ) (#) f) is_bounded_on Y by A1, Th44;

      hence thesis by Th23;

    end;

    theorem :: VFUNCT_2:46

    

     Th46: f1 is_bounded_on X & f2 is_bounded_on Y implies (f1 + f2) is_bounded_on (X /\ Y)

    proof

      assume that

       A1: f1 is_bounded_on X and

       A2: f2 is_bounded_on Y;

      consider r1 be Real such that

       A3: for c be Element of M st c in (X /\ ( dom f1)) holds ||.(f1 /. c).|| <= r1 by A1;

      consider r2 be Real such that

       A4: for c be Element of M st c in (Y /\ ( dom f2)) holds ||.(f2 /. c).|| <= r2 by A2;

      take r = (r1 + r2);

      let c be Element of M;

      assume

       A5: c in ((X /\ Y) /\ ( dom (f1 + f2)));

      then

       A6: c in (X /\ Y) by XBOOLE_0:def 4;

      then

       A7: c in Y 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 VFUNCT_1:def 1;

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

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

      then

       A10: ||.(f2 /. c).|| <= r2 by A4;

      

       A11: c in X by A6, XBOOLE_0:def 4;

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

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

      then ||.(f1 /. c).|| <= r1 by A3;

      then ||.((f1 /. c) + (f2 /. c)).|| <= ( ||.(f1 /. c).|| + ||.(f2 /. c).||) & ( ||.(f1 /. c).|| + ||.(f2 /. c).||) <= r by A10, CLVECT_1:def 13, XREAL_1: 7;

      then ||.((f1 /. c) + (f2 /. c)).|| <= r by XXREAL_0: 2;

      hence thesis by A8, VFUNCT_1:def 1;

    end;

    theorem :: VFUNCT_2:47

    for f1 be PartFunc of M, COMPLEX holds (f1 | X) is bounded & f2 is_bounded_on Y implies (f1 (#) f2) is_bounded_on (X /\ Y)

    proof

      let f1 be PartFunc of M, COMPLEX ;

      assume that

       A1: (f1 | X) is bounded and

       A2: f2 is_bounded_on Y;

      consider r1 be Real such that

       A3: for c be Element of M st c in (X /\ ( dom f1)) holds |.(f1 /. c).| <= r1 by A1, CFUNCT_1: 69;

      consider r2 be Real such that

       A4: for c be Element of M st c in (Y /\ ( dom f2)) holds ||.(f2 /. c).|| <= r2 by A2;

      reconsider r1 as Real;

      now

        take r = (r1 * r2);

        let c be Element of M;

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

        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 CLVECT_1: 105, COMPLEX1: 46;

        then ( |.(f1 /. c).| * ||.(f2 /. c).||) <= r by A10, A12, XREAL_1: 66;

        then ||.((f1 /. c) * (f2 /. c)).|| <= r by CLVECT_1:def 13;

        hence ||.((f1 (#) f2) /. c).|| <= r by A8, Def1;

      end;

      hence thesis;

    end;

    theorem :: VFUNCT_2:48

    f1 is_bounded_on X & f2 is_bounded_on Y implies (f1 - f2) is_bounded_on (X /\ Y)

    proof

      assume that

       A1: f1 is_bounded_on X and

       A2: f2 is_bounded_on Y;

      ( - f2) is_bounded_on Y by A2, Th45;

      then (f1 + ( - f2)) is_bounded_on (X /\ Y) by A1, Th46;

      hence thesis by Th25;

    end;

    theorem :: VFUNCT_2:49

    f is_bounded_on X & f is_bounded_on Y implies f is_bounded_on (X \/ Y)

    proof

      assume that

       A1: f is_bounded_on X and

       A2: f is_bounded_on Y;

      consider r1 be Real such that

       A3: for c be Element of M st c in (X /\ ( dom f)) holds ||.(f /. c).|| <= r1 by A1;

      consider r2 be Real such that

       A4: for c be Element of M st c in (Y /\ ( dom f)) holds ||.(f /. c).|| <= r2 by A2;

      reconsider r = ( |.r1.| + |.r2.|) as Real;

      take r;

      let c be Element of M;

      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 ) <= r by A9, XREAL_1: 7;

          hence thesis;

        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 + ||.(f /. c).||) <= r by A11, XREAL_1: 7;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: VFUNCT_2:50

    (f1 | X) is constant & (f2 | Y) is constant implies ((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 VECTOR of V such that

       A3: for c be Element of M st c in (X /\ ( dom f1)) holds (f1 /. c) = r1 by A1, PARTFUN2: 35;

      consider r2 be VECTOR of V such that

       A4: for c be Element of M st c in (Y /\ ( dom f2)) holds (f2 /. c) = r2 by A2, PARTFUN2: 35;

      now

        let c be Element of M;

        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 VFUNCT_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, VFUNCT_1:def 1

        .= (r1 + (f2 /. c)) by A3, A10

        .= (r1 + r2) by A4, A12;

      end;

      hence ((f1 + f2) | (X /\ Y)) is constant by PARTFUN2: 35;

      now

        let c be Element of M;

        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 VFUNCT_1:def 2;

        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, VFUNCT_1:def 2

        .= (r1 - (f2 /. c)) by A3, A18

        .= (r1 - r2) by A4, A20;

      end;

      hence thesis by PARTFUN2: 35;

    end;

    theorem :: VFUNCT_2:51

    for f1 be PartFunc of M, COMPLEX holds (f1 | X) is constant & (f2 | Y) is constant implies ((f1 (#) f2) | (X /\ Y)) is constant

    proof

      let f1 be PartFunc of M, COMPLEX ;

      assume that

       A1: (f1 | X) is constant and

       A2: (f2 | Y) is constant;

      consider z1 be Element of COMPLEX such that

       A3: for c be Element of M st c in (X /\ ( dom f1)) holds (f1 . c) = z1 by A1, PARTFUN2: 57;

      consider r2 be VECTOR of V such that

       A4: for c be Element of M st c in (Y /\ ( dom f2)) holds (f2 /. c) = r2 by A2, PARTFUN2: 35;

      now

        let c be Element of M;

        assume

         A5: c in ((X /\ Y) /\ ( dom (f1 (#) f2)));

        then

         A6: c in (X /\ Y) by XBOOLE_0:def 4;

        then

         A7: c in Y 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 Def1;

        then

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

        then

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

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

        then

         A12: c in (Y /\ ( dom f2)) by A7, XBOOLE_0:def 4;

        c in X by A6, XBOOLE_0:def 4;

        then

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

        

        thus ((f1 (#) f2) /. c) = ((f1 /. c) * (f2 /. c)) by A8, Def1

        .= (z1 * (f2 /. c)) by A3, A13, A11

        .= (z1 * r2) by A4, A12;

      end;

      hence thesis by PARTFUN2: 35;

    end;

    theorem :: VFUNCT_2:52

    

     Th52: (f | Y) is constant implies ((z (#) f) | Y) is constant

    proof

      assume (f | Y) is constant;

      then

      consider r be VECTOR of V such that

       A1: for c be Element of M st c in (Y /\ ( dom f)) holds (f /. c) = r by PARTFUN2: 35;

      now

        let c be Element of M;

        assume

         A2: c in (Y /\ ( dom (z (#) f)));

        then

         A3: c in Y by XBOOLE_0:def 4;

        

         A4: c in ( dom (z (#) f)) by A2, XBOOLE_0:def 4;

        then c in ( dom f) by Def2;

        then

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

        

        thus ((z (#) f) /. c) = (z * (f /. c)) by A4, Def2

        .= (z * r) by A1, A5;

      end;

      hence thesis by PARTFUN2: 35;

    end;

    theorem :: VFUNCT_2:53

    

     Th53: (f | Y) is constant implies ( ||.f.|| | Y) is constant & (( - f) | Y) is constant

    proof

      assume (f | Y) is constant;

      then

      consider r be VECTOR of V such that

       A1: for c be Element of M st c in (Y /\ ( dom f)) holds (f /. c) = r by PARTFUN2: 35;

      

       A2: ||.r.|| in REAL by XREAL_0:def 1;

      now

        let c be Element of M;

        assume

         A3: c in (Y /\ ( dom ||.f.||));

        then

         A4: c in Y by XBOOLE_0:def 4;

        

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

        then c in ( dom f) by NORMSP_0:def 3;

        then

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

        

        thus ( ||.f.|| . c) = ||.(f /. c).|| by A5, NORMSP_0:def 3

        .= ||.r.|| by A1, A6;

      end;

      hence ( ||.f.|| | Y) is constant by PARTFUN2: 57, A2;

      now

        take p = ( - r);

        let c be Element of M;

        assume

         A7: c in (Y /\ ( dom ( - f)));

        then c in (Y /\ ( dom f)) by VFUNCT_1:def 5;

        then

         A8: ( - (f /. c)) = p by A1;

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

        hence (( - f) /. c) = p by A8, VFUNCT_1:def 5;

      end;

      hence thesis by PARTFUN2: 35;

    end;

    theorem :: VFUNCT_2:54

    

     Th54: (f | Y) is constant implies f is_bounded_on Y

    proof

      assume (f | Y) is constant;

      then

      consider r be VECTOR of V such that

       A1: for c be Element of M st c in (Y /\ ( dom f)) holds (f /. c) = r by PARTFUN2: 35;

      now

        reconsider p = ||.r.|| as Real;

        take p;

        let c be Element of M;

        assume c in (Y /\ ( dom f));

        hence ||.(f /. c).|| <= p by A1;

      end;

      hence thesis;

    end;

    theorem :: VFUNCT_2:55

    (f | Y) is constant implies (for z holds (z (#) f) is_bounded_on Y) & ( - f) is_bounded_on Y & ( ||.f.|| | Y) is bounded

    proof

      assume

       A1: (f | Y) is constant;

      hereby

        let z;

        ((z (#) f) | Y) is constant by A1, Th52;

        hence (z (#) f) is_bounded_on Y by Th54;

      end;

      (( - f) | Y) is constant by A1, Th53;

      hence ( - f) is_bounded_on Y by Th54;

      ( ||.f.|| | Y) is constant by A1, Th53;

      hence thesis;

    end;

    theorem :: VFUNCT_2:56

    f1 is_bounded_on X & (f2 | Y) is constant implies (f1 + f2) is_bounded_on (X /\ Y)

    proof

      assume that

       A1: f1 is_bounded_on X and

       A2: (f2 | Y) is constant;

      f2 is_bounded_on Y by A2, Th54;

      hence thesis by A1, Th46;

    end;

    theorem :: VFUNCT_2:57

    f1 is_bounded_on X & (f2 | Y) is constant implies (f1 - f2) is_bounded_on (X /\ Y) & (f2 - f1) is_bounded_on (X /\ Y)

    proof

      assume that

       A1: f1 is_bounded_on X and

       A2: (f2 | Y) is constant;

      

       A3: f2 is_bounded_on Y by A2, Th54;

      then ( - f2) is_bounded_on Y by Th45;

      then

       A4: (f1 + ( - f2)) is_bounded_on (X /\ Y) by A1, Th46;

      ( - f1) is_bounded_on X by A1, Th45;

      then (f2 + ( - f1)) is_bounded_on (Y /\ X) by A3, Th46;

      hence thesis by A4, Th25;

    end;