vfunct_1.miz



    begin

    reserve x,X,Y for set;

    reserve C for non empty set;

    reserve c for Element of C;

    reserve V for RealNormSpace;

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

    reserve r,r1,r2,p for Real;

    definition

      let C;

      let V be non empty addLoopStr;

      let f1,f2 be PartFunc of C, V;

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

      deffunc G( set) = ((f1 /. $1) - (f2 /. $1));

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

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

      :: VFUNCT_1:def1

      func f1 + f2 -> PartFunc of C, V means

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

      existence

      proof

        consider F be PartFunc of C, V 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 thesis by A1, A2, SUBSET_1: 3;

      end;

      uniqueness

      proof

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

      end;

      :: VFUNCT_1:def2

      func f1 - f2 -> PartFunc of C, V means

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

      existence

      proof

        consider F be PartFunc of C, V such that

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

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

        take F;

        thus thesis by A3, A4, SUBSET_1: 3;

      end;

      uniqueness

      proof

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

      end;

    end

    registration

      let C;

      let V be non empty addLoopStr;

      let f1,f2 be Function of C, V;

      cluster (f1 + f2) -> total;

      coherence

      proof

        

        thus ( dom (f1 + f2)) = (( dom f1) /\ ( dom f2)) by Def1

        .= (C /\ ( dom f2)) by FUNCT_2:def 1

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

        .= C;

      end;

      cluster (f1 - f2) -> total;

      coherence

      proof

        

        thus ( dom (f1 - f2)) = (( dom f1) /\ ( dom f2)) by Def2

        .= (C /\ ( dom f2)) by FUNCT_2:def 1

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

        .= C;

      end;

    end

    definition

      let C;

      let V be non empty RLSStruct;

      let f1 be PartFunc of C, REAL ;

      let f2 be PartFunc of C, V;

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

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

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

      :: VFUNCT_1:def3

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

      : Def3: ( dom it ) = (( dom f1) /\ ( dom f2)) & for c st c in ( dom it ) holds (it /. c) = ((f1 . c) * (f2 /. c));

      existence

      proof

        consider F be PartFunc of C, V 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 thesis by A1, A2, SUBSET_1: 3;

      end;

      uniqueness

      proof

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

      end;

    end

    registration

      let C;

      let V be non empty RLSStruct;

      let f1 be Function of C, REAL ;

      let f2 be Function of C, V;

      cluster (f1 (#) f2) -> total;

      coherence

      proof

        

        thus ( dom (f1 (#) f2)) = (( dom f1) /\ ( dom f2)) by Def3

        .= (C /\ ( dom f2)) by FUNCT_2:def 1

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

        .= C;

      end;

    end

    definition

      let C;

      let V be non empty RLSStruct;

      let f be PartFunc of C, V;

      let r be Real;

      deffunc F( Element of C) = (r * (f /. $1));

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

      :: VFUNCT_1:def4

      func r (#) f -> PartFunc of C, V means

      : Def4: ( dom it ) = ( dom f) & for c st c in ( dom it ) holds (it /. c) = (r * (f /. c));

      existence

      proof

        consider F be PartFunc of C, V 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 thesis by A1, A2, SUBSET_1: 3;

      end;

      uniqueness

      proof

        set X = ( dom f);

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

      end;

    end

    registration

      let C;

      let V be non empty RLSStruct;

      let f be Function of C, V;

      let r;

      cluster (r (#) f) -> total;

      coherence

      proof

        

        thus ( dom (r (#) f)) = ( dom f) by Def4

        .= C by FUNCT_2:def 1;

      end;

    end

    definition

      let C;

      let V be non empty addLoopStr;

      let f be PartFunc of C, V;

      deffunc G( Element of C) = ( - (f /. $1));

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

      :: VFUNCT_1:def5

      func - f -> PartFunc of C, V means

      : Def5: ( dom it ) = ( dom f) & for c st c in ( dom it ) holds (it /. c) = ( - (f /. c));

      existence

      proof

        consider F be PartFunc of C, V 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) = G(c) from PARTFUN2:sch 2;

        take F;

        thus thesis by A1, A2, SUBSET_1: 3;

      end;

      uniqueness

      proof

        set X = ( dom f);

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

      end;

    end

    registration

      let C;

      let V be non empty addLoopStr;

      let f be Function of C, V;

      cluster ( - f) -> total;

      coherence

      proof

        

        thus ( dom ( - f)) = ( dom f) by Def5

        .= C by FUNCT_2:def 1;

      end;

    end

    theorem :: VFUNCT_1:1

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

    proof

      let f1 be PartFunc of C, REAL ;

      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

         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) " {( 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

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

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

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

        then

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

        

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

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

        then

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

        (f1 . x1) <> 0 by A3, RLVECT_1: 10;

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

        then

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

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

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

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

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

        then

        reconsider x1 = x as Element of C;

        

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

        then

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

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

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

        then

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

        

         A12: x in (( dom f1) \ (f1 " { 0 })) 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 Def3;

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

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

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

        then ((f1 . x1) * (f2 /. x1)) <> ( 0. V) by A11, RLVECT_1: 11;

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

        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 A14, XBOOLE_0:def 5;

      end;

    end;

    theorem :: VFUNCT_1:2

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

    proof

      now

        let c;

        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 ;

        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;

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

          then (f /. c) = ( 0. V);

          then

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

          c in ( dom f) by A7, Def5;

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

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

        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_1:3

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

    proof

      assume

       A1: r <> 0 ;

      now

        let c;

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

        proof

          assume

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

          then

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

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

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

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

          then (f /. c) = ( 0. V) by A1, RLVECT_1: 36;

          then

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

          c in ( dom f) by A3, Def4;

          hence thesis by A4, PARTFUN2: 26;

        end;

        assume

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

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

        then

         A6: c in ( dom (r (#) f)) by Def4;

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

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

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

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

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

      end;

      hence thesis by SUBSET_1: 3;

    end;

    theorem :: VFUNCT_1:4

    

     Th4: for V be Abelian non empty addLoopStr holds for f1,f2 be PartFunc of C, V holds (f1 + f2) = (f2 + f1)

    proof

      let V be Abelian non empty addLoopStr;

      let f1,f2 be PartFunc of C, V;

      

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

      .= ( dom (f2 + f1)) by Def1;

      now

        let c;

        assume

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

        

        hence ((f1 + f2) /. c) = ((f2 /. c) + (f1 /. c)) by Def1

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

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    definition

      let C;

      let V be Abelian non empty addLoopStr;

      let f1,f2 be PartFunc of C, V;

      :: original: +

      redefine

      func f1 + f2;

      commutativity by Th4;

    end

    theorem :: VFUNCT_1:5

    for V be add-associative non empty addLoopStr holds for f1,f2,f3 be PartFunc of C, V holds ((f1 + f2) + f3) = (f1 + (f2 + f3))

    proof

      let V be add-associative non empty addLoopStr;

      let f1,f2,f3 be PartFunc of C, V;

      

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

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

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

        assume

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

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

        then

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

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

        then

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

        

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

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

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

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

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

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_1:6

    for V be scalar-associative non empty RLSStruct holds for f1,f2 be PartFunc of C, REAL , f3 be PartFunc of C, V holds ((f1 (#) f2) (#) f3) = (f1 (#) (f2 (#) f3))

    proof

      let V be scalar-associative non empty RLSStruct;

      let f1,f2 be PartFunc of C, REAL ;

      let f3 be PartFunc of C, V;

      

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

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

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

      now

        let c;

        assume

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

        then c in (( dom f1) /\ ( dom (f2 (#) f3))) by A1, Def3;

        then

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

        

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

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

        .= ((f1 . c) * ((f2 . c) * (f3 /. c))) by RLVECT_1:def 7

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

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

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_1:7

    for V be scalar-distributive non empty RLSStruct holds for f1,f2 be PartFunc of C, REAL holds for f3 be Function of C, V holds ((f1 + f2) (#) f3) = ((f1 (#) f3) + (f2 (#) f3))

    proof

      let V be scalar-distributive non empty RLSStruct;

      let f1,f2 be PartFunc of C, REAL ;

      let f3 be Function of C, V;

      

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

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

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

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

      now

        let c;

        assume

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

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

        then

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

        

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

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

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

        .= (((f1 . c) * (f3 /. c)) + ((f2 . c) * (f3 /. c))) by RLVECT_1:def 6

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

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

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

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_1:8

    for V be vector-distributive non empty RLSStruct holds for f1,f2 be PartFunc of C, V holds for f3 be Function of C, REAL holds (f3 (#) (f1 + f2)) = ((f3 (#) f1) + (f3 (#) f2))

    proof

      let V be vector-distributive non empty RLSStruct;

      let f1,f2 be PartFunc of C, V;

      let f3 be Function of C, REAL ;

      

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

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

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

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

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

      now

        let c;

        assume

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

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

        then

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

        

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

        then

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

        

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

        

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

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

        .= (((f3 . c) * (f1 /. c)) + ((f3 . c) * (f2 /. c))) by RLVECT_1:def 5

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

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

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

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_1:9

    for V be scalar-associative non empty RLSStruct holds for f1 be PartFunc of C, REAL holds for f2 be PartFunc of C, V holds (r (#) (f1 (#) f2)) = ((r (#) f1) (#) f2)

    proof

      let V be scalar-associative non empty RLSStruct;

      let f1 be PartFunc of C, REAL ;

      let f2 be PartFunc of C, V;

      

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

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

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

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

      now

        let c;

        assume

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

        then

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

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

        then

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

        

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

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

        .= ((r * (f1 . c)) * (f2 /. c)) by RLVECT_1:def 7

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

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

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_1:10

    for V be scalar-associative non empty RLSStruct holds for f1 be PartFunc of C, REAL holds for f2 be PartFunc of C, V holds (r (#) (f1 (#) f2)) = (f1 (#) (r (#) f2))

    proof

      let V be scalar-associative non empty RLSStruct;

      let f1 be PartFunc of C, REAL ;

      let f2 be PartFunc of C, V;

      

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

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

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

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

      now

        let c;

        assume

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

        then

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

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

        then

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

        

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

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

        .= (((f1 . c) * r) * (f2 /. c)) by RLVECT_1:def 7

        .= ((f1 . c) * (r * (f2 /. c))) by RLVECT_1:def 7

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

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

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_1:11

    for V be add-associative right_zeroed right_complementable Abelian scalar-distributive scalar-associative scalar-unital vector-distributive non empty RLSStruct holds for f1,f2 be PartFunc of C, REAL holds for f3 be Function of C, V holds ((f1 - f2) (#) f3) = ((f1 (#) f3) - (f2 (#) f3))

    proof

      let V be add-associative right_zeroed right_complementable Abelian scalar-distributive scalar-associative scalar-unital vector-distributive non empty RLSStruct;

      let f1,f2 be PartFunc of C, REAL ;

      let f3 be Function of C, V;

      

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

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

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

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

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

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

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

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

      now

        let c;

        assume

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

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

        then

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

        

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

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

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

        .= (((f1 . c) * (f3 /. c)) - ((f2 . c) * (f3 /. c))) by RLVECT_1: 35

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

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

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

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_1:12

    for V be add-associative right_zeroed right_complementable Abelian scalar-distributive scalar-associative scalar-unital vector-distributive non empty RLSStruct holds for f1,f2 be PartFunc of C, V holds for f3 be PartFunc of C, REAL holds ((f3 (#) f1) - (f3 (#) f2)) = (f3 (#) (f1 - f2))

    proof

      let V be add-associative right_zeroed right_complementable Abelian scalar-distributive scalar-associative scalar-unital vector-distributive non empty RLSStruct;

      let f1,f2 be PartFunc of C, V;

      let f3 be PartFunc of C, REAL ;

      

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

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

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

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

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

      now

        let c;

        assume

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

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

        then

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

        

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

        then

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

        

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

        

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

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

        .= (((f3 . c) * (f1 /. c)) - ((f3 . c) * (f2 /. c))) by RLVECT_1: 34

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

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

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

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_1:13

    for V be vector-distributive non empty RLSStruct holds for f1,f2 be PartFunc of C, V holds (r (#) (f1 + f2)) = ((r (#) f1) + (r (#) f2))

    proof

      let V be vector-distributive non empty RLSStruct;

      let f1,f2 be PartFunc of C, V;

      

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

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

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

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

      .= ( dom ((r (#) f1) + (r (#) f2))) by Def1;

      now

        let c;

        assume

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

        then

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

        

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

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

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

        .= ((r * (f1 /. c)) + (r * (f2 /. c))) by RLVECT_1:def 5

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

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

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

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_1:14

    for V be scalar-associative non empty RLSStruct holds for f be PartFunc of C, V holds ((r * p) (#) f) = (r (#) (p (#) f))

    proof

      let V be scalar-associative non empty RLSStruct;

      let f be PartFunc of C, V;

      

       A1: ( dom ((r * p) (#) f)) = ( dom f) by Def4

      .= ( dom (p (#) f)) by Def4

      .= ( dom (r (#) (p (#) f))) by Def4;

      now

        let c;

        assume

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

        then

         A3: c in ( dom (p (#) f)) by A1, Def4;

        

        thus (((r * p) (#) f) /. c) = ((r * p) * (f /. c)) by A2, Def4

        .= (r * (p * (f /. c))) by RLVECT_1:def 7

        .= (r * ((p (#) f) /. c)) by A3, Def4

        .= ((r (#) (p (#) f)) /. c) by A1, A2, Def4;

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_1:15

    for V be add-associative right_zeroed right_complementable Abelian scalar-distributive scalar-associative scalar-unital vector-distributive non empty RLSStruct holds for f1,f2 be PartFunc of C, V holds (r (#) (f1 - f2)) = ((r (#) f1) - (r (#) f2))

    proof

      let V be add-associative right_zeroed right_complementable Abelian scalar-distributive scalar-associative scalar-unital vector-distributive non empty RLSStruct;

      let f1,f2 be PartFunc of C, V;

      

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

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

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

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

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

      now

        let c;

        assume

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

        then

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

        

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

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

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

        .= ((r * (f1 /. c)) - (r * (f2 /. c))) by RLVECT_1: 34

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

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

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

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_1:16

    for V be add-associative right_zeroed right_complementable Abelian scalar-distributive scalar-unital vector-distributive non empty RLSStruct holds for f1,f2 be PartFunc of C, V holds (f1 - f2) = (( - 1) (#) (f2 - f1))

    proof

      let V be add-associative right_zeroed right_complementable Abelian scalar-distributive scalar-unital vector-distributive non empty RLSStruct;

      let f1,f2 be PartFunc of C, V;

      

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

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

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

      now

        

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

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

        let c such that

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

        

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

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

        .= (( - 1) * ((f2 /. c) - (f1 /. c))) by RLVECT_1: 16

        .= (( - 1) * ((f2 - f1) /. c)) by A3, A2, Def2

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

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_1:17

    for V be add-associative right_zeroed right_complementable Abelian non empty addLoopStr holds for f1,f2,f3 be PartFunc of C, V holds (f1 - (f2 + f3)) = ((f1 - f2) - f3)

    proof

      let V be add-associative right_zeroed right_complementable Abelian non empty addLoopStr;

      let f1,f2,f3 be PartFunc of C, V;

      

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

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

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

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

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

      now

        let c;

        assume

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

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

        then

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

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

        then

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

        

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

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

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

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

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

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_1:18

    for V be scalar-unital non empty RLSStruct holds for f be PartFunc of C, V holds (1 (#) f) = f

    proof

      let V be scalar-unital non empty RLSStruct;

      let f be PartFunc of C, V;

       A1:

      now

        let c;

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

        

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

        .= (f /. c) by RLVECT_1:def 8;

      end;

      ( dom (1 (#) f)) = ( dom f) by Def4;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_1:19

    for V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr holds for f1,f2,f3 be PartFunc of C, V holds (f1 - (f2 - f3)) = ((f1 - f2) + f3)

    proof

      let V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr;

      let f1,f2,f3 be PartFunc of C, V;

      

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

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

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

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

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

      now

        let c;

        assume

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

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

        then

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

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

        then

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

        

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

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

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

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

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

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_1:20

    for V be add-associative non empty addLoopStr holds for f1,f2,f3 be PartFunc of C, V holds (f1 + (f2 - f3)) = ((f1 + f2) - f3)

    proof

      let V be add-associative non empty addLoopStr;

      let f1,f2,f3 be PartFunc of C, V;

      

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

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

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

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

      .= ( dom ((f1 + f2) - f3)) by Def2;

      now

        let c;

        assume

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

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

        then

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

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

        then

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

        

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

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

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

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

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

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_1:21

    for V be RealNormSpace-like non empty NORMSTR holds for f1 be PartFunc of C, REAL holds for f2 be PartFunc of C, V holds ||.(f1 (#) f2).|| = (( abs f1) (#) ||.f2.||)

    proof

      let V be RealNormSpace-like non empty NORMSTR;

      let f1 be PartFunc of C, REAL ;

      let f2 be PartFunc of C, V;

      

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

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

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

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

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

      now

        let c;

        assume

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

        then

         A3: c in ( dom (f1 (#) f2)) by NORMSP_0:def 3;

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

        then

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

        

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

        .= ||.((f1 . c) * (f2 /. c)).|| by A3, Def3

        .= ( |.(f1 . c).| * ||.(f2 /. c).||) by NORMSP_1:def 1

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

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

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

      end;

      hence thesis by A1, PARTFUN1: 5;

    end;

    theorem :: VFUNCT_1:22

    for V be RealNormSpace-like non empty NORMSTR holds for f be PartFunc of C, V holds ||.(r (#) f).|| = ( |.r.| (#) ||.f.||)

    proof

      let V be RealNormSpace-like non empty NORMSTR;

      let f be PartFunc of C, V;

      

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

      .= ( dom f) by Def4

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

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

      now

        let c;

        assume

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

        then

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

        

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

        

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

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

        .= ( |.r.| * ||.(f /. c).||) by NORMSP_1:def 1

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

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

      end;

      hence thesis by A1, PARTFUN1: 5;

    end;

    theorem :: VFUNCT_1:23

    

     Th23: for V be add-associative right_zeroed right_complementable Abelian scalar-distributive scalar-unital vector-distributive non empty RLSStruct holds for f be PartFunc of C, V holds ( - f) = (( - 1) (#) f)

    proof

      let V be add-associative right_zeroed right_complementable Abelian scalar-distributive scalar-unital vector-distributive non empty RLSStruct;

      let f be PartFunc of C, V;

      

       A1: ( dom ( - f)) = ( dom f) by Def5

      .= ( dom (( - 1) (#) f)) by Def4;

      now

        let c;

        assume

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

        

        hence (( - f) /. c) = ( - (f /. c)) by A1, Def5

        .= (( - 1) * (f /. c)) by RLVECT_1: 16

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

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_1:24

    

     Th24: for V be add-associative right_zeroed right_complementable non empty addLoopStr holds for f be PartFunc of C, V holds ( - ( - f)) = f

    proof

      let V be add-associative right_zeroed right_complementable non empty addLoopStr;

      let f be PartFunc of C, V;

      

       A1: ( dom ( - ( - f))) = ( dom ( - f)) by Def5;

      

       A2: ( dom ( - f)) = ( dom f) by Def5;

      now

        let c;

        assume

         A3: c in ( dom f);

        

        hence (( - ( - f)) /. c) = ( - (( - f) /. c)) by A1, A2, Def5

        .= ( - ( - (f /. c))) by A2, A3, Def5

        .= (f /. c);

      end;

      hence thesis by A1, A2, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_1:25

    

     Th25: for V be non empty addLoopStr holds for f1,f2 be PartFunc of C, V holds (f1 - f2) = (f1 + ( - f2))

    proof

      let V be non empty addLoopStr;

      let f1,f2 be PartFunc of C, V;

      

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

      .= (( dom f1) /\ ( dom ( - f2))) by Def5

      .= ( dom (f1 + ( - f2))) by Def1;

      now

        let c;

        assume

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

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

        then

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

        

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

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

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

      end;

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_1:26

    for V be add-associative right_zeroed right_complementable Abelian scalar-distributive scalar-unital scalar-associative vector-distributive non empty RLSStruct holds for f1,f2 be PartFunc of C, V holds (f1 - ( - f2)) = (f1 + f2)

    proof

      let V be add-associative right_zeroed right_complementable Abelian scalar-distributive scalar-unital scalar-associative vector-distributive non empty RLSStruct;

      let f1,f2 be PartFunc of C, V;

      

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

      .= (f1 + f2) by Th24;

    end;

    theorem :: VFUNCT_1: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;

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

        

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

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

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

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

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

        

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

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

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

        .= (((f1 | X) + f2) /. c) by A17, 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 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 Def1;

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

        

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

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

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

        .= ((f1 + (f2 | X)) /. c) by A25, 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 A18, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_1:28

    for f1 be PartFunc of C, REAL 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 C, REAL ;

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

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

        

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

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

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

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

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

      end;

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

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

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

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

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

        

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

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

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

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

      end;

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

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

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

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

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

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

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

        

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

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

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

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

      end;

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

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

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

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

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

      hence thesis by A18, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_1:29

    

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

    proof

       A1:

      now

        let c;

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

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

        

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

        .= ( - (f /. c)) by A5, Def5

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

        .= (( - (f | X)) /. c) by A7, Def5;

      end;

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

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

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

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

      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;

        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_1: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_1:31

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

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

        

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

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

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

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

      end;

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

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

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

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

      hence thesis by A1, PARTFUN2: 1;

    end;

    theorem :: VFUNCT_1:32

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

    proof

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

      proof

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

        assume (f1 + f2) is total;

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

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

      end;

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

      proof

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

        assume (f1 - f2) is total;

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

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

      end;

    end;

    theorem :: VFUNCT_1:33

    for f1 be PartFunc of C, REAL holds (f1 is total & f2 is total iff (f1 (#) f2) is total)

    proof

      let f1 be PartFunc of C, REAL ;

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

      assume (f1 (#) f2) is total;

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

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

    end;

    theorem :: VFUNCT_1:34

    f is total iff (r (#) f) is total by Def4;

    theorem :: VFUNCT_1:35

    f is total iff ( - f) is total

    proof

      thus f is total implies ( - f) is total;

      assume

       A1: ( - f) is total;

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

      hence thesis by A1, Def4;

    end;

    theorem :: VFUNCT_1:36

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

    theorem :: VFUNCT_1:37

    f1 is total & f2 is total implies ((f1 + f2) /. c) = ((f1 /. c) + (f2 /. c)) & ((f1 - f2) /. c) = ((f1 /. c) - (f2 /. c))

    proof

      assume

       A1: f1 is total & f2 is total;

      then ( dom (f1 + f2)) = C by PARTFUN1:def 2;

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

      ( dom (f1 - f2)) = C by A1, PARTFUN1:def 2;

      hence thesis by Def2;

    end;

    theorem :: VFUNCT_1:38

    for f1 be PartFunc of C, REAL holds f1 is total & f2 is total implies ((f1 (#) f2) /. c) = ((f1 . c) * (f2 /. c))

    proof

      let f1 be PartFunc of C, REAL ;

      assume f1 is total & f2 is total;

      then ( dom (f1 (#) f2)) = C by PARTFUN1:def 2;

      hence thesis by Def3;

    end;

    theorem :: VFUNCT_1:39

    f is total implies ((r (#) f) /. c) = (r * (f /. c))

    proof

      assume f is total;

      then ( dom (r (#) f)) = C by PARTFUN1:def 2;

      hence thesis by Def4;

    end;

    theorem :: VFUNCT_1:40

    f is total implies (( - f) /. c) = ( - (f /. c)) & ( ||.f.|| . c) = ||.(f /. c).||

    proof

      assume

       A1: f is total;

      then ( dom ( - f)) = C by PARTFUN1:def 2;

      hence (( - f) /. c) = ( - (f /. c)) by Def5;

       ||.f.|| is total by A1, NORMSP_0:def 3;

      hence thesis by NORMSP_0:def 3;

    end;

    definition

      let C;

      let V be non empty NORMSTR;

      let f be PartFunc of C, V;

      let Y;

      :: VFUNCT_1:def6

      pred f is_bounded_on Y means ex r st for c st c in (Y /\ ( dom f)) holds ||.(f /. c).|| <= r;

    end

    theorem :: VFUNCT_1: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 such that

       A3: for c st c in (X /\ ( dom f)) holds ||.(f /. c).|| <= r by A2;

      take r;

      let c;

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

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

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

      hence thesis by A3;

    end;

    theorem :: VFUNCT_1:42

    X misses ( dom f) implies f is_bounded_on X

    proof

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

      then for c holds c in (X /\ ( dom f)) implies ||.(f /. c).|| <= 0 ;

      hence thesis;

    end;

    theorem :: VFUNCT_1:43

    ( 0 (#) f) is_bounded_on Y

    proof

      now

        take p = 0 ;

        let c;

        ( 0 * ||.(f /. c).||) = 0 ;

        then ( |. 0 .| * ||.(f /. c).||) <= 0 by ABSVALUE: 2;

        then

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

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

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

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

      end;

      hence thesis;

    end;

    theorem :: VFUNCT_1:44

    

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

    proof

      assume f is_bounded_on Y;

      then

      consider r1 such that

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

      take p = ( |.r.| * |.r1.|);

      let c;

      assume

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

      then

       A3: c in Y by XBOOLE_0:def 4;

      

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

      then c in ( dom f) by Def4;

      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 |.r.| >= 0 & ||.(f /. c).|| <= |.r1.| by A5, COMPLEX1: 46, XXREAL_0: 2;

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

      then ||.(r * (f /. c)).|| <= p by NORMSP_1:def 1;

      hence thesis by A4, Def4;

    end;

    theorem :: VFUNCT_1: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 such that

       A2: for c 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, NORMSP_1: 4;

        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;

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

      hence thesis by Th23;

    end;

    theorem :: VFUNCT_1: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 such that

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

      consider r2 such that

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

      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 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 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, NORMSP_1:def 1, XREAL_1: 7;

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

      hence thesis by A8, Def1;

    end;

    theorem :: VFUNCT_1:47

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

    proof

      let f1 be PartFunc of C, REAL ;

      assume that

       A1: (f1 | X) is bounded and

       A2: f2 is_bounded_on Y;

      consider r1 be Real such that

       A3: for c be object st c in (X /\ ( dom f1)) holds |.(f1 . c).| <= r1 by A1, RFUNCT_1: 73;

      consider r2 such that

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

      reconsider r1 as Real;

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

        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, NORMSP_1: 4;

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

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

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

      end;

      hence thesis;

    end;

    theorem :: VFUNCT_1: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_1: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 such that

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

      consider r2 such that

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

      take r = ( |.r1.| + |.r2.|);

      let c;

      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_1: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 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 st c in (Y /\ ( dom f2)) holds (f2 /. c) = r2 by A2, PARTFUN2: 35;

      now

        let c;

        assume

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

        then

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

        then

         A7: c in X by XBOOLE_0:def 4;

        

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

        then

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

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

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

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

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

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

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

      end;

      hence thesis by PARTFUN2: 35;

    end;

    theorem :: VFUNCT_1:51

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

    proof

      let f1 be PartFunc of C, REAL ;

      assume that

       A1: (f1 | X) is constant and

       A2: (f2 | Y) is constant;

      consider r1 be Element of REAL such that

       A3: for c st c in (X /\ ( dom f1)) holds (f1 . c) = r1 by A1, PARTFUN2: 57;

      consider r2 be VECTOR of V such that

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

      now

        let c;

        assume

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

        then

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

        then

         A7: c in X by XBOOLE_0:def 4;

        

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

        then

         A9: c in (( dom f1) /\ ( dom f2)) by Def3;

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

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

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

      end;

      hence thesis by PARTFUN2: 35;

    end;

    theorem :: VFUNCT_1:52

    

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

    proof

      assume (f | Y) is constant;

      then

      consider r be VECTOR of V such that

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

      now

        let c;

        assume

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

        then

         A3: c in Y by XBOOLE_0:def 4;

        

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

        then c in ( dom f) by Def4;

        then

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

        

        thus ((p (#) f) /. c) = (p * (f /. c)) by A4, Def4

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

      end;

      hence thesis by PARTFUN2: 35;

    end;

    theorem :: VFUNCT_1: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 st c in (Y /\ ( dom f)) holds (f /. c) = r by PARTFUN2: 35;

      now

        let c;

        assume

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

        then

         A3: c in Y by XBOOLE_0:def 4;

        

         A4: c in ( dom ||.f.||) by A2, XBOOLE_0:def 4;

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

        then

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

        

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

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

      end;

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

      now

        take p = ( - r);

        let c;

        assume

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

        then c in (Y /\ ( dom f)) by Def5;

        then

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

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

        hence (( - f) /. c) = p by A7, Def5;

      end;

      hence thesis by PARTFUN2: 35;

    end;

    theorem :: VFUNCT_1: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 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;

    end;

    theorem :: VFUNCT_1:55

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

    proof

      assume

       A1: (f | Y) is constant;

      hereby

        let r;

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

        hence (r (#) 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_1: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_1: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;