:: by Takashi Mitsuishi , Katsumi Wasaki and Yasunari Shidama

::

:: Received December 7, 1999

:: Copyright (c) 1999-2012 Association of Mizar Users

begin

definition

let C be non empty set ;

let f1, f2 be PartFunc of C,COMPLEX;

deffunc H_{1}( set ) -> Element of COMPLEX = (f1 /. $1) * ((f2 /. $1) ");

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

( dom b_{1} = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( 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,COMPLEX st dom b_{1} = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( 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) \ (f2 " {0})) & ( 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 f1, f2 be PartFunc of C,COMPLEX;

deffunc H

func f1 / f2 -> PartFunc of C,COMPLEX means :Def1: :: CFUNCT_1:def 1

( dom it = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( 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) \ (f2 " {0})) & ( 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 / CFUNCT_1:def 1 :

for C being non empty set

for f1, f2, b_{4} being PartFunc of C,COMPLEX holds

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

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

for C being non empty set

for f1, f2, b

( b

b

definition

let C be non empty set ;

let f be PartFunc of C,COMPLEX;

deffunc H_{1}( set ) -> Element of COMPLEX = (f /. $1) " ;

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

( dom b_{1} = (dom f) \ (f " {0}) & ( 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,COMPLEX st dom b_{1} = (dom f) \ (f " {0}) & ( for c being Element of C st c in dom b_{1} holds

b_{1} /. c = (f /. c) " ) & dom b_{2} = (dom f) \ (f " {0}) & ( 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 f be PartFunc of C,COMPLEX;

deffunc H

func f ^ -> PartFunc of C,COMPLEX means :Def2: :: CFUNCT_1:def 2

( dom it = (dom f) \ (f " {0}) & ( for c being Element of C st c in dom it holds

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

existence ( dom it = (dom f) \ (f " {0}) & ( 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 Def2 defines ^ CFUNCT_1:def 2 :

for C being non empty set

for f, b_{3} being PartFunc of C,COMPLEX holds

( b_{3} = f ^ iff ( dom b_{3} = (dom f) \ (f " {0}) & ( for c being Element of C st c in dom b_{3} holds

b_{3} /. c = (f /. c) " ) ) );

for C being non empty set

for f, b

( b

b

theorem Th1: :: CFUNCT_1:1

for C being non empty set

for f1, f2 being PartFunc of C,COMPLEX holds

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

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

for f1, f2 being PartFunc of C,COMPLEX holds

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

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

proof end;

theorem Th2: :: CFUNCT_1:2

for C being non empty set

for f1, f2 being PartFunc of C,COMPLEX holds

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

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

for f1, f2 being PartFunc of C,COMPLEX holds

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

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

proof end;

theorem Th3: :: CFUNCT_1:3

for C being non empty set

for f1, f2 being PartFunc of C,COMPLEX holds

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

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

for f1, f2 being PartFunc of C,COMPLEX holds

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

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

proof end;

theorem Th4: :: CFUNCT_1:4

for C being non empty set

for f being PartFunc of C,COMPLEX

for r being Element of COMPLEX holds

( dom (r (#) f) = dom f & ( for c being Element of C st c in dom (r (#) f) holds

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

for f being PartFunc of C,COMPLEX

for r being Element of COMPLEX holds

( dom (r (#) f) = dom f & ( for c being Element of C st c in dom (r (#) f) holds

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

proof end;

theorem Th5: :: CFUNCT_1:5

for C being non empty set

for f being PartFunc of C,COMPLEX holds

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

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

for f being PartFunc of C,COMPLEX holds

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

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

proof end;

Lm1: for x, Y being set

for C being non empty set

for f being PartFunc of C,COMPLEX holds

( x in f " Y iff ( x in dom f & f /. x in Y ) )

by PARTFUN2:26;

theorem Th6: :: CFUNCT_1:6

for C being non empty set

for g being PartFunc of C,COMPLEX holds

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

for g being PartFunc of C,COMPLEX holds

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

proof end;

theorem Th7: :: CFUNCT_1:7

for C being non empty set

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

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

proof end;

theorem Th8: :: CFUNCT_1:8

for C being non empty set

for c being Element of C

for f being PartFunc of C,COMPLEX st c in dom (f ^) holds

f /. c <> 0

for c being Element of C

for f being PartFunc of C,COMPLEX st c in dom (f ^) holds

f /. c <> 0

proof end;

theorem Th10: :: CFUNCT_1:10

for C being non empty set

for f being PartFunc of C,COMPLEX holds

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

for f being PartFunc of C,COMPLEX holds

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

proof end;

theorem Th11: :: CFUNCT_1:11

for C being non empty set

for f being PartFunc of C,COMPLEX holds dom ((f ^) ^) = dom (f | (dom (f ^)))

for f being PartFunc of C,COMPLEX holds dom ((f ^) ^) = dom (f | (dom (f ^)))

proof end;

theorem Th12: :: CFUNCT_1:12

for C being non empty set

for f being PartFunc of C,COMPLEX

for r being Element of COMPLEX st r <> 0 holds

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

for f being PartFunc of C,COMPLEX

for r being Element of COMPLEX st r <> 0 holds

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

proof end;

begin

::

:: BASIC PROPERTIES OF OPERATIONS

::

:: BASIC PROPERTIES OF OPERATIONS

::

theorem :: CFUNCT_1:13

for C being non empty set

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

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

proof end;

theorem Th14: :: CFUNCT_1:14

for C being non empty set

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

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

proof end;

theorem Th15: :: CFUNCT_1:15

for C being non empty set

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

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

proof end;

theorem :: CFUNCT_1:16

theorem Th17: :: CFUNCT_1:17

for C being non empty set

for f1, f2 being PartFunc of C,COMPLEX

for r being Element of COMPLEX holds r (#) (f1 (#) f2) = (r (#) f1) (#) f2

for f1, f2 being PartFunc of C,COMPLEX

for r being Element of COMPLEX holds r (#) (f1 (#) f2) = (r (#) f1) (#) f2

proof end;

theorem Th18: :: CFUNCT_1:18

for C being non empty set

for f1, f2 being PartFunc of C,COMPLEX

for r being Element of COMPLEX holds r (#) (f1 (#) f2) = f1 (#) (r (#) f2)

for f1, f2 being PartFunc of C,COMPLEX

for r being Element of COMPLEX holds r (#) (f1 (#) f2) = f1 (#) (r (#) f2)

proof end;

theorem Th19: :: CFUNCT_1:19

for C being non empty set

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

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

proof end;

theorem :: CFUNCT_1:20

theorem :: CFUNCT_1:21

for C being non empty set

for f1, f2 being PartFunc of C,COMPLEX

for r being Element of COMPLEX holds r (#) (f1 + f2) = (r (#) f1) + (r (#) f2)

for f1, f2 being PartFunc of C,COMPLEX

for r being Element of COMPLEX holds r (#) (f1 + f2) = (r (#) f1) + (r (#) f2)

proof end;

theorem :: CFUNCT_1:22

for C being non empty set

for f being PartFunc of C,COMPLEX

for r, q being Element of COMPLEX holds (r * q) (#) f = r (#) (q (#) f)

for f being PartFunc of C,COMPLEX

for r, q being Element of COMPLEX holds (r * q) (#) f = r (#) (q (#) f)

proof end;

theorem :: CFUNCT_1:23

for C being non empty set

for f1, f2 being PartFunc of C,COMPLEX

for r being Element of COMPLEX holds r (#) (f1 - f2) = (r (#) f1) - (r (#) f2)

for f1, f2 being PartFunc of C,COMPLEX

for r being Element of COMPLEX holds r (#) (f1 - f2) = (r (#) f1) - (r (#) f2)

proof end;

theorem :: CFUNCT_1:24

for C being non empty set

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

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

proof end;

theorem :: CFUNCT_1:25

for C being non empty set

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

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

proof end;

theorem :: CFUNCT_1:27

for C being non empty set

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

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

proof end;

theorem :: CFUNCT_1:28

for C being non empty set

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

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

proof end;

theorem Th29: :: CFUNCT_1:29

for C being non empty set

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

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

proof end;

theorem Th30: :: CFUNCT_1:30

for C being non empty set

for f being PartFunc of C,COMPLEX

for r being Element of COMPLEX holds |.(r (#) f).| = |.r.| (#) |.f.|

for f being PartFunc of C,COMPLEX

for r being Element of COMPLEX holds |.(r (#) f).| = |.r.| (#) |.f.|

proof end;

theorem :: CFUNCT_1:31

theorem :: CFUNCT_1:33

theorem Th35: :: CFUNCT_1:35

for C being non empty set

for f1, f2 being PartFunc of C,COMPLEX holds (f1 (#) f2) ^ = (f1 ^) (#) (f2 ^)

for f1, f2 being PartFunc of C,COMPLEX holds (f1 (#) f2) ^ = (f1 ^) (#) (f2 ^)

proof end;

theorem Th36: :: CFUNCT_1:36

for C being non empty set

for f being PartFunc of C,COMPLEX

for r being Element of COMPLEX st r <> 0 holds

(r (#) f) ^ = (r ") (#) (f ^)

for f being PartFunc of C,COMPLEX

for r being Element of COMPLEX st r <> 0 holds

(r (#) f) ^ = (r ") (#) (f ^)

proof end;

Lm2: (- 1r) " = - 1r

by COMPLEX1:def 4;

theorem :: CFUNCT_1:37

theorem Th40: :: CFUNCT_1:40

for C being non empty set

for g, f being PartFunc of C,COMPLEX

for r being Element of COMPLEX holds r (#) (g / f) = (r (#) g) / f

for g, f being PartFunc of C,COMPLEX

for r being Element of COMPLEX holds r (#) (g / f) = (r (#) g) / f

proof end;

theorem :: CFUNCT_1:41

for C being non empty set

for f, g being PartFunc of C,COMPLEX holds (f / g) (#) g = f | (dom (g ^))

for f, g being PartFunc of C,COMPLEX holds (f / g) (#) g = f | (dom (g ^))

proof end;

theorem Th42: :: CFUNCT_1:42

for C being non empty set

for f, g, f1, g1 being PartFunc of C,COMPLEX holds (f / g) (#) (f1 / g1) = (f (#) f1) / (g (#) g1)

for f, g, f1, g1 being PartFunc of C,COMPLEX holds (f / g) (#) (f1 / g1) = (f (#) f1) / (g (#) g1)

proof end;

theorem Th43: :: CFUNCT_1:43

for C being non empty set

for f1, f2 being PartFunc of C,COMPLEX holds (f1 / f2) ^ = (f2 | (dom (f2 ^))) / f1

for f1, f2 being PartFunc of C,COMPLEX holds (f1 / f2) ^ = (f2 | (dom (f2 ^))) / f1

proof end;

theorem Th44: :: CFUNCT_1:44

for C being non empty set

for g, f1, f2 being PartFunc of C,COMPLEX holds g (#) (f1 / f2) = (g (#) f1) / f2

for g, f1, f2 being PartFunc of C,COMPLEX holds g (#) (f1 / f2) = (g (#) f1) / f2

proof end;

theorem :: CFUNCT_1:45

for C being non empty set

for g, f1, f2 being PartFunc of C,COMPLEX holds g / (f1 / f2) = (g (#) (f2 | (dom (f2 ^)))) / f1

for g, f1, f2 being PartFunc of C,COMPLEX holds g / (f1 / f2) = (g (#) (f2 | (dom (f2 ^)))) / f1

proof end;

theorem :: CFUNCT_1:46

for C being non empty set

for f, g being PartFunc of C,COMPLEX holds

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

for f, g being PartFunc of C,COMPLEX holds

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

proof end;

theorem :: CFUNCT_1:47

for C being non empty set

for f1, f, f2 being PartFunc of C,COMPLEX holds

( (f1 / f) + (f2 / f) = (f1 + f2) / f & (f1 / f) - (f2 / f) = (f1 - f2) / f )

for f1, f, f2 being PartFunc of C,COMPLEX holds

( (f1 / f) + (f2 / f) = (f1 + f2) / f & (f1 / f) - (f2 / f) = (f1 - f2) / f )

proof end;

theorem Th48: :: CFUNCT_1:48

for C being non empty set

for f1, f, g1, g being PartFunc of C,COMPLEX holds (f1 / f) + (g1 / g) = ((f1 (#) g) + (g1 (#) f)) / (f (#) g)

for f1, f, g1, g being PartFunc of C,COMPLEX holds (f1 / f) + (g1 / g) = ((f1 (#) g) + (g1 (#) f)) / (f (#) g)

proof end;

theorem :: CFUNCT_1:49

for C being non empty set

for f, g, f1, g1 being PartFunc of C,COMPLEX holds (f / g) / (f1 / g1) = (f (#) (g1 | (dom (g1 ^)))) / (g (#) f1)

for f, g, f1, g1 being PartFunc of C,COMPLEX holds (f / g) / (f1 / g1) = (f (#) (g1 | (dom (g1 ^)))) / (g (#) f1)

proof end;

theorem :: CFUNCT_1:50

for C being non empty set

for f1, f, g1, g being PartFunc of C,COMPLEX holds (f1 / f) - (g1 / g) = ((f1 (#) g) - (g1 (#) f)) / (f (#) g)

for f1, f, g1, g being PartFunc of C,COMPLEX holds (f1 / f) - (g1 / g) = ((f1 (#) g) - (g1 (#) f)) / (f (#) g)

proof end;

theorem :: CFUNCT_1:51

for C being non empty set

for f1, f2 being PartFunc of C,COMPLEX holds |.(f1 / f2).| = |.f1.| / |.f2.|

for f1, f2 being PartFunc of C,COMPLEX holds |.(f1 / f2).| = |.f1.| / |.f2.|

proof end;

theorem Th52: :: CFUNCT_1:52

for X being set

for C being non empty set

for f1, f2 being PartFunc of C,COMPLEX 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 f1, f2 being PartFunc of C,COMPLEX holds

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

proof end;

theorem Th53: :: CFUNCT_1:53

for X being set

for C being non empty set

for f1, f2 being PartFunc of C,COMPLEX 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 f1, f2 being PartFunc of C,COMPLEX holds

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

proof end;

theorem Th54: :: CFUNCT_1:54

for X being set

for C being non empty set

for f being PartFunc of C,COMPLEX holds

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

for C being non empty set

for f being PartFunc of C,COMPLEX holds

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

proof end;

theorem :: CFUNCT_1:55

for X being set

for C being non empty set

for f1, f2 being PartFunc of C,COMPLEX 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 f1, f2 being PartFunc of C,COMPLEX holds

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

proof end;

theorem :: CFUNCT_1:56

for X being set

for C being non empty set

for f1, f2 being PartFunc of C,COMPLEX 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 f1, f2 being PartFunc of C,COMPLEX holds

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

proof end;

theorem :: CFUNCT_1:57

for X being set

for C being non empty set

for f being PartFunc of C,COMPLEX

for r being Element of COMPLEX holds (r (#) f) | X = r (#) (f | X)

for C being non empty set

for f being PartFunc of C,COMPLEX

for r being Element of COMPLEX holds (r (#) f) | X = r (#) (f | X)

proof end;

begin

::

:: TOTAL PARTIAL FUNCTIONS FROM A DOMAIN, TO COMPLEX

::

:: TOTAL PARTIAL FUNCTIONS FROM A DOMAIN, TO COMPLEX

::

theorem Th58: :: CFUNCT_1:58

for C being non empty set

for f1, f2 being PartFunc of C,COMPLEX 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 ) ) & ( f1 is total & f2 is total implies f1 (#) f2 is total ) & ( f1 (#) f2 is total implies ( f1 is total & f2 is total ) ) )

for f1, f2 being PartFunc of C,COMPLEX 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 ) ) & ( 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 Th59: :: CFUNCT_1:59

for C being non empty set

for f being PartFunc of C,COMPLEX

for r being Element of COMPLEX holds

( f is total iff r (#) f is total )

for f being PartFunc of C,COMPLEX

for r being Element of COMPLEX holds

( f is total iff r (#) f is total )

proof end;

theorem Th62: :: CFUNCT_1:62

for C being non empty set

for f being PartFunc of C,COMPLEX holds

( f ^ is total iff ( f " {0} = {} & f is total ) )

for f being PartFunc of C,COMPLEX holds

( f ^ is total iff ( f " {0} = {} & f is total ) )

proof end;

theorem Th63: :: CFUNCT_1:63

for C being non empty set

for f1, f2 being PartFunc of C,COMPLEX holds

( ( f1 is total & f2 " {0} = {} & f2 is total ) iff f1 / f2 is total )

for f1, f2 being PartFunc of C,COMPLEX holds

( ( f1 is total & f2 " {0} = {} & f2 is total ) iff f1 / f2 is total )

proof end;

theorem :: CFUNCT_1:64

for C being non empty set

for c being Element of C

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

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

for c being Element of C

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

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

proof end;

theorem :: CFUNCT_1:65

for C being non empty set

for c being Element of C

for f being PartFunc of C,COMPLEX

for r being Element of COMPLEX st f is total holds

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

for c being Element of C

for f being PartFunc of C,COMPLEX

for r being Element of COMPLEX st f is total holds

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

proof end;

theorem :: CFUNCT_1:66

for C being non empty set

for c being Element of C

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

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

for c being Element of C

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

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

proof end;

theorem :: CFUNCT_1:67

for C being non empty set

for c being Element of C

for f being PartFunc of C,COMPLEX st f ^ is total holds

(f ^) /. c = (f /. c) "

for c being Element of C

for f being PartFunc of C,COMPLEX st f ^ is total holds

(f ^) /. c = (f /. c) "

proof end;

theorem :: CFUNCT_1:68

for C being non empty set

for c being Element of C

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

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

for c being Element of C

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

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

proof end;

begin

Lm3: for C being non empty set

for f being PartFunc of C,COMPLEX holds

( |.f.| is bounded iff f is bounded )

proof end;

theorem Th69: :: CFUNCT_1:69

for Y being set

for C being non empty set

for f being PartFunc of C,COMPLEX holds

( f | Y is bounded iff ex p being real number st

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

|.(f /. c).| <= p )

for C being non empty set

for f being PartFunc of C,COMPLEX holds

( f | Y is bounded iff ex p being real number st

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

|.(f /. c).| <= p )

proof end;

theorem :: CFUNCT_1:70

for Y, X being set

for C being non empty set

for f being PartFunc of C,COMPLEX st Y c= X & f | X is bounded holds

f | Y is bounded

for C being non empty set

for f being PartFunc of C,COMPLEX st Y c= X & f | X is bounded holds

f | Y is bounded

proof end;

theorem :: CFUNCT_1:71

for X being set

for C being non empty set

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

f | X is bounded

for C being non empty set

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

f | X is bounded

proof end;

theorem Th72: :: CFUNCT_1:72

for Y being set

for C being non empty set

for f being PartFunc of C,COMPLEX

for r being Element of COMPLEX st f | Y is bounded holds

(r (#) f) | Y is bounded

for C being non empty set

for f being PartFunc of C,COMPLEX

for r being Element of COMPLEX st f | Y is bounded holds

(r (#) f) | Y is bounded

proof end;

theorem :: CFUNCT_1:73

for X being set

for C being non empty set

for f being PartFunc of C,COMPLEX holds |.f.| | X is bounded_below

for C being non empty set

for f being PartFunc of C,COMPLEX holds |.f.| | X is bounded_below

proof end;

theorem Th74: :: CFUNCT_1:74

for Y being set

for C being non empty set

for f being PartFunc of C,COMPLEX st f | Y is bounded holds

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

for C being non empty set

for f being PartFunc of C,COMPLEX st f | Y is bounded holds

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

proof end;

theorem Th75: :: CFUNCT_1:75

for X, Y being set

for C being non empty set

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

(f1 + f2) | (X /\ Y) is bounded

for C being non empty set

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

(f1 + f2) | (X /\ Y) is bounded

proof end;

theorem Th76: :: CFUNCT_1:76

for X, Y being set

for C being non empty set

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

( (f1 (#) f2) | (X /\ Y) is bounded & (f1 - f2) | (X /\ Y) is bounded )

for C being non empty set

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

( (f1 (#) f2) | (X /\ Y) is bounded & (f1 - f2) | (X /\ Y) is bounded )

proof end;

theorem :: CFUNCT_1:77

for X, Y being set

for C being non empty set

for f being PartFunc of C,COMPLEX st f | X is bounded & f | Y is bounded holds

f | (X \/ Y) is bounded

for C being non empty set

for f being PartFunc of C,COMPLEX st f | X is bounded & f | Y is bounded holds

f | (X \/ Y) is bounded

proof end;

theorem :: CFUNCT_1:78

for X, Y being set

for C being non empty set

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

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

for C being non empty set

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

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

proof end;

theorem Th79: :: CFUNCT_1:79

for Y being set

for C being non empty set

for f being PartFunc of C,COMPLEX

for q being Element of COMPLEX st f | Y is constant holds

(q (#) f) | Y is constant

for C being non empty set

for f being PartFunc of C,COMPLEX

for q being Element of COMPLEX st f | Y is constant holds

(q (#) f) | Y is constant

proof end;

theorem Th80: :: CFUNCT_1:80

for Y being set

for C being non empty set

for f being PartFunc of C,COMPLEX st f | Y is constant holds

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

for C being non empty set

for f being PartFunc of C,COMPLEX st f | Y is constant holds

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

proof end;

theorem Th81: :: CFUNCT_1:81

for Y being set

for C being non empty set

for f being PartFunc of C,COMPLEX st f | Y is constant holds

f | Y is bounded

for C being non empty set

for f being PartFunc of C,COMPLEX st f | Y is constant holds

f | Y is bounded

proof end;

theorem :: CFUNCT_1:82

for Y being set

for C being non empty set

for f being PartFunc of C,COMPLEX st f | Y is constant holds

( ( for r being Element of COMPLEX holds (r (#) f) | Y is bounded ) & (- f) | Y is bounded & |.f.| | Y is bounded )

for C being non empty set

for f being PartFunc of C,COMPLEX st f | Y is constant holds

( ( for r being Element of COMPLEX holds (r (#) f) | Y is bounded ) & (- f) | Y is bounded & |.f.| | Y is bounded )

proof end;

theorem Th83: :: CFUNCT_1:83

for X, Y being set

for C being non empty set

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

(f1 + f2) | (X /\ Y) is bounded

for C being non empty set

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

(f1 + f2) | (X /\ Y) is bounded

proof end;

theorem :: CFUNCT_1:84

for X, Y being set

for C being non empty set

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

( (f1 - f2) | (X /\ Y) is bounded & (f2 - f1) | (X /\ Y) is bounded & (f1 (#) f2) | (X /\ Y) is bounded )

for C being non empty set

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

( (f1 - f2) | (X /\ Y) is bounded & (f2 - f1) | (X /\ Y) is bounded & (f1 (#) f2) | (X /\ Y) is bounded )

proof end;

theorem :: CFUNCT_1:85

::DEFINITIONS OF COMPLEX FUNCTIONS

::