:: by Noboru Endou

::

:: Received August 20, 2004

:: Copyright (c) 2004-2021 Association of Mizar Users

definition

let M be non empty set ;

let V be ComplexNormSpace;

let f1 be PartFunc of M,COMPLEX;

let f2 be PartFunc of M,V;

deffunc H_{1}( Element of M) -> 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 M,V st

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

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

for b_{1}, b_{2} being PartFunc of M,V st dom b_{1} = (dom f1) /\ (dom f2) & ( for c being Element of M 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 M st c in dom b_{2} holds

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

b_{1} = b_{2}

end;
let V be ComplexNormSpace;

let f1 be PartFunc of M,COMPLEX;

let f2 be PartFunc of M,V;

deffunc H

defpred S

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

func f1 (#) f2 -> PartFunc of M,V means :Def1: :: VFUNCT_2:def 1

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

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

existence ( dom it = (dom f1) /\ (dom f2) & ( for c being Element of M 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_2:def 1 :

for M being non empty set

for V being ComplexNormSpace

for f1 being PartFunc of M,COMPLEX

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

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

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

for M being non empty set

for V being ComplexNormSpace

for f1 being PartFunc of M,COMPLEX

for f2, b

( b

b

definition

let X be non empty set ;

let V be ComplexNormSpace;

let f be PartFunc of X,V;

let z be Complex;

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

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

set M = dom f;

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

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

b_{1} /. x = z * (f /. x) ) )

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

b_{1} /. x = z * (f /. x) ) & dom b_{2} = dom f & ( for x being Element of X st x in dom b_{2} holds

b_{2} /. x = z * (f /. x) ) holds

b_{1} = b_{2}

end;
let V be ComplexNormSpace;

let f be PartFunc of X,V;

let z be Complex;

deffunc H

defpred S

set M = dom f;

func z (#) f -> PartFunc of X,V means :Def2: :: VFUNCT_2:def 2

( dom it = dom f & ( for x being Element of X st x in dom it holds

it /. x = z * (f /. x) ) );

existence ( dom it = dom f & ( for x being Element of X st x in dom it holds

it /. x = z * (f /. x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def2 defines (#) VFUNCT_2:def 2 :

for X being non empty set

for V being ComplexNormSpace

for f being PartFunc of X,V

for z being Complex

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

( b_{5} = z (#) f iff ( dom b_{5} = dom f & ( for x being Element of X st x in dom b_{5} holds

b_{5} /. x = z * (f /. x) ) ) );

for X being non empty set

for V being ComplexNormSpace

for f being PartFunc of X,V

for z being Complex

for b

( b

b

theorem :: VFUNCT_2:1

for M being non empty set

for V being ComplexNormSpace

for f1 being PartFunc of M,COMPLEX

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

for V being ComplexNormSpace

for f1 being PartFunc of M,COMPLEX

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

proof end;

theorem :: VFUNCT_2:2

for M being non empty set

for V being ComplexNormSpace

for f being PartFunc of M,V holds

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

for V being ComplexNormSpace

for f being PartFunc of M,V holds

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

proof end;

theorem :: VFUNCT_2:3

for M being non empty set

for V being ComplexNormSpace

for f being PartFunc of M,V

for z being Complex st z <> 0c holds

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

for V being ComplexNormSpace

for f being PartFunc of M,V

for z being Complex st z <> 0c holds

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

proof end;

::

:: BASIC PROPERTIES OF OPERATIONS

::

:: BASIC PROPERTIES OF OPERATIONS

::

definition

let M be non empty set ;

let V be ComplexNormSpace;

let f1, f2 be PartFunc of M,V;

:: original: +

redefine func f1 + f2 -> Element of K16(K17(M, the U1 of V));

commutativity

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

end;
let V be ComplexNormSpace;

let f1, f2 be PartFunc of M,V;

:: original: +

redefine func f1 + f2 -> Element of K16(K17(M, the U1 of V));

commutativity

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

theorem :: VFUNCT_2:5

for M being non empty set

for V being ComplexNormSpace

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

for V being ComplexNormSpace

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

proof end;

theorem :: VFUNCT_2:6

for M being non empty set

for V being ComplexNormSpace

for f1, f2 being PartFunc of M,COMPLEX

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

for V being ComplexNormSpace

for f1, f2 being PartFunc of M,COMPLEX

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

proof end;

theorem :: VFUNCT_2:7

for M being non empty set

for V being ComplexNormSpace

for f3 being PartFunc of M,V

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

for V being ComplexNormSpace

for f3 being PartFunc of M,V

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

proof end;

theorem :: VFUNCT_2:8

for M being non empty set

for V being ComplexNormSpace

for f1, f2 being PartFunc of M,V

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

for V being ComplexNormSpace

for f1, f2 being PartFunc of M,V

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

proof end;

theorem :: VFUNCT_2:9

for M being non empty set

for V being ComplexNormSpace

for f2 being PartFunc of M,V

for z being Complex

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

for V being ComplexNormSpace

for f2 being PartFunc of M,V

for z being Complex

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

proof end;

theorem :: VFUNCT_2:10

for M being non empty set

for V being ComplexNormSpace

for f2 being PartFunc of M,V

for z being Complex

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

for V being ComplexNormSpace

for f2 being PartFunc of M,V

for z being Complex

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

proof end;

theorem :: VFUNCT_2:11

for M being non empty set

for V being ComplexNormSpace

for f3 being PartFunc of M,V

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

for V being ComplexNormSpace

for f3 being PartFunc of M,V

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

proof end;

theorem :: VFUNCT_2:12

for M being non empty set

for V being ComplexNormSpace

for f1, f2 being PartFunc of M,V

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

for V being ComplexNormSpace

for f1, f2 being PartFunc of M,V

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

proof end;

theorem :: VFUNCT_2:13

for M being non empty set

for V being ComplexNormSpace

for f1, f2 being PartFunc of M,V

for z being Complex holds z (#) (f1 + f2) = (z (#) f1) + (z (#) f2)

for V being ComplexNormSpace

for f1, f2 being PartFunc of M,V

for z being Complex holds z (#) (f1 + f2) = (z (#) f1) + (z (#) f2)

proof end;

theorem Th14: :: VFUNCT_2:14

for M being non empty set

for V being ComplexNormSpace

for f being PartFunc of M,V

for z1, z2 being Complex holds (z1 * z2) (#) f = z1 (#) (z2 (#) f)

for V being ComplexNormSpace

for f being PartFunc of M,V

for z1, z2 being Complex holds (z1 * z2) (#) f = z1 (#) (z2 (#) f)

proof end;

theorem :: VFUNCT_2:15

for M being non empty set

for V being ComplexNormSpace

for f1, f2 being PartFunc of M,V

for z being Complex holds z (#) (f1 - f2) = (z (#) f1) - (z (#) f2)

for V being ComplexNormSpace

for f1, f2 being PartFunc of M,V

for z being Complex holds z (#) (f1 - f2) = (z (#) f1) - (z (#) f2)

proof end;

theorem :: VFUNCT_2:16

for M being non empty set

for V being ComplexNormSpace

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

for V being ComplexNormSpace

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

proof end;

theorem :: VFUNCT_2:17

for M being non empty set

for V being ComplexNormSpace

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

for V being ComplexNormSpace

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

proof end;

theorem Th18: :: VFUNCT_2:18

for M being non empty set

for V being ComplexNormSpace

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

for V being ComplexNormSpace

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

proof end;

theorem :: VFUNCT_2:19

for M being non empty set

for V being ComplexNormSpace

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

for V being ComplexNormSpace

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

proof end;

theorem :: VFUNCT_2:20

for M being non empty set

for V being ComplexNormSpace

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

for V being ComplexNormSpace

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

proof end;

theorem :: VFUNCT_2:21

for M being non empty set

for V being ComplexNormSpace

for f2 being PartFunc of M,V

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

for V being ComplexNormSpace

for f2 being PartFunc of M,V

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

proof end;

theorem :: VFUNCT_2:22

for M being non empty set

for V being ComplexNormSpace

for f being PartFunc of M,V

for z being Complex holds ||.(z (#) f).|| = |.z.| (#) ||.f.||

for V being ComplexNormSpace

for f being PartFunc of M,V

for z being Complex holds ||.(z (#) f).|| = |.z.| (#) ||.f.||

proof end;

theorem Th23: :: VFUNCT_2:23

for M being non empty set

for V being ComplexNormSpace

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

for V being ComplexNormSpace

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

proof end;

theorem Th24: :: VFUNCT_2:24

for M being non empty set

for V being ComplexNormSpace

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

for V being ComplexNormSpace

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

proof end;

theorem Th25: :: VFUNCT_2:25

for M being non empty set

for V being ComplexNormSpace

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

for V being ComplexNormSpace

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

proof end;

theorem :: VFUNCT_2:26

for M being non empty set

for V being ComplexNormSpace

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

for V being ComplexNormSpace

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

proof end;

theorem Th27: :: VFUNCT_2:27

for M being non empty set

for V being ComplexNormSpace

for f1, f2 being PartFunc of M,V

for X being set holds

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

for V being ComplexNormSpace

for f1, f2 being PartFunc of M,V

for X being set holds

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

proof end;

theorem :: VFUNCT_2:28

for M being non empty set

for V being ComplexNormSpace

for f2 being PartFunc of M,V

for X being set

for f1 being PartFunc of M,COMPLEX holds

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

for V being ComplexNormSpace

for f2 being PartFunc of M,V

for X being set

for f1 being PartFunc of M,COMPLEX holds

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

proof end;

theorem Th29: :: VFUNCT_2:29

for M being non empty set

for V being ComplexNormSpace

for f being PartFunc of M,V

for X being set holds

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

for V being ComplexNormSpace

for f being PartFunc of M,V

for X being set holds

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

proof end;

theorem :: VFUNCT_2:30

for M being non empty set

for V being ComplexNormSpace

for f1, f2 being PartFunc of M,V

for X being set holds

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

for V being ComplexNormSpace

for f1, f2 being PartFunc of M,V

for X being set holds

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

proof end;

theorem :: VFUNCT_2:31

for M being non empty set

for V being ComplexNormSpace

for f being PartFunc of M,V

for z being Complex

for X being set holds (z (#) f) | X = z (#) (f | X)

for V being ComplexNormSpace

for f being PartFunc of M,V

for z being Complex

for X being set holds (z (#) f) | X = z (#) (f | X)

proof end;

::

:: TOTAL PARTIAL FUNCTIONS FROM A DOMAIN TO COMPLEX

::

:: TOTAL PARTIAL FUNCTIONS FROM A DOMAIN TO COMPLEX

::

theorem Th32: :: VFUNCT_2:32

for M being non empty set

for V being ComplexNormSpace

for f1, f2 being PartFunc of M,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 ComplexNormSpace

for f1, f2 being PartFunc of M,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 Th33: :: VFUNCT_2:33

for M being non empty set

for V being ComplexNormSpace

for f2 being PartFunc of M,V

for f1 being PartFunc of M,COMPLEX holds

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

for V being ComplexNormSpace

for f2 being PartFunc of M,V

for f1 being PartFunc of M,COMPLEX holds

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

proof end;

theorem Th35: :: VFUNCT_2:35

for M being non empty set

for V being ComplexNormSpace

for f being PartFunc of M,V holds

( f is total iff - f is total )

for V being ComplexNormSpace

for f being PartFunc of M,V holds

( f is total iff - f is total )

proof end;

theorem Th36: :: VFUNCT_2:36

for M being non empty set

for V being ComplexNormSpace

for f being PartFunc of M,V holds

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

for V being ComplexNormSpace

for f being PartFunc of M,V holds

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

theorem :: VFUNCT_2:37

for M being non empty set

for V being ComplexNormSpace

for f1, f2 being PartFunc of M,V

for x being Element of M st f1 is total & f2 is total holds

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

for V being ComplexNormSpace

for f1, f2 being PartFunc of M,V

for x being Element of M st f1 is total & f2 is total holds

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

proof end;

theorem :: VFUNCT_2:38

for M being non empty set

for V being ComplexNormSpace

for f2 being PartFunc of M,V

for f1 being PartFunc of M,COMPLEX

for x being Element of M st f1 is total & f2 is total holds

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

for V being ComplexNormSpace

for f2 being PartFunc of M,V

for f1 being PartFunc of M,COMPLEX

for x being Element of M st f1 is total & f2 is total holds

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

proof end;

theorem :: VFUNCT_2:39

for M being non empty set

for V being ComplexNormSpace

for f being PartFunc of M,V

for z being Complex

for x being Element of M st f is total holds

(z (#) f) /. x = z * (f /. x)

for V being ComplexNormSpace

for f being PartFunc of M,V

for z being Complex

for x being Element of M st f is total holds

(z (#) f) /. x = z * (f /. x)

proof end;

theorem :: VFUNCT_2:40

for M being non empty set

for V being ComplexNormSpace

for f being PartFunc of M,V

for x being Element of M st f is total holds

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

for V being ComplexNormSpace

for f being PartFunc of M,V

for x being Element of M st f is total holds

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

proof end;

::

:: BOUNDED AND CONSTANT PARTIAL FUNCTIONS

:: FROM A DOMAIN TO A NORMED COMPLEX SPACE

::

:: BOUNDED AND CONSTANT PARTIAL FUNCTIONS

:: FROM A DOMAIN TO A NORMED COMPLEX SPACE

::

definition
end;

:: deftheorem defines is_bounded_on VFUNCT_2:def 3 :

for M being non empty set

for V being ComplexNormSpace

for f being PartFunc of M,V

for Y being set holds

( f is_bounded_on Y iff ex r being Real st

for x being Element of M st x in Y /\ (dom f) holds

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

for M being non empty set

for V being ComplexNormSpace

for f being PartFunc of M,V

for Y being set holds

( f is_bounded_on Y iff ex r being Real st

for x being Element of M st x in Y /\ (dom f) holds

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

theorem :: VFUNCT_2:41

for M being non empty set

for V being ComplexNormSpace

for f being PartFunc of M,V

for X, Y being set st Y c= X & f is_bounded_on X holds

f is_bounded_on Y

for V being ComplexNormSpace

for f being PartFunc of M,V

for X, Y being set st Y c= X & f is_bounded_on X holds

f is_bounded_on Y

proof end;

theorem :: VFUNCT_2:42

for M being non empty set

for V being ComplexNormSpace

for f being PartFunc of M,V

for X being set st X misses dom f holds

f is_bounded_on X

for V being ComplexNormSpace

for f being PartFunc of M,V

for X being set st X misses dom f holds

f is_bounded_on X

proof end;

theorem :: VFUNCT_2:43

for M being non empty set

for V being ComplexNormSpace

for f being PartFunc of M,V

for Y being set holds 0c (#) f is_bounded_on Y

for V being ComplexNormSpace

for f being PartFunc of M,V

for Y being set holds 0c (#) f is_bounded_on Y

proof end;

theorem Th44: :: VFUNCT_2:44

for M being non empty set

for V being ComplexNormSpace

for f being PartFunc of M,V

for z being Complex

for Y being set st f is_bounded_on Y holds

z (#) f is_bounded_on Y

for V being ComplexNormSpace

for f being PartFunc of M,V

for z being Complex

for Y being set st f is_bounded_on Y holds

z (#) f is_bounded_on Y

proof end;

theorem Th45: :: VFUNCT_2:45

for M being non empty set

for V being ComplexNormSpace

for f being PartFunc of M,V

for Y being set st f is_bounded_on Y holds

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

for V being ComplexNormSpace

for f being PartFunc of M,V

for Y being set st f is_bounded_on Y holds

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

proof end;

theorem Th46: :: VFUNCT_2:46

for M being non empty set

for V being ComplexNormSpace

for f1, f2 being PartFunc of M,V

for X, Y being set st f1 is_bounded_on X & f2 is_bounded_on Y holds

f1 + f2 is_bounded_on X /\ Y

for V being ComplexNormSpace

for f1, f2 being PartFunc of M,V

for X, Y being set st f1 is_bounded_on X & f2 is_bounded_on Y holds

f1 + f2 is_bounded_on X /\ Y

proof end;

theorem :: VFUNCT_2:47

for M being non empty set

for V being ComplexNormSpace

for f2 being PartFunc of M,V

for X, Y being set

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

f1 (#) f2 is_bounded_on X /\ Y

for V being ComplexNormSpace

for f2 being PartFunc of M,V

for X, Y being set

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

f1 (#) f2 is_bounded_on X /\ Y

proof end;

theorem :: VFUNCT_2:48

for M being non empty set

for V being ComplexNormSpace

for f1, f2 being PartFunc of M,V

for X, Y being set st f1 is_bounded_on X & f2 is_bounded_on Y holds

f1 - f2 is_bounded_on X /\ Y

for V being ComplexNormSpace

for f1, f2 being PartFunc of M,V

for X, Y being set st f1 is_bounded_on X & f2 is_bounded_on Y holds

f1 - f2 is_bounded_on X /\ Y

proof end;

theorem :: VFUNCT_2:49

for M being non empty set

for V being ComplexNormSpace

for f being PartFunc of M,V

for X, Y being set st f is_bounded_on X & f is_bounded_on Y holds

f is_bounded_on X \/ Y

for V being ComplexNormSpace

for f being PartFunc of M,V

for X, Y being set st f is_bounded_on X & f is_bounded_on Y holds

f is_bounded_on X \/ Y

proof end;

theorem :: VFUNCT_2:50

for M being non empty set

for V being ComplexNormSpace

for f1, f2 being PartFunc of M,V

for X, Y being set st f1 | X is constant & f2 | Y is constant holds

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

for V being ComplexNormSpace

for f1, f2 being PartFunc of M,V

for X, Y being set st f1 | X is constant & f2 | Y is constant holds

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

proof end;

theorem :: VFUNCT_2:51

for M being non empty set

for V being ComplexNormSpace

for f2 being PartFunc of M,V

for X, Y being set

for f1 being PartFunc of M,COMPLEX st f1 | X is constant & f2 | Y is constant holds

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

for V being ComplexNormSpace

for f2 being PartFunc of M,V

for X, Y being set

for f1 being PartFunc of M,COMPLEX st f1 | X is constant & f2 | Y is constant holds

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

proof end;

theorem Th52: :: VFUNCT_2:52

for M being non empty set

for V being ComplexNormSpace

for f being PartFunc of M,V

for z being Complex

for Y being set st f | Y is constant holds

(z (#) f) | Y is constant

for V being ComplexNormSpace

for f being PartFunc of M,V

for z being Complex

for Y being set st f | Y is constant holds

(z (#) f) | Y is constant

proof end;

theorem Th53: :: VFUNCT_2:53

for M being non empty set

for V being ComplexNormSpace

for f being PartFunc of M,V

for Y being set st f | Y is constant holds

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

for V being ComplexNormSpace

for f being PartFunc of M,V

for Y being set st f | Y is constant holds

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

proof end;

theorem Th54: :: VFUNCT_2:54

for M being non empty set

for V being ComplexNormSpace

for f being PartFunc of M,V

for Y being set st f | Y is constant holds

f is_bounded_on Y

for V being ComplexNormSpace

for f being PartFunc of M,V

for Y being set st f | Y is constant holds

f is_bounded_on Y

proof end;

theorem :: VFUNCT_2:55

for M being non empty set

for V being ComplexNormSpace

for f being PartFunc of M,V

for Y being set st f | Y is constant holds

( ( for z being Complex holds z (#) f is_bounded_on Y ) & - f is_bounded_on Y & ||.f.|| | Y is bounded )

for V being ComplexNormSpace

for f being PartFunc of M,V

for Y being set st f | Y is constant holds

( ( for z being Complex holds z (#) f is_bounded_on Y ) & - f is_bounded_on Y & ||.f.|| | Y is bounded )

proof end;

theorem :: VFUNCT_2:56

for M being non empty set

for V being ComplexNormSpace

for f1, f2 being PartFunc of M,V

for X, Y being set st f1 is_bounded_on X & f2 | Y is constant holds

f1 + f2 is_bounded_on X /\ Y

for V being ComplexNormSpace

for f1, f2 being PartFunc of M,V

for X, Y being set st f1 is_bounded_on X & f2 | Y is constant holds

f1 + f2 is_bounded_on X /\ Y

proof end;

theorem :: VFUNCT_2:57

for M being non empty set

for V being ComplexNormSpace

for f1, f2 being PartFunc of M,V

for X, Y being set st f1 is_bounded_on X & f2 | Y is constant holds

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

for V being ComplexNormSpace

for f1, f2 being PartFunc of M,V

for X, Y being set st f1 is_bounded_on X & f2 | Y is constant 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 COMPLEX NUMBERS

::