:: by Hiroshi Yamazaki and Yasunari Shidama

::

:: Received October 27, 1992

:: Copyright (c) 1992-2018 Association of Mizar Users

definition

let C be non empty set ;

let V be non empty addLoopStr ;

let f1, f2 be PartFunc of C,V;

deffunc H_{1}( set ) -> Element of the U1 of V = (f1 /. $1) + (f2 /. $1);

deffunc H_{2}( set ) -> Element of the U1 of V = (f1 /. $1) - (f2 /. $1);

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

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

ex b_{1} being PartFunc of C,V st

( dom b_{1} = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b_{1} holds

b_{1} /. c = (f1 /. c) + (f2 /. c) ) )

for b_{1}, b_{2} being PartFunc of C,V st dom b_{1} = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b_{1} holds

b_{1} /. c = (f1 /. c) + (f2 /. c) ) & dom b_{2} = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b_{2} holds

b_{2} /. c = (f1 /. c) + (f2 /. c) ) holds

b_{1} = b_{2}

ex b_{1} being PartFunc of C,V st

( dom b_{1} = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b_{1} holds

b_{1} /. c = (f1 /. c) - (f2 /. c) ) )

for b_{1}, b_{2} being PartFunc of C,V st dom b_{1} = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b_{1} holds

b_{1} /. c = (f1 /. c) - (f2 /. c) ) & dom b_{2} = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b_{2} holds

b_{2} /. c = (f1 /. c) - (f2 /. c) ) holds

b_{1} = b_{2}

end;
let V be non empty addLoopStr ;

let f1, f2 be PartFunc of C,V;

deffunc H

deffunc H

defpred S

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

func f1 + f2 -> PartFunc of C,V means :Def1: :: VFUNCT_1:def 1

( dom it = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom it holds

it /. c = (f1 /. c) + (f2 /. c) ) );

existence ( dom it = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom it holds

it /. c = (f1 /. c) + (f2 /. c) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

func f1 - f2 -> PartFunc of C,V means :Def2: :: VFUNCT_1:def 2

( dom it = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom it holds

it /. c = (f1 /. c) - (f2 /. c) ) );

existence ( dom it = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom it holds

it /. c = (f1 /. c) - (f2 /. c) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def1 defines + VFUNCT_1:def 1 :

for C being non empty set

for V being non empty addLoopStr

for f1, f2, b_{5} being PartFunc of C,V holds

( b_{5} = f1 + f2 iff ( dom b_{5} = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b_{5} holds

b_{5} /. c = (f1 /. c) + (f2 /. c) ) ) );

for C being non empty set

for V being non empty addLoopStr

for f1, f2, b

( b

b

:: deftheorem Def2 defines - VFUNCT_1:def 2 :

for C being non empty set

for V being non empty addLoopStr

for f1, f2, b_{5} being PartFunc of C,V holds

( b_{5} = f1 - f2 iff ( dom b_{5} = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b_{5} holds

b_{5} /. c = (f1 /. c) - (f2 /. c) ) ) );

for C being non empty set

for V being non empty addLoopStr

for f1, f2, b

( b

b

registration

let C be non empty set ;

let V be non empty addLoopStr ;

let f1, f2 be Function of C,V;

coherence

f1 + f2 is total

f1 - f2 is total

end;
let V be non empty addLoopStr ;

let f1, f2 be Function of C,V;

coherence

f1 + f2 is total

proof end;

coherence f1 - f2 is total

proof end;

definition

let C be non empty set ;

let V be non empty RLSStruct ;

let f1 be PartFunc of C,REAL;

let f2 be PartFunc of C,V;

deffunc H_{1}( Element of C) -> Element of the U1 of V = (f1 . $1) * (f2 /. $1);

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

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

ex b_{1} being PartFunc of C,V st

( dom b_{1} = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b_{1} holds

b_{1} /. c = (f1 . c) * (f2 /. c) ) )

for b_{1}, b_{2} being PartFunc of C,V st dom b_{1} = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b_{1} holds

b_{1} /. c = (f1 . c) * (f2 /. c) ) & dom b_{2} = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b_{2} holds

b_{2} /. c = (f1 . c) * (f2 /. c) ) holds

b_{1} = b_{2}

end;
let V be non empty RLSStruct ;

let f1 be PartFunc of C,REAL;

let f2 be PartFunc of C,V;

deffunc H

defpred S

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

func f1 (#) f2 -> PartFunc of C,V means :Def3: :: VFUNCT_1:def 3

( dom it = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom it holds

it /. c = (f1 . c) * (f2 /. c) ) );

existence ( dom it = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom it holds

it /. c = (f1 . c) * (f2 /. c) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def3 defines (#) VFUNCT_1:def 3 :

for C being non empty set

for V being non empty RLSStruct

for f1 being PartFunc of C,REAL

for f2, b_{5} being PartFunc of C,V holds

( b_{5} = f1 (#) f2 iff ( dom b_{5} = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b_{5} holds

b_{5} /. c = (f1 . c) * (f2 /. c) ) ) );

for C being non empty set

for V being non empty RLSStruct

for f1 being PartFunc of C,REAL

for f2, b

( b

b

registration

let C be non empty set ;

let V be non empty RLSStruct ;

let f1 be Function of C,REAL;

let f2 be Function of C,V;

coherence

f1 (#) f2 is total

end;
let V be non empty RLSStruct ;

let f1 be Function of C,REAL;

let f2 be Function of C,V;

coherence

f1 (#) f2 is total

proof end;

definition

let C be non empty set ;

let V be non empty RLSStruct ;

let f be PartFunc of C,V;

let r be Real;

deffunc H_{1}( Element of C) -> Element of the U1 of V = r * (f /. $1);

defpred S_{1}[ set ] means $1 in dom f;

ex b_{1} being PartFunc of C,V st

( dom b_{1} = dom f & ( for c being Element of C st c in dom b_{1} holds

b_{1} /. c = r * (f /. c) ) )

for b_{1}, b_{2} being PartFunc of C,V st dom b_{1} = dom f & ( for c being Element of C st c in dom b_{1} holds

b_{1} /. c = r * (f /. c) ) & dom b_{2} = dom f & ( for c being Element of C st c in dom b_{2} holds

b_{2} /. c = r * (f /. c) ) holds

b_{1} = b_{2}

end;
let V be non empty RLSStruct ;

let f be PartFunc of C,V;

let r be Real;

deffunc H

defpred S

func r (#) f -> PartFunc of C,V means :Def4: :: VFUNCT_1:def 4

( dom it = dom f & ( for c being Element of C st c in dom it holds

it /. c = r * (f /. c) ) );

existence ( dom it = dom f & ( for c being Element of C st c in dom it holds

it /. c = r * (f /. c) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def4 defines (#) VFUNCT_1:def 4 :

for C being non empty set

for V being non empty RLSStruct

for f being PartFunc of C,V

for r being Real

for b_{5} being PartFunc of C,V holds

( b_{5} = r (#) f iff ( dom b_{5} = dom f & ( for c being Element of C st c in dom b_{5} holds

b_{5} /. c = r * (f /. c) ) ) );

for C being non empty set

for V being non empty RLSStruct

for f being PartFunc of C,V

for r being Real

for b

( b

b

registration

let C be non empty set ;

let V be non empty RLSStruct ;

let f be Function of C,V;

let r be Real;

coherence

r (#) f is total

end;
let V be non empty RLSStruct ;

let f be Function of C,V;

let r be Real;

coherence

r (#) f is total

proof end;

definition

let C be non empty set ;

let V be non empty addLoopStr ;

let f be PartFunc of C,V;

deffunc H_{1}( Element of C) -> Element of the U1 of V = - (f /. $1);

defpred S_{1}[ set ] means $1 in dom f;

ex b_{1} being PartFunc of C,V st

( dom b_{1} = dom f & ( for c being Element of C st c in dom b_{1} holds

b_{1} /. c = - (f /. c) ) )

for b_{1}, b_{2} being PartFunc of C,V st dom b_{1} = dom f & ( for c being Element of C st c in dom b_{1} holds

b_{1} /. c = - (f /. c) ) & dom b_{2} = dom f & ( for c being Element of C st c in dom b_{2} holds

b_{2} /. c = - (f /. c) ) holds

b_{1} = b_{2}

end;
let V be non empty addLoopStr ;

let f be PartFunc of C,V;

deffunc H

defpred S

func - f -> PartFunc of C,V means :Def5: :: VFUNCT_1:def 5

( dom it = dom f & ( for c being Element of C st c in dom it holds

it /. c = - (f /. c) ) );

existence ( dom it = dom f & ( for c being Element of C st c in dom it holds

it /. c = - (f /. c) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def5 defines - VFUNCT_1:def 5 :

for C being non empty set

for V being non empty addLoopStr

for f, b_{4} being PartFunc of C,V holds

( b_{4} = - f iff ( dom b_{4} = dom f & ( for c being Element of C st c in dom b_{4} holds

b_{4} /. c = - (f /. c) ) ) );

for C being non empty set

for V being non empty addLoopStr

for f, b

( b

b

registration

let C be non empty set ;

let V be non empty addLoopStr ;

let f be Function of C,V;

coherence

- f is total

end;
let V be non empty addLoopStr ;

let f be Function of C,V;

coherence

- f is total

proof end;

theorem :: VFUNCT_1:1

for C being non empty set

for V being RealNormSpace

for f2 being PartFunc of C,V

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

for V being RealNormSpace

for f2 being PartFunc of C,V

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

proof end;

theorem :: VFUNCT_1:2

for C being non empty set

for V being RealNormSpace

for f being PartFunc of C,V holds

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

for V being RealNormSpace

for f being PartFunc of C,V holds

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

proof end;

theorem :: VFUNCT_1:3

for C being non empty set

for V being RealNormSpace

for f being PartFunc of C,V

for r being Real st r <> 0 holds

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

for V being RealNormSpace

for f being PartFunc of C,V

for r being Real st r <> 0 holds

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

proof end;

::

:: BASIC PROPERTIES OF OPERATIONS

::

:: BASIC PROPERTIES OF OPERATIONS

::

theorem Th4: :: VFUNCT_1:4

for C being non empty set

for V being non empty Abelian addLoopStr

for f1, f2 being PartFunc of C,V holds f1 + f2 = f2 + f1

for V being non empty Abelian addLoopStr

for f1, f2 being PartFunc of C,V holds f1 + f2 = f2 + f1

proof end;

definition

let C be non empty set ;

let V be non empty Abelian addLoopStr ;

let f1, f2 be PartFunc of C,V;

:: original: +

redefine func f1 + f2 -> PartFunc of C,V;

commutativity

for f1, f2 being PartFunc of C,V holds f1 + f2 = f2 + f1 by Th4;

end;
let V be non empty Abelian addLoopStr ;

let f1, f2 be PartFunc of C,V;

:: original: +

redefine func f1 + f2 -> PartFunc of C,V;

commutativity

for f1, f2 being PartFunc of C,V holds f1 + f2 = f2 + f1 by Th4;

theorem :: VFUNCT_1:5

for C being non empty set

for V being non empty add-associative addLoopStr

for f1, f2, f3 being PartFunc of C,V holds (f1 + f2) + f3 = f1 + (f2 + f3)

for V being non empty add-associative addLoopStr

for f1, f2, f3 being PartFunc of C,V holds (f1 + f2) + f3 = f1 + (f2 + f3)

proof end;

theorem :: VFUNCT_1:6

for C being non empty set

for V being non empty scalar-associative RLSStruct

for f1, f2 being PartFunc of C,REAL

for f3 being PartFunc of C,V holds (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3)

for V being non empty scalar-associative RLSStruct

for f1, f2 being PartFunc of C,REAL

for f3 being PartFunc of C,V holds (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3)

proof end;

theorem :: VFUNCT_1:7

for C being non empty set

for V being non empty scalar-distributive RLSStruct

for f1, f2 being PartFunc of C,REAL

for f3 being Function of C,V holds (f1 + f2) (#) f3 = (f1 (#) f3) + (f2 (#) f3)

for V being non empty scalar-distributive RLSStruct

for f1, f2 being PartFunc of C,REAL

for f3 being Function of C,V holds (f1 + f2) (#) f3 = (f1 (#) f3) + (f2 (#) f3)

proof end;

theorem :: VFUNCT_1:8

for C being non empty set

for V being non empty vector-distributive RLSStruct

for f1, f2 being PartFunc of C,V

for f3 being Function of C,REAL holds f3 (#) (f1 + f2) = (f3 (#) f1) + (f3 (#) f2)

for V being non empty vector-distributive RLSStruct

for f1, f2 being PartFunc of C,V

for f3 being Function of C,REAL holds f3 (#) (f1 + f2) = (f3 (#) f1) + (f3 (#) f2)

proof end;

theorem :: VFUNCT_1:9

for C being non empty set

for r being Real

for V being non empty scalar-associative RLSStruct

for f1 being PartFunc of C,REAL

for f2 being PartFunc of C,V holds r (#) (f1 (#) f2) = (r (#) f1) (#) f2

for r being Real

for V being non empty scalar-associative RLSStruct

for f1 being PartFunc of C,REAL

for f2 being PartFunc of C,V holds r (#) (f1 (#) f2) = (r (#) f1) (#) f2

proof end;

theorem :: VFUNCT_1:10

for C being non empty set

for r being Real

for V being non empty scalar-associative RLSStruct

for f1 being PartFunc of C,REAL

for f2 being PartFunc of C,V holds r (#) (f1 (#) f2) = f1 (#) (r (#) f2)

for r being Real

for V being non empty scalar-associative RLSStruct

for f1 being PartFunc of C,REAL

for f2 being PartFunc of C,V holds r (#) (f1 (#) f2) = f1 (#) (r (#) f2)

proof end;

theorem :: VFUNCT_1:11

for C being non empty set

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for f1, f2 being PartFunc of C,REAL

for f3 being Function of C,V holds (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3)

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for f1, f2 being PartFunc of C,REAL

for f3 being Function of C,V holds (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3)

proof end;

theorem :: VFUNCT_1:12

for C being non empty set

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for f1, f2 being PartFunc of C,V

for f3 being PartFunc of C,REAL holds (f3 (#) f1) - (f3 (#) f2) = f3 (#) (f1 - f2)

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for f1, f2 being PartFunc of C,V

for f3 being PartFunc of C,REAL holds (f3 (#) f1) - (f3 (#) f2) = f3 (#) (f1 - f2)

proof end;

theorem :: VFUNCT_1:13

for C being non empty set

for r being Real

for V being non empty vector-distributive RLSStruct

for f1, f2 being PartFunc of C,V holds r (#) (f1 + f2) = (r (#) f1) + (r (#) f2)

for r being Real

for V being non empty vector-distributive RLSStruct

for f1, f2 being PartFunc of C,V holds r (#) (f1 + f2) = (r (#) f1) + (r (#) f2)

proof end;

theorem :: VFUNCT_1:14

for C being non empty set

for r, p being Real

for V being non empty scalar-associative RLSStruct

for f being PartFunc of C,V holds (r * p) (#) f = r (#) (p (#) f)

for r, p being Real

for V being non empty scalar-associative RLSStruct

for f being PartFunc of C,V holds (r * p) (#) f = r (#) (p (#) f)

proof end;

theorem :: VFUNCT_1:15

for C being non empty set

for r being Real

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for f1, f2 being PartFunc of C,V holds r (#) (f1 - f2) = (r (#) f1) - (r (#) f2)

for r being Real

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for f1, f2 being PartFunc of C,V holds r (#) (f1 - f2) = (r (#) f1) - (r (#) f2)

proof end;

theorem :: VFUNCT_1:16

for C being non empty set

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-unital RLSStruct

for f1, f2 being PartFunc of C,V holds f1 - f2 = (- 1) (#) (f2 - f1)

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-unital RLSStruct

for f1, f2 being PartFunc of C,V holds f1 - f2 = (- 1) (#) (f2 - f1)

proof end;

theorem :: VFUNCT_1:17

for C being non empty set

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for f1, f2, f3 being PartFunc of C,V holds f1 - (f2 + f3) = (f1 - f2) - f3

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for f1, f2, f3 being PartFunc of C,V holds f1 - (f2 + f3) = (f1 - f2) - f3

proof end;

theorem :: VFUNCT_1:18

for C being non empty set

for V being non empty scalar-unital RLSStruct

for f being PartFunc of C,V holds 1 (#) f = f

for V being non empty scalar-unital RLSStruct

for f being PartFunc of C,V holds 1 (#) f = f

proof end;

theorem :: VFUNCT_1:19

for C being non empty set

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for f1, f2, f3 being PartFunc of C,V holds f1 - (f2 - f3) = (f1 - f2) + f3

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for f1, f2, f3 being PartFunc of C,V holds f1 - (f2 - f3) = (f1 - f2) + f3

proof end;

theorem :: VFUNCT_1:20

for C being non empty set

for V being non empty add-associative addLoopStr

for f1, f2, f3 being PartFunc of C,V holds f1 + (f2 - f3) = (f1 + f2) - f3

for V being non empty add-associative addLoopStr

for f1, f2, f3 being PartFunc of C,V holds f1 + (f2 - f3) = (f1 + f2) - f3

proof end;

theorem :: VFUNCT_1:21

for C being non empty set

for V being non empty RealNormSpace-like NORMSTR

for f1 being PartFunc of C,REAL

for f2 being PartFunc of C,V holds ||.(f1 (#) f2).|| = (abs f1) (#) ||.f2.||

for V being non empty RealNormSpace-like NORMSTR

for f1 being PartFunc of C,REAL

for f2 being PartFunc of C,V holds ||.(f1 (#) f2).|| = (abs f1) (#) ||.f2.||

proof end;

theorem :: VFUNCT_1:22

for C being non empty set

for r being Real

for V being non empty RealNormSpace-like NORMSTR

for f being PartFunc of C,V holds ||.(r (#) f).|| = |.r.| (#) ||.f.||

for r being Real

for V being non empty RealNormSpace-like NORMSTR

for f being PartFunc of C,V holds ||.(r (#) f).|| = |.r.| (#) ||.f.||

proof end;

theorem Th23: :: VFUNCT_1:23

for C being non empty set

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-unital RLSStruct

for f being PartFunc of C,V holds - f = (- 1) (#) f

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-unital RLSStruct

for f being PartFunc of C,V holds - f = (- 1) (#) f

proof end;

theorem Th24: :: VFUNCT_1:24

for C being non empty set

for V being non empty right_complementable add-associative right_zeroed addLoopStr

for f being PartFunc of C,V holds - (- f) = f

for V being non empty right_complementable add-associative right_zeroed addLoopStr

for f being PartFunc of C,V holds - (- f) = f

proof end;

theorem Th25: :: VFUNCT_1:25

for C being non empty set

for V being non empty addLoopStr

for f1, f2 being PartFunc of C,V holds f1 - f2 = f1 + (- f2)

for V being non empty addLoopStr

for f1, f2 being PartFunc of C,V holds f1 - f2 = f1 + (- f2)

proof end;

theorem :: VFUNCT_1:26

for C being non empty set

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for f1, f2 being PartFunc of C,V holds f1 - (- f2) = f1 + f2

for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

for f1, f2 being PartFunc of C,V holds f1 - (- f2) = f1 + f2

proof end;

theorem Th27: :: VFUNCT_1:27

for X being set

for C being non empty set

for V being RealNormSpace

for f1, f2 being PartFunc of C,V holds

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

for C being non empty set

for V being RealNormSpace

for f1, f2 being PartFunc of C,V holds

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

proof end;

theorem :: VFUNCT_1:28

for X being set

for C being non empty set

for V being RealNormSpace

for f2 being PartFunc of C,V

for f1 being PartFunc of C,REAL holds

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

for C being non empty set

for V being RealNormSpace

for f2 being PartFunc of C,V

for f1 being 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 end;

theorem Th29: :: VFUNCT_1:29

for X being set

for C being non empty set

for V being RealNormSpace

for f being PartFunc of C,V holds

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

for C being non empty set

for V being RealNormSpace

for f being PartFunc of C,V holds

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

proof end;

theorem :: VFUNCT_1:30

for X being set

for C being non empty set

for V being RealNormSpace

for f1, f2 being PartFunc of C,V holds

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

for C being non empty set

for V being RealNormSpace

for f1, f2 being PartFunc of C,V holds

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

proof end;

theorem :: VFUNCT_1:31

for X being set

for C being non empty set

for V being RealNormSpace

for f being PartFunc of C,V

for r being Real holds (r (#) f) | X = r (#) (f | X)

for C being non empty set

for V being RealNormSpace

for f being PartFunc of C,V

for r being Real holds (r (#) f) | X = r (#) (f | X)

proof end;

::

:: TOTAL PARTIAL FUNCTIONS FROM A DOMAIN TO REAL

::

:: TOTAL PARTIAL FUNCTIONS FROM A DOMAIN TO REAL

::

theorem :: VFUNCT_1:32

for C being non empty set

for V being RealNormSpace

for f1, f2 being PartFunc of C,V holds

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

for V being RealNormSpace

for f1, f2 being PartFunc of C,V holds

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

proof end;

theorem :: VFUNCT_1:33

for C being non empty set

for V being RealNormSpace

for f2 being PartFunc of C,V

for f1 being PartFunc of C,REAL holds

( ( f1 is total & f2 is total ) iff f1 (#) f2 is total )

for V being RealNormSpace

for f2 being PartFunc of C,V

for f1 being PartFunc of C,REAL holds

( ( f1 is total & f2 is total ) iff f1 (#) f2 is total )

proof end;

theorem :: VFUNCT_1:34

theorem :: VFUNCT_1:35

for C being non empty set

for V being RealNormSpace

for f being PartFunc of C,V holds

( f is total iff - f is total )

for V being RealNormSpace

for f being PartFunc of C,V holds

( f is total iff - f is total )

proof end;

theorem :: VFUNCT_1:36

for C being non empty set

for V being RealNormSpace

for f being PartFunc of C,V holds

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

for V being RealNormSpace

for f being PartFunc of C,V holds

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

theorem :: VFUNCT_1:37

for C being non empty set

for c being Element of C

for V being RealNormSpace

for f1, f2 being PartFunc of C,V st f1 is total & f2 is total holds

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

for c being Element of C

for V being RealNormSpace

for f1, f2 being PartFunc of C,V st f1 is total & f2 is total holds

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

proof end;

theorem :: VFUNCT_1:38

for C being non empty set

for c being Element of C

for V being RealNormSpace

for f2 being PartFunc of C,V

for f1 being PartFunc of C,REAL st f1 is total & f2 is total holds

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

for c being Element of C

for V being RealNormSpace

for f2 being PartFunc of C,V

for f1 being PartFunc of C,REAL st f1 is total & f2 is total holds

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

proof end;

theorem :: VFUNCT_1:39

for C being non empty set

for c being Element of C

for V being RealNormSpace

for f being PartFunc of C,V

for r being Real st f is total holds

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

for c being Element of C

for V being RealNormSpace

for f being PartFunc of C,V

for r being Real st f is total holds

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

proof end;

theorem :: VFUNCT_1:40

for C being non empty set

for c being Element of C

for V being RealNormSpace

for f being PartFunc of C,V st f is total holds

( (- f) /. c = - (f /. c) & ||.f.|| . c = ||.(f /. c).|| )

for c being Element of C

for V being RealNormSpace

for f being PartFunc of C,V st f is total holds

( (- f) /. c = - (f /. c) & ||.f.|| . c = ||.(f /. c).|| )

proof end;

::

:: BOUNDED AND CONSTANT PARTIAL FUNCTIONS FROM A DOMAIN TO A NORMED REAL SPACE

::

:: BOUNDED AND CONSTANT PARTIAL FUNCTIONS FROM A DOMAIN TO A NORMED REAL SPACE

::

definition
end;

:: deftheorem defines is_bounded_on VFUNCT_1:def 6 :

for C being non empty set

for V being non empty NORMSTR

for f being PartFunc of C,V

for Y being set holds

( f is_bounded_on Y iff ex r being Real st

for c being Element of C st c in Y /\ (dom f) holds

||.(f /. c).|| <= r );

for C being non empty set

for V being non empty NORMSTR

for f being PartFunc of C,V

for Y being set holds

( f is_bounded_on Y iff ex r being Real st

for c being Element of C st c in Y /\ (dom f) holds

||.(f /. c).|| <= r );

theorem :: VFUNCT_1:41

for X, Y being set

for C being non empty set

for V being RealNormSpace

for f being PartFunc of C,V st Y c= X & f is_bounded_on X holds

f is_bounded_on Y

for C being non empty set

for V being RealNormSpace

for f being PartFunc of C,V st Y c= X & f is_bounded_on X holds

f is_bounded_on Y

proof end;

theorem :: VFUNCT_1:42

for X being set

for C being non empty set

for V being RealNormSpace

for f being PartFunc of C,V st X misses dom f holds

f is_bounded_on X

for C being non empty set

for V being RealNormSpace

for f being PartFunc of C,V st X misses dom f holds

f is_bounded_on X

proof end;

theorem :: VFUNCT_1:43

for Y being set

for C being non empty set

for V being RealNormSpace

for f being PartFunc of C,V holds 0 (#) f is_bounded_on Y

for C being non empty set

for V being RealNormSpace

for f being PartFunc of C,V holds 0 (#) f is_bounded_on Y

proof end;

theorem Th44: :: VFUNCT_1:44

for Y being set

for C being non empty set

for V being RealNormSpace

for f being PartFunc of C,V

for r being Real st f is_bounded_on Y holds

r (#) f is_bounded_on Y

for C being non empty set

for V being RealNormSpace

for f being PartFunc of C,V

for r being Real st f is_bounded_on Y holds

r (#) f is_bounded_on Y

proof end;

theorem Th45: :: VFUNCT_1:45

for Y being set

for C being non empty set

for V being RealNormSpace

for f being PartFunc of C,V st f is_bounded_on Y holds

( ||.f.|| | Y is bounded & - f is_bounded_on Y )

for C being non empty set

for V being RealNormSpace

for f being PartFunc of C,V st f is_bounded_on Y holds

( ||.f.|| | Y is bounded & - f is_bounded_on Y )

proof end;

theorem Th46: :: VFUNCT_1:46

for X, Y being set

for C being non empty set

for V being RealNormSpace

for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 is_bounded_on Y holds

f1 + f2 is_bounded_on X /\ Y

for C being non empty set

for V being RealNormSpace

for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 is_bounded_on Y holds

f1 + f2 is_bounded_on X /\ Y

proof end;

theorem :: VFUNCT_1:47

for X, Y being set

for C being non empty set

for V being RealNormSpace

for f2 being PartFunc of C,V

for f1 being PartFunc of C,REAL st f1 | X is bounded & f2 is_bounded_on Y holds

f1 (#) f2 is_bounded_on X /\ Y

for C being non empty set

for V being RealNormSpace

for f2 being PartFunc of C,V

for f1 being PartFunc of C,REAL st f1 | X is bounded & f2 is_bounded_on Y holds

f1 (#) f2 is_bounded_on X /\ Y

proof end;

theorem :: VFUNCT_1:48

for X, Y being set

for C being non empty set

for V being RealNormSpace

for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 is_bounded_on Y holds

f1 - f2 is_bounded_on X /\ Y

for C being non empty set

for V being RealNormSpace

for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 is_bounded_on Y holds

f1 - f2 is_bounded_on X /\ Y

proof end;

theorem :: VFUNCT_1:49

for X, Y being set

for C being non empty set

for V being RealNormSpace

for f being PartFunc of C,V st f is_bounded_on X & f is_bounded_on Y holds

f is_bounded_on X \/ Y

for C being non empty set

for V being RealNormSpace

for f being PartFunc of C,V st f is_bounded_on X & f is_bounded_on Y holds

f is_bounded_on X \/ Y

proof end;

theorem :: VFUNCT_1:50

for X, Y being set

for C being non empty set

for V being RealNormSpace

for f1, f2 being PartFunc of C,V st f1 | X is V8() & f2 | Y is V8() holds

( (f1 + f2) | (X /\ Y) is V8() & (f1 - f2) | (X /\ Y) is V8() )

for C being non empty set

for V being RealNormSpace

for f1, f2 being PartFunc of C,V st f1 | X is V8() & f2 | Y is V8() holds

( (f1 + f2) | (X /\ Y) is V8() & (f1 - f2) | (X /\ Y) is V8() )

proof end;

theorem :: VFUNCT_1:51

for X, Y being set

for C being non empty set

for V being RealNormSpace

for f2 being PartFunc of C,V

for f1 being PartFunc of C,REAL st f1 | X is V8() & f2 | Y is V8() holds

(f1 (#) f2) | (X /\ Y) is V8()

for C being non empty set

for V being RealNormSpace

for f2 being PartFunc of C,V

for f1 being PartFunc of C,REAL st f1 | X is V8() & f2 | Y is V8() holds

(f1 (#) f2) | (X /\ Y) is V8()

proof end;

theorem Th52: :: VFUNCT_1:52

for Y being set

for C being non empty set

for V being RealNormSpace

for f being PartFunc of C,V

for p being Real st f | Y is V8() holds

(p (#) f) | Y is V8()

for C being non empty set

for V being RealNormSpace

for f being PartFunc of C,V

for p being Real st f | Y is V8() holds

(p (#) f) | Y is V8()

proof end;

theorem Th53: :: VFUNCT_1:53

for Y being set

for C being non empty set

for V being RealNormSpace

for f being PartFunc of C,V st f | Y is V8() holds

( ||.f.|| | Y is V8() & (- f) | Y is V8() )

for C being non empty set

for V being RealNormSpace

for f being PartFunc of C,V st f | Y is V8() holds

( ||.f.|| | Y is V8() & (- f) | Y is V8() )

proof end;

theorem Th54: :: VFUNCT_1:54

for Y being set

for C being non empty set

for V being RealNormSpace

for f being PartFunc of C,V st f | Y is V8() holds

f is_bounded_on Y

for C being non empty set

for V being RealNormSpace

for f being PartFunc of C,V st f | Y is V8() holds

f is_bounded_on Y

proof end;

theorem :: VFUNCT_1:55

for Y being set

for C being non empty set

for V being RealNormSpace

for f being PartFunc of C,V st f | Y is V8() holds

( ( for r being Real holds r (#) f is_bounded_on Y ) & - f is_bounded_on Y & ||.f.|| | Y is bounded )

for C being non empty set

for V being RealNormSpace

for f being PartFunc of C,V st f | Y is V8() holds

( ( for r being Real holds r (#) f is_bounded_on Y ) & - f is_bounded_on Y & ||.f.|| | Y is bounded )

proof end;

theorem :: VFUNCT_1:56

for X, Y being set

for C being non empty set

for V being RealNormSpace

for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 | Y is V8() holds

f1 + f2 is_bounded_on X /\ Y

for C being non empty set

for V being RealNormSpace

for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 | Y is V8() holds

f1 + f2 is_bounded_on X /\ Y

proof end;

theorem :: VFUNCT_1:57

for X, Y being set

for C being non empty set

for V being RealNormSpace

for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 | Y is V8() holds

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

for C being non empty set

for V being RealNormSpace

for f1, f2 being PartFunc of C,V st f1 is_bounded_on X & f2 | Y is V8() holds

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

proof end;

::OPERATIONS ON PARTIAL FUNCTIONS FROM A DOMAIN TO THE SET OF REAL NUMBERS

::