VALUED_2: Operations from Sets into Functional Sets

:: Operations from Sets into Functional Sets
:: by Artur Korni{\l}owicz
::
:: Received October 15, 2008
:: Copyright (c) 2008 Association of Mizar Users

theorem Th1: :: VALUED_2:1

for X1, X2, X3 being set holds X1 /\ (X2 /\ X3) = (X1 /\ X2) /\ (X1 /\ X3)

proof end;

definition

let X be set ;
attr X is complex-functions-membered means :Def1: :: VALUED_2:def 1
for x being set st x in X holds
x is complex-valued Function;

end;

:: deftheorem Def1 defines complex-functions-membered VALUED_2:def 1 :

definition

let X be set ;
attr X is ext-real-functions-membered means :Def2: :: VALUED_2:def 2
for x being set st x in X holds
x is ext-real-valued Function;

end;

:: deftheorem Def2 defines ext-real-functions-membered VALUED_2:def 2 :

definition

let X be set ;
attr X is real-functions-membered means :Def3: :: VALUED_2:def 3
for x being set st x in X holds
x is real-valued Function;

end;

:: deftheorem Def3 defines real-functions-membered VALUED_2:def 3 :

definition

let X be set ;
attr X is rational-functions-membered means :Def4: :: VALUED_2:def 4
for x being set st x in X holds
x is rational-valued Function;

end;

:: deftheorem Def4 defines rational-functions-membered VALUED_2:def 4 :

definition

let X be set ;
attr X is integer-functions-membered means :Def5: :: VALUED_2:def 5
for x being set st x in X holds
x is integer-valued Function;

end;

:: deftheorem Def5 defines integer-functions-membered VALUED_2:def 5 :

definition

let X be set ;
attr X is natural-functions-membered means :Def6: :: VALUED_2:def 6
for x being set st x in X holds
x is natural-valued Function;

end;

:: deftheorem Def6 defines natural-functions-membered VALUED_2:def 6 :

registration

cluster natural-functions-membered -> integer-functions-membered set ;
coherence

proof end;

cluster integer-functions-membered -> rational-functions-membered set ;
coherence

proof end;

cluster rational-functions-membered -> real-functions-membered set ;
coherence

proof end;

cluster real-functions-membered -> complex-functions-membered set ;
coherence

proof end;

cluster real-functions-membered -> ext-real-functions-membered set ;
coherence

proof end;

end;

registration

cluster empty -> natural-functions-membered set ;
coherence

proof end;

end;

registration

let f be complex-valued Function;
cluster {f} -> complex-functions-membered ;
coherence

proof end;

end;

registration

cluster complex-functions-membered -> functional set ;
coherence

proof end;

cluster ext-real-functions-membered -> functional set ;
coherence

proof end;

end;

consider ff being natural-valued Function;

registration

cluster non empty natural-functions-membered set ;
existence

proof end;

end;

registration

let X be complex-functions-membered set ;
cluster -> complex-functions-membered Element of bool X;
coherence

proof end;

end;

registration

let X be ext-real-functions-membered set ;
cluster -> ext-real-functions-membered Element of bool X;
coherence

proof end;

end;

registration

let X be real-functions-membered set ;
cluster -> real-functions-membered Element of bool X;
coherence

proof end;

end;

registration

let X be rational-functions-membered set ;
cluster -> rational-functions-membered Element of bool X;
coherence

proof end;

end;

registration

let X be integer-functions-membered set ;
cluster -> integer-functions-membered Element of bool X;
coherence

proof end;

end;

registration

let X be natural-functions-membered set ;
cluster -> natural-functions-membered Element of bool X;
coherence

proof end;

end;

definition

let D be set ;
set A = COMPLEX ;
defpred S₁[ set ] means $1 is PartFunc of D, COMPLEX ;
func C_PFuncs D -> set means :Def7: :: VALUED_2:def 7
for f being set holds
( f in it iff f is PartFunc of D, COMPLEX );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines C_PFuncs VALUED_2:def 7 :

definition

let D be set ;
set A = COMPLEX ;
defpred S₁[ set ] means $1 is Function of D, COMPLEX ;
func C_Funcs D -> set means :Def8: :: VALUED_2:def 8
for f being set holds
( f in it iff f is Function of D, COMPLEX );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines C_Funcs VALUED_2:def 8 :

definition

let D be set ;
set A = ExtREAL ;
defpred S₁[ set ] means $1 is PartFunc of D, ExtREAL ;
func E_PFuncs D -> set means :Def9: :: VALUED_2:def 9
for f being set holds
( f in it iff f is PartFunc of D, ExtREAL );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines E_PFuncs VALUED_2:def 9 :

definition

let D be set ;
set A = ExtREAL ;
defpred S₁[ set ] means $1 is Function of D, ExtREAL ;
func E_Funcs D -> set means :Def10: :: VALUED_2:def 10
for f being set holds
( f in it iff f is Function of D, ExtREAL );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines E_Funcs VALUED_2:def 10 :

definition

let D be set ;
set A = REAL ;
defpred S₁[ set ] means $1 is PartFunc of D, REAL ;
func R_PFuncs D -> set means :Def11: :: VALUED_2:def 11
for f being set holds
( f in it iff f is PartFunc of D, REAL );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines R_PFuncs VALUED_2:def 11 :

definition

let D be set ;
set A = REAL ;
defpred S₁[ set ] means $1 is Function of D, REAL ;
func R_Funcs D -> set means :Def12: :: VALUED_2:def 12
for f being set holds
( f in it iff f is Function of D, REAL );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines R_Funcs VALUED_2:def 12 :

definition

let D be set ;
set A = RAT ;
defpred S₁[ set ] means $1 is PartFunc of D, RAT ;
func Q_PFuncs D -> set means :Def13: :: VALUED_2:def 13
for f being set holds
( f in it iff f is PartFunc of D, RAT );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines Q_PFuncs VALUED_2:def 13 :

definition

let D be set ;
set A = RAT ;
defpred S₁[ set ] means $1 is Function of D, RAT ;
func Q_Funcs D -> set means :Def14: :: VALUED_2:def 14
for f being set holds
( f in it iff f is Function of D, RAT );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines Q_Funcs VALUED_2:def 14 :

definition

let D be set ;
set A = INT ;
defpred S₁[ set ] means $1 is PartFunc of D, INT ;
func I_PFuncs D -> set means :Def15: :: VALUED_2:def 15
for f being set holds
( f in it iff f is PartFunc of D, INT );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines I_PFuncs VALUED_2:def 15 :

definition

let D be set ;
set A = INT ;
defpred S₁[ set ] means $1 is Function of D, INT ;
func I_Funcs D -> set means :Def16: :: VALUED_2:def 16
for f being set holds
( f in it iff f is Function of D, INT );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def16 defines I_Funcs VALUED_2:def 16 :

definition

let D be set ;
set A = NAT ;
defpred S₁[ set ] means $1 is PartFunc of D, NAT ;
func N_PFuncs D -> set means :Def17: :: VALUED_2:def 17
for f being set holds
( f in it iff f is PartFunc of D, NAT );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def17 defines N_PFuncs VALUED_2:def 17 :

definition

let D be set ;
set A = NAT ;
defpred S₁[ set ] means $1 is Function of D, NAT ;
func N_Funcs D -> set means :Def18: :: VALUED_2:def 18
for f being set holds
( f in it iff f is Function of D, NAT );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def18 defines N_Funcs VALUED_2:def 18 :

theorem Th2: :: VALUED_2:2

for X being set holds C_Funcs X is Subset of (C_PFuncs X)

proof end;

theorem Th3: :: VALUED_2:3

for X being set holds E_Funcs X is Subset of (E_PFuncs X)

proof end;

theorem Th4: :: VALUED_2:4

for X being set holds R_Funcs X is Subset of (R_PFuncs X)

proof end;

theorem Th5: :: VALUED_2:5

for X being set holds Q_Funcs X is Subset of (Q_PFuncs X)

proof end;

theorem Th6: :: VALUED_2:6

for X being set holds I_Funcs X is Subset of (I_PFuncs X)

proof end;

theorem Th7: :: VALUED_2:7

for X being set holds N_Funcs X is Subset of (N_PFuncs X)

proof end;

registration

let X be set ;
cluster C_PFuncs X -> complex-functions-membered ;
coherence

proof end;

cluster C_Funcs X -> complex-functions-membered ;
coherence

proof end;

cluster E_PFuncs X -> ext-real-functions-membered ;
coherence

proof end;

cluster E_Funcs X -> ext-real-functions-membered ;
coherence

proof end;

cluster R_PFuncs X -> real-functions-membered ;
coherence

proof end;

cluster R_Funcs X -> real-functions-membered ;
coherence

proof end;

cluster Q_PFuncs X -> rational-functions-membered ;
coherence

proof end;

cluster Q_Funcs X -> rational-functions-membered ;
coherence

proof end;

cluster I_PFuncs X -> integer-functions-membered ;
coherence

proof end;

cluster I_Funcs X -> integer-functions-membered ;
coherence

proof end;

cluster N_PFuncs X -> natural-functions-membered ;
coherence

proof end;

cluster N_Funcs X -> natural-functions-membered ;
coherence

proof end;

end;

registration

let X be complex-functions-membered set ;
cluster -> complex-valued Element of X;
coherence

proof end;

end;

registration

let X be ext-real-functions-membered set ;
cluster -> ext-real-valued Element of X;
coherence

proof end;

end;

registration

let X be real-functions-membered set ;
cluster -> real-valued Element of X;
coherence

proof end;

end;

registration

let X be rational-functions-membered set ;
cluster -> rational-valued Element of X;
coherence

proof end;

end;

registration

let X be integer-functions-membered set ;
cluster -> integer-valued Element of X;
coherence

proof end;

end;

registration

let X be natural-functions-membered set ;
cluster -> natural-valued Element of X;
coherence

proof end;

end;

registration

let X, x be set ;
let Y be complex-functions-membered set ;
let f be PartFunc of X,Y;
cluster f . x -> Relation-like Function-like ;
coherence

proof end;

end;

registration

let X, x be set ;
let Y be ext-real-functions-membered set ;
let f be PartFunc of X,Y;
cluster f . x -> Relation-like Function-like ;
coherence

proof end;

end;

registration

let X, x be set ;
let Y be complex-functions-membered set ;
let f be PartFunc of X,Y;
cluster f . x -> complex-valued ;
coherence

proof end;

end;

registration

let X, x be set ;
let Y be ext-real-functions-membered set ;
let f be PartFunc of X,Y;
cluster f . x -> ext-real-valued ;
coherence

proof end;

end;

registration

let X, x be set ;
let Y be real-functions-membered set ;
let f be PartFunc of X,Y;
cluster f . x -> real-valued ;
coherence

proof end;

end;

registration

let X, x be set ;
let Y be rational-functions-membered set ;
let f be PartFunc of X,Y;
cluster f . x -> rational-valued ;
coherence

proof end;

end;

registration

let X, x be set ;
let Y be integer-functions-membered set ;
let f be PartFunc of X,Y;
cluster f . x -> integer-valued ;
coherence

proof end;

end;

registration

let X, x be set ;
let Y be natural-functions-membered set ;
let f be PartFunc of X,Y;
cluster f . x -> natural-valued ;
coherence

proof end;

end;

registration

let X be set ;
let Y be complex-membered set ;
cluster PFuncs X,Y -> complex-functions-membered ;
coherence

proof end;

end;

registration

let X be set ;
let Y be ext-real-membered set ;
cluster PFuncs X,Y -> ext-real-functions-membered ;
coherence

proof end;

end;

registration

let X be set ;
let Y be real-membered set ;
cluster PFuncs X,Y -> real-functions-membered ;
coherence

proof end;

end;

registration

let X be set ;
let Y be rational-membered set ;
cluster PFuncs X,Y -> rational-functions-membered ;
coherence

proof end;

end;

registration

let X be set ;
let Y be integer-membered set ;
cluster PFuncs X,Y -> integer-functions-membered ;
coherence

proof end;

end;

registration

let X be set ;
let Y be natural-membered set ;
cluster PFuncs X,Y -> natural-functions-membered ;
coherence

proof end;

end;

registration

let X be set ;
let Y be complex-membered set ;
cluster Funcs X,Y -> complex-functions-membered ;
coherence

proof end;

end;

registration

let X be set ;
let Y be ext-real-membered set ;
cluster Funcs X,Y -> ext-real-functions-membered ;
coherence

proof end;

end;

registration

let X be set ;
let Y be real-membered set ;
cluster Funcs X,Y -> real-functions-membered ;
coherence

proof end;

end;

registration

let X be set ;
let Y be rational-membered set ;
cluster Funcs X,Y -> rational-functions-membered ;
coherence

proof end;

end;

registration

let X be set ;
let Y be integer-membered set ;
cluster Funcs X,Y -> integer-functions-membered ;
coherence

proof end;

end;

registration

let X be set ;
let Y be natural-membered set ;
cluster Funcs X,Y -> natural-functions-membered ;
coherence

proof end;

end;

definition

let R be Relation;
attr R is complex-functions-valued means :Def19: :: VALUED_2:def 19
rng R is complex-functions-membered;
attr R is ext-real-functions-valued means :Def20: :: VALUED_2:def 20
rng R is ext-real-functions-membered;
attr R is real-functions-valued means :Def21: :: VALUED_2:def 21
rng R is real-functions-membered;
attr R is rational-functions-valued means :Def22: :: VALUED_2:def 22
rng R is rational-functions-membered;
attr R is integer-functions-valued means :Def23: :: VALUED_2:def 23
rng R is integer-functions-membered;
attr R is natural-functions-valued means :Def24: :: VALUED_2:def 24
rng R is natural-functions-membered;

end;

:: deftheorem Def19 defines complex-functions-valued VALUED_2:def 19 :

:: deftheorem Def20 defines ext-real-functions-valued VALUED_2:def 20 :

:: deftheorem Def21 defines real-functions-valued VALUED_2:def 21 :

:: deftheorem Def22 defines rational-functions-valued VALUED_2:def 22 :

:: deftheorem Def23 defines integer-functions-valued VALUED_2:def 23 :

:: deftheorem Def24 defines natural-functions-valued VALUED_2:def 24 :

definition

let f be Function;
redefine attr f is complex-functions-valued means :: VALUED_2:def 25
for x being set st x in dom f holds
f . x is complex-valued Function;
compatibility

proof end;

redefine attr f is ext-real-functions-valued means :: VALUED_2:def 26
for x being set st x in dom f holds
f . x is ext-real-valued Function;
compatibility

proof end;

redefine attr f is real-functions-valued means :: VALUED_2:def 27
for x being set st x in dom f holds
f . x is real-valued Function;
compatibility

proof end;

redefine attr f is rational-functions-valued means :: VALUED_2:def 28
for x being set st x in dom f holds
f . x is rational-valued Function;
compatibility

proof end;

redefine attr f is integer-functions-valued means :: VALUED_2:def 29
for x being set st x in dom f holds
f . x is integer-valued Function;
compatibility

proof end;

redefine attr f is natural-functions-valued means :: VALUED_2:def 30
for x being set st x in dom f holds
f . x is natural-valued Function;
compatibility

proof end;

end;

:: deftheorem defines complex-functions-valued VALUED_2:def 25 :

:: deftheorem defines ext-real-functions-valued VALUED_2:def 26 :

:: deftheorem defines real-functions-valued VALUED_2:def 27 :

:: deftheorem defines rational-functions-valued VALUED_2:def 28 :

:: deftheorem defines integer-functions-valued VALUED_2:def 29 :

:: deftheorem defines natural-functions-valued VALUED_2:def 30 :

registration

cluster natural-functions-valued -> integer-functions-valued set ;
coherence

proof end;

cluster integer-functions-valued -> rational-functions-valued set ;
coherence

proof end;

cluster rational-functions-valued -> real-functions-valued set ;
coherence

proof end;

cluster real-functions-valued -> ext-real-functions-valued set ;
coherence

proof end;

cluster real-functions-valued -> complex-functions-valued set ;
coherence

proof end;

end;

registration

cluster empty -> natural-functions-valued set ;
coherence

proof end;

end;

registration

let R be complex-functions-valued Relation;
cluster rng R -> complex-functions-membered ;
coherence by Def19;

end;

registration

let R be ext-real-functions-valued Relation;
cluster rng R -> ext-real-functions-membered ;
coherence by Def20;

end;

registration

let R be real-functions-valued Relation;
cluster rng R -> real-functions-membered ;
coherence by Def21;

end;

registration

let R be rational-functions-valued Relation;
cluster rng R -> rational-functions-membered ;
coherence by Def22;

end;

registration

let R be integer-functions-valued Relation;
cluster rng R -> integer-functions-membered ;
coherence by Def23;

end;

registration

let R be natural-functions-valued Relation;
cluster rng R -> natural-functions-membered ;
coherence by Def24;

end;

registration

let X be set ;
let Y be complex-functions-membered set ;
cluster -> complex-functions-valued Relation of X,Y;
coherence

proof end;

end;

registration

let X be set ;
let Y be ext-real-functions-membered set ;
cluster -> ext-real-functions-valued Relation of X,Y;
coherence

proof end;

end;

registration

let X be set ;
let Y be real-functions-membered set ;
cluster -> real-functions-valued Relation of X,Y;
coherence

proof end;

end;

registration

let X be set ;
let Y be rational-functions-membered set ;
cluster -> rational-functions-valued Relation of X,Y;
coherence

proof end;

end;

registration

let X be set ;
let Y be integer-functions-membered set ;
cluster -> integer-functions-valued Relation of X,Y;
coherence

proof end;

end;

registration

let X be set ;
let Y be natural-functions-membered set ;
cluster -> natural-functions-valued Relation of X,Y;
coherence

proof end;

end;

registration

let f be complex-functions-valued Function;
let x be set ;
cluster f . x -> Relation-like Function-like ;
coherence

proof end;

end;

registration

let f be ext-real-functions-valued Function;
let x be set ;
cluster f . x -> Relation-like Function-like ;
coherence

proof end;

end;

registration

let f be complex-functions-valued Function;
let x be set ;
cluster f . x -> complex-valued ;
coherence

proof end;

end;

registration

let f be ext-real-functions-valued Function;
let x be set ;
cluster f . x -> ext-real-valued ;
coherence

proof end;

end;

registration

let f be real-functions-valued Function;
let x be set ;
cluster f . x -> real-valued ;
coherence

proof end;

end;

registration

let f be rational-functions-valued Function;
let x be set ;
cluster f . x -> rational-valued ;
coherence

proof end;

end;

registration

let f be integer-functions-valued Function;
let x be set ;
cluster f . x -> integer-valued ;
coherence

proof end;

end;

registration

let f be natural-functions-valued Function;
let x be set ;
cluster f . x -> natural-valued ;
coherence

proof end;

end;

theorem Tha: :: VALUED_2:8

for c1, c2 being complex number
for g being complex-valued Function st g <> {} & g + c1 = g + c2 holds
c1 = c2

proof end;

theorem Thb: :: VALUED_2:9

for c1, c2 being complex number
for g being complex-valued Function st g <> {} & g - c1 = g - c2 holds
c1 = c2

proof end;

theorem Thc: :: VALUED_2:10

for c1, c2 being complex number
for g being complex-valued Function st g <> {} & g is non-empty & g (#) c1 = g (#) c2 holds
c1 = c2

proof end;

theorem Th81: :: VALUED_2:11

for c being complex number
for g being complex-valued Function holds - (g + c) = (- g) - c

proof end;

theorem Th82: :: VALUED_2:12

for c being complex number
for g being complex-valued Function holds - (g - c) = (- g) + c

proof end;

theorem Th8: :: VALUED_2:13

for c1, c2 being complex number
for g being complex-valued Function holds (g + c1) + c2 = g + (c1 + c2)

proof end;

theorem Th9: :: VALUED_2:14

for c1, c2 being complex number
for g being complex-valued Function holds (g + c1) - c2 = g + (c1 - c2)

proof end;

theorem Th10: :: VALUED_2:15

for c1, c2 being complex number
for g being complex-valued Function holds (g - c1) + c2 = g - (c1 - c2)

proof end;

theorem Th11: :: VALUED_2:16

for c1, c2 being complex number
for g being complex-valued Function holds (g - c1) - c2 = g - (c1 + c2)

proof end;

theorem Th12: :: VALUED_2:17

for c1, c2 being complex number
for g being complex-valued Function holds (g (#) c1) (#) c2 = g (#) (c1 * c2)

proof end;

theorem Th13a: :: VALUED_2:18

for g, h being complex-valued Function holds - (g + h) = (- g) - h

proof end;

theorem Th13: :: VALUED_2:19

for g, h being complex-valued Function holds g - h = - (h - g)

proof end;

theorem Th14b: :: VALUED_2:20

for g, h, k being complex-valued Function holds (g (#) h) /" k = g (#) (h /" k)

proof end;

theorem Th14a: :: VALUED_2:21

for g, h, k being complex-valued Function holds (g /" h) (#) k = (g (#) k) /" h

proof end;

theorem Th14: :: VALUED_2:22

for g, h, k being complex-valued Function holds (g /" h) /" k = g /" (h (#) k)

proof end;

theorem Th17: :: VALUED_2:23

for c being complex number
for g being complex-valued Function holds c (#) (- g) = (- c) (#) g

proof end;

theorem Th18: :: VALUED_2:24

for c being complex number
for g being complex-valued Function holds c (#) (- g) = - (c (#) g)

proof end;

theorem Th19: :: VALUED_2:25

for c being complex number
for g being complex-valued Function holds (- c) (#) g = - (c (#) g)

proof end;

theorem Th13b: :: VALUED_2:26

for g, h being complex-valued Function holds - (g (#) h) = (- g) (#) h

proof end;

theorem :: VALUED_2:27

for g, h being complex-valued Function holds - (g /" h) = (- g) /" h

proof end;

theorem Th13d: :: VALUED_2:28

for g, h being complex-valued Function holds - (g /" h) = g /" (- h)

proof end;

definition

let f be complex-valued Function;
let c be complex number ;
func f (/) c -> Function equals :: VALUED_2:def 31
(1 / c) (#) f;
coherence ;

end;

:: deftheorem defines (/) VALUED_2:def 31 :

registration

let f be complex-valued Function;
let c be complex number ;
cluster f (/) c -> complex-valued ;
coherence ;

end;

registration

let f be real-valued Function;
let r be real number ;
cluster f (/) r -> real-valued ;
coherence ;

end;

registration

let f be complex-valued FinSequence;
let c be complex number ;
cluster f (/) c -> FinSequence-like ;
coherence ;

end;

theorem :: VALUED_2:29

for c being complex number
for g being complex-valued Function holds dom (g (/) c) = dom g by VALUED_1:def 5;

theorem :: VALUED_2:30

for x being set
for c being complex number
for g being complex-valued Function holds (g (/) c) . x = (g . x) / c by VALUED_1:6;

theorem Th20: :: VALUED_2:31

for c being complex number
for g being complex-valued Function holds (- g) (/) c = - (g (/) c)

proof end;

theorem Th21: :: VALUED_2:32

for c being complex number
for g being complex-valued Function holds g (/) (- c) = - (g (/) c)

proof end;

theorem :: VALUED_2:33

for c being complex number
for g being complex-valued Function holds g (/) (- c) = (- g) (/) c

proof end;

theorem Thd: :: VALUED_2:34

for c1, c2 being complex number
for g being complex-valued Function st g <> {} & g is non-empty & g (/) c1 = g (/) c2 holds
c1 = c2

proof end;

theorem :: VALUED_2:35

for c1, c2 being complex number
for g being complex-valued Function holds (g (#) c1) (/) c2 = g (#) (c1 / c2)

proof end;

theorem :: VALUED_2:36

for c1, c2 being complex number
for g being complex-valued Function holds (g (/) c1) (#) c2 = (g (#) c2) (/) c1

proof end;

theorem :: VALUED_2:37

for c1, c2 being complex number
for g being complex-valued Function holds (g (/) c1) (/) c2 = g (/) (c1 * c2)

proof end;

theorem :: VALUED_2:38

for c being complex number
for g, h being complex-valued Function holds (g + h) (/) c = (g (/) c) + (h (/) c)

proof end;

theorem :: VALUED_2:39

for c being complex number
for g, h being complex-valued Function holds (g - h) (/) c = (g (/) c) - (h (/) c)

proof end;

theorem :: VALUED_2:40

for c being complex number
for g, h being complex-valued Function holds (g (#) h) (/) c = g (#) (h (/) c)

proof end;

theorem :: VALUED_2:41

for c being complex number
for g, h being complex-valued Function holds (g /" h) (/) c = g /" (h (#) c)

proof end;

definition

let X be set ;
let Y be complex-functions-membered set ;
let f be PartFunc of X,Y;
deffunc H₁( set ) -> set = - (f . $1);
func <-> f -> Function means :Def32: :: VALUED_2:def 32
( dom it = dom f & ( for x being set st x in dom it holds
it . x = - (f . x) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def32 defines <-> VALUED_2:def 32 :

registration

let X be set ;
let Y be complex-functions-membered set ;
let f be PartFunc of X,Y;
cluster <-> f -> complex-functions-valued ;
coherence

proof end;

end;

registration

let X be set ;
let Y be real-functions-membered set ;
let f be PartFunc of X,Y;
cluster <-> f -> real-functions-valued ;
coherence

proof end;

end;

registration

let X be set ;
let Y be rational-functions-membered set ;
let f be PartFunc of X,Y;
cluster <-> f -> rational-functions-valued ;
coherence

proof end;

end;

registration

let X be set ;
let Y be integer-functions-membered set ;
let f be PartFunc of X,Y;
cluster <-> f -> integer-functions-valued ;
coherence

proof end;

end;

registration

let Y be complex-functions-membered set ;
let f be FinSequence of Y;
cluster <-> f -> FinSequence-like ;
coherence

proof end;

end;

theorem :: VALUED_2:42

for X, X1 being set
for Y, Y1 being complex-functions-membered set
for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1 st f1 = <-> f holds
<-> f1 = f

proof end;

theorem :: VALUED_2:43

for X1, X2 being set
for Y1, Y2 being complex-functions-membered set
for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2 st <-> f1 = <-> f2 holds
f1 = f2

proof end;

definition

let X be complex-functions-membered set ;
let Y be set ;
let f be PartFunc of X,Y;
defpred S₁[ set , set ] means ex a being complex-valued Function st
( $1 = a & $2 = f . (- a) );
func f (-) -> Function means :: VALUED_2:def 33
( dom it = dom f & ( for x being complex-valued Function st x in dom it holds
it . x = f . (- x) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines (-) VALUED_2:def 33 :

definition

let X be set ;
let Y be complex-functions-membered set ;
let f be PartFunc of X,Y;
deffunc H₁( set ) -> set = (f . $1) " ;
func </> f -> Function means :Def34: :: VALUED_2:def 34
( dom it = dom f & ( for x being set st x in dom it holds
it . x = (f . x) " ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def34 defines </> VALUED_2:def 34 :

registration

let X be set ;
let Y be complex-functions-membered set ;
let f be PartFunc of X,Y;
cluster </> f -> complex-functions-valued ;
coherence

proof end;

end;

registration

let X be set ;
let Y be real-functions-membered set ;
let f be PartFunc of X,Y;
cluster </> f -> real-functions-valued ;
coherence

proof end;

end;

registration

let X be set ;
let Y be rational-functions-membered set ;
let f be PartFunc of X,Y;
cluster </> f -> rational-functions-valued ;
coherence

proof end;

end;

registration

let Y be complex-functions-membered set ;
let f be FinSequence of Y;
cluster </> f -> FinSequence-like ;
coherence

proof end;

end;

theorem :: VALUED_2:44

for X, X1 being set
for Y, Y1 being complex-functions-membered set
for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1 st f1 = </> f holds
</> f1 = f

proof end;

definition

let X be set ;
let Y be complex-functions-membered set ;
let f be PartFunc of X,Y;
deffunc H₁( set ) -> set = abs (f . $1);
func abs f -> Function means :Def35: :: VALUED_2:def 35
( dom it = dom f & ( for x being set st x in dom it holds
it . x = abs (f . x) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def35 defines abs VALUED_2:def 35 :

registration

let X be set ;
let Y be complex-functions-membered set ;
let f be PartFunc of X,Y;
cluster abs f -> complex-functions-valued ;
coherence

proof end;

end;

registration

let X be set ;
let Y be real-functions-membered set ;
let f be PartFunc of X,Y;
cluster abs f -> real-functions-valued ;
coherence

proof end;

end;

registration

let X be set ;
let Y be rational-functions-membered set ;
let f be PartFunc of X,Y;
cluster abs f -> rational-functions-valued ;
coherence

proof end;

end;

registration

let X be set ;
let Y be integer-functions-membered set ;
let f be PartFunc of X,Y;
cluster abs f -> natural-functions-valued ;
coherence

proof end;

end;

registration

let Y be complex-functions-membered set ;
let f be FinSequence of Y;
cluster abs f -> FinSequence-like ;
coherence

proof end;

end;

theorem :: VALUED_2:45

for X, X1 being set
for Y, Y1 being complex-functions-membered set
for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1 st f1 = abs f holds
abs f1 = abs f

proof end;

definition

let X be set ;
let Y be complex-functions-membered set ;
let f be PartFunc of X,Y;
let c be complex number ;
deffunc H₁( set ) -> set = c + (f . $1);
func f [+] c -> Function means :Def36: :: VALUED_2:def 36
( dom it = dom f & ( for x being set st x in dom it holds
it . x = c + (f . x) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def36 defines [+] VALUED_2:def 36 :

registration

let X be set ;
let Y be complex-functions-membered set ;
let f be PartFunc of X,Y;
let c be complex number ;
cluster f [+] c -> complex-functions-valued ;
coherence

proof end;

end;

registration

let X be set ;
let Y be real-functions-membered set ;
let f be PartFunc of X,Y;
let c be real number ;
cluster f [+] c -> real-functions-valued ;
coherence

proof end;

end;

registration

let X be set ;
let Y be rational-functions-membered set ;
let f be PartFunc of X,Y;
let c be rational number ;
cluster f [+] c -> rational-functions-valued ;
coherence

proof end;

end;

registration

let X be set ;
let Y be integer-functions-membered set ;
let f be PartFunc of X,Y;
let c be integer number ;
cluster f [+] c -> integer-functions-valued ;
coherence

proof end;

end;

registration

let X be set ;
let Y be natural-functions-membered set ;
let f be PartFunc of X,Y;
let c be natural number ;
cluster f [+] c -> natural-functions-valued ;
coherence

proof end;

end;

theorem :: VALUED_2:46

for X, X1 being set
for Y, Y1 being complex-functions-membered set
for c1, c2 being complex number
for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1 st f1 = f [+] c1 holds
f1 [+] c2 = f [+] (c1 + c2)

proof end;

theorem :: VALUED_2:47

for X being set
for Y being complex-functions-membered set
for c1, c2 being complex number
for f being PartFunc of X,Y st f <> {} & f is non-empty & f [+] c1 = f [+] c2 holds
c1 = c2

proof end;

definition

let X be set ;
let Y be complex-functions-membered set ;
let f be PartFunc of X,Y;
let c be complex number ;
func f [-] c -> Function equals :: VALUED_2:def 37
f [+] (- c);
coherence ;

end;

:: deftheorem defines [-] VALUED_2:def 37 :

theorem :: VALUED_2:48

for X being set
for Y being complex-functions-membered set
for c being complex number
for f being PartFunc of X,Y holds dom (f [-] c) = dom f by Def36;

theorem :: VALUED_2:49

for X, x being set
for Y being complex-functions-membered set
for c being complex number
for f being PartFunc of X,Y st x in dom (f [-] c) holds
(f [-] c) . x = (f . x) - c by Def36;

registration

let X be set ;
let Y be complex-functions-membered set ;
let f be PartFunc of X,Y;
let c be complex number ;
cluster f [-] c -> complex-functions-valued ;
coherence ;

end;

registration

let X be set ;
let Y be real-functions-membered set ;
let f be PartFunc of X,Y;
let c be real number ;
cluster f [-] c -> real-functions-valued ;
coherence ;

end;

registration

let X be set ;
let Y be rational-functions-membered set ;
let f be PartFunc of X,Y;
let c be rational number ;
cluster f [-] c -> rational-functions-valued ;
coherence ;

end;

registration

let X be set ;
let Y be integer-functions-membered set ;
let f be PartFunc of X,Y;
let c be integer number ;
cluster f [-] c -> integer-functions-valued ;
coherence ;

end;

theorem :: VALUED_2:50

for X being set
for Y being complex-functions-membered set
for c1, c2 being complex number
for f being PartFunc of X,Y st f <> {} & f is non-empty & f [-] c1 = f [-] c2 holds
c1 = c2

proof end;

theorem :: VALUED_2:51

for X, X1 being set
for Y, Y1 being complex-functions-membered set
for c1, c2 being complex number
for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1 st f1 = f [+] c1 holds
f1 [-] c2 = f [+] (c1 - c2)

proof end;

theorem :: VALUED_2:52

for X, X1 being set
for Y, Y1 being complex-functions-membered set
for c1, c2 being complex number
for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1 st f1 = f [-] c1 holds
f1 [+] c2 = f [-] (c1 - c2)

proof end;

theorem :: VALUED_2:53

for X, X1 being set
for Y, Y1 being complex-functions-membered set
for c1, c2 being complex number
for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1 st f1 = f [-] c1 holds
f1 [-] c2 = f [-] (c1 + c2)

proof end;

definition

let X be set ;
let Y be complex-functions-membered set ;
let f be PartFunc of X,Y;
let c be complex number ;
deffunc H₁( set ) -> set = c (#) (f . $1);
func f [#] c -> Function means :Def38: :: VALUED_2:def 38
( dom it = dom f & ( for x being set st x in dom it holds
it . x = c (#) (f . x) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def38 defines [#] VALUED_2:def 38 :

registration

let X be set ;
let Y be complex-functions-membered set ;
let f be PartFunc of X,Y;
let c be complex number ;
cluster f [#] c -> complex-functions-valued ;
coherence

proof end;

end;

registration

let X be set ;
let Y be real-functions-membered set ;
let f be PartFunc of X,Y;
let c be real number ;
cluster f [#] c -> real-functions-valued ;
coherence

proof end;

end;

registration

let X be set ;
let Y be rational-functions-membered set ;
let f be PartFunc of X,Y;
let c be rational number ;
cluster f [#] c -> rational-functions-valued ;
coherence

proof end;

end;

registration

let X be set ;
let Y be integer-functions-membered set ;
let f be PartFunc of X,Y;
let c be integer number ;
cluster f [#] c -> integer-functions-valued ;
coherence

proof end;

end;

registration

let X be set ;
let Y be natural-functions-membered set ;
let f be PartFunc of X,Y;
let c be natural number ;
cluster f [#] c -> natural-functions-valued ;
coherence

proof end;

end;

theorem :: VALUED_2:54

for X, X1 being set
for Y, Y1 being complex-functions-membered set
for c1, c2 being complex number
for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1 st f1 = f [#] c1 holds
f1 [#] c2 = f [#] (c1 * c2)

proof end;

theorem :: VALUED_2:55

for X being set
for Y being complex-functions-membered set
for c1, c2 being complex number
for f being PartFunc of X,Y st f <> {} & f is non-empty & ( for x being set st x in dom f holds
f . x is non-empty ) & f [#] c1 = f [#] c2 holds
c1 = c2

proof end;

definition

let X be set ;
let Y be complex-functions-membered set ;
let f be PartFunc of X,Y;
let c be complex number ;
func f [/] c -> Function equals :: VALUED_2:def 39
f [#] (c " );
coherence ;

end;

:: deftheorem defines [/] VALUED_2:def 39 :

theorem :: VALUED_2:56

for X being set
for Y being complex-functions-membered set
for c being complex number
for f being PartFunc of X,Y holds dom (f [/] c) = dom f by Def38;

theorem :: VALUED_2:57

for X, x being set
for Y being complex-functions-membered set
for c being complex number
for f being PartFunc of X,Y st x in dom (f [/] c) holds
(f [/] c) . x = (c " ) (#) (f . x) by Def38;

registration

let X be set ;
let Y be complex-functions-membered set ;
let f be PartFunc of X,Y;
let c be complex number ;
cluster f [/] c -> complex-functions-valued ;
coherence ;

end;

registration

let X be set ;
let Y be real-functions-membered set ;
let f be PartFunc of X,Y;
let c be real number ;
cluster f [/] c -> real-functions-valued ;
coherence ;

end;

registration

let X be set ;
let Y be rational-functions-membered set ;
let f be PartFunc of X,Y;
let c be rational number ;
cluster f [/] c -> rational-functions-valued ;
coherence ;

end;

theorem :: VALUED_2:58

for X, X1 being set
for Y, Y1 being complex-functions-membered set
for c1, c2 being complex number
for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1 st f1 = f [/] c1 holds
f1 [/] c2 = f [/] (c1 * c2)

proof end;

theorem :: VALUED_2:59

proof end;

definition

let X be set ;
let Y be complex-functions-membered set ;
let f be PartFunc of X,Y;
let g be complex-valued Function;
deffunc H₁( set ) -> set = (f . $1) + (g . $1);
func f <+> g -> Function means :Def40: :: VALUED_2:def 40
( dom it = (dom f) /\ (dom g) & ( for x being set st x in dom it holds
it . x = (f . x) + (g . x) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def40 defines <+> VALUED_2:def 40 :

registration

let X be set ;
let Y be complex-functions-membered set ;
let f be PartFunc of X,Y;
let g be complex-valued Function;
cluster f <+> g -> complex-functions-valued ;
coherence

proof end;

end;

registration

let X be set ;
let Y be real-functions-membered set ;
let f be PartFunc of X,Y;
let g be real-valued Function;
cluster f <+> g -> real-functions-valued ;
coherence

proof end;

end;

registration

let X be set ;
let Y be rational-functions-membered set ;
let f be PartFunc of X,Y;
let g be rational-valued Function;
cluster f <+> g -> rational-functions-valued ;
coherence

proof end;

end;

registration

let X be set ;
let Y be integer-functions-membered set ;
let f be PartFunc of X,Y;
let g be integer-valued Function;
cluster f <+> g -> integer-functions-valued ;
coherence

proof end;

end;

registration

let X be set ;
let Y be natural-functions-membered set ;
let f be PartFunc of X,Y;
let g be natural-valued Function;
cluster f <+> g -> natural-functions-valued ;
coherence

proof end;

end;

theorem :: VALUED_2:60

for X, X1 being set
for Y, Y1 being complex-functions-membered set
for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1
for g, h being complex-valued Function st f1 = f <+> g holds
f1 <+> h = f <+> (g + h)

proof end;

theorem :: VALUED_2:61

for X, X1, X2 being set
for Y, Y1, Y2 being complex-functions-membered set
for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2
for g being complex-valued Function st f1 = f <+> g & f2 = <-> f holds
<-> f1 = f2 <+> (- g)

proof end;

definition

let X be set ;
let Y be complex-functions-membered set ;
let f be PartFunc of X,Y;
let g be complex-valued Function;
func f <-> g -> Function equals :: VALUED_2:def 41
f <+> (- g);
coherence ;

end;

:: deftheorem defines <-> VALUED_2:def 41 :

theorem Th35: :: VALUED_2:62

for X being set
for Y being complex-functions-membered set
for f being PartFunc of X,Y
for g being complex-valued Function holds dom (f <-> g) = (dom f) /\ (dom g)

proof end;

theorem Th36: :: VALUED_2:63

for X, x being set
for Y being complex-functions-membered set
for f being PartFunc of X,Y
for g being complex-valued Function st x in dom (f <-> g) holds
(f <-> g) . x = (f . x) - (g . x)

proof end;

registration

let X be set ;
let Y be complex-functions-membered set ;
let f be PartFunc of X,Y;
let g be complex-valued Function;
cluster f <-> g -> complex-functions-valued ;
coherence ;

end;

registration

let X be set ;
let Y be real-functions-membered set ;
let f be PartFunc of X,Y;
let g be real-valued Function;
cluster f <-> g -> real-functions-valued ;
coherence ;

end;

registration

let X be set ;
let Y be rational-functions-membered set ;
let f be PartFunc of X,Y;
let g be rational-valued Function;
cluster f <-> g -> rational-functions-valued ;
coherence ;

end;

registration

let X be set ;
let Y be integer-functions-membered set ;
let f be PartFunc of X,Y;
let g be integer-valued Function;
cluster f <-> g -> integer-functions-valued ;
coherence ;

end;

theorem :: VALUED_2:64

for X being set
for Y being complex-functions-membered set
for f being PartFunc of X,Y
for g being complex-valued Function holds f <-> (- g) = f <+> g ;

theorem :: VALUED_2:65

proof end;

theorem :: VALUED_2:66

proof end;

theorem :: VALUED_2:67

for X, X1 being set
for Y, Y1 being complex-functions-membered set
for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1
for g, h being complex-valued Function st f1 = f <-> g holds
f1 <+> h = f <-> (g - h)

proof end;

theorem :: VALUED_2:68

proof end;

definition

let X be set ;
let Y be complex-functions-membered set ;
let f be PartFunc of X,Y;
let g be complex-valued Function;
deffunc H₁( set ) -> set = (f . $1) (#) (g . $1);
func f <#> g -> Function means :Def42: :: VALUED_2:def 42
( dom it = (dom f) /\ (dom g) & ( for x being set st x in dom it holds
it . x = (f . x) (#) (g . x) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def42 defines <#> VALUED_2:def 42 :

registration

let X be set ;
let Y be complex-functions-membered set ;
let f be PartFunc of X,Y;
let g be complex-valued Function;
cluster f <#> g -> complex-functions-valued ;
coherence

proof end;

end;

registration

let X be set ;
let Y be real-functions-membered set ;
let f be PartFunc of X,Y;
let g be real-valued Function;
cluster f <#> g -> real-functions-valued ;
coherence

proof end;

end;

registration

let X be set ;
let Y be rational-functions-membered set ;
let f be PartFunc of X,Y;
let g be rational-valued Function;
cluster f <#> g -> rational-functions-valued ;
coherence

proof end;

end;

registration

let X be set ;
let Y be integer-functions-membered set ;
let f be PartFunc of X,Y;
let g be integer-valued Function;
cluster f <#> g -> integer-functions-valued ;
coherence

proof end;

end;

registration

let X be set ;
let Y be natural-functions-membered set ;
let f be PartFunc of X,Y;
let g be natural-valued Function;
cluster f <#> g -> natural-functions-valued ;
coherence

proof end;

end;

theorem :: VALUED_2:69

for X, X1 being set
for Y, Y1 being complex-functions-membered set
for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1
for g being complex-valued Function st f1 = <-> f holds
f <#> (- g) = f1 <#> g

proof end;

theorem :: VALUED_2:70

for X, X1 being set
for Y, Y1 being complex-functions-membered set
for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1
for g being complex-valued Function st f1 = f <#> g holds
f <#> (- g) = <-> f1

proof end;

theorem :: VALUED_2:71

for X, X1 being set
for Y, Y1 being complex-functions-membered set
for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1
for g, h being complex-valued Function st f1 = f <#> g holds
f1 <#> h = f <#> (g (#) h)

proof end;

definition

let X be set ;
let Y be complex-functions-membered set ;
let f be PartFunc of X,Y;
let g be complex-valued Function;
func f </> g -> Function equals :: VALUED_2:def 43
f <#> (g " );
coherence ;

end;

:: deftheorem defines </> VALUED_2:def 43 :

theorem Th100: :: VALUED_2:72

for X being set
for Y being complex-functions-membered set
for f being PartFunc of X,Y
for g being complex-valued Function holds dom (f </> g) = (dom f) /\ (dom g)

proof end;

theorem Th101: :: VALUED_2:73

for X, x being set
for Y being complex-functions-membered set
for f being PartFunc of X,Y
for g being complex-valued Function st x in dom (f </> g) holds
(f </> g) . x = (f . x) (/) (g . x)

proof end;

registration

let X be set ;
let Y be complex-functions-membered set ;
let f be PartFunc of X,Y;
let g be complex-valued Function;
cluster f </> g -> complex-functions-valued ;
coherence ;

end;

registration

let X be set ;
let Y be real-functions-membered set ;
let f be PartFunc of X,Y;
let g be real-valued Function;
cluster f </> g -> real-functions-valued ;
coherence ;

end;

registration

let X be set ;
let Y be rational-functions-membered set ;
let f be PartFunc of X,Y;
let g be rational-valued Function;
cluster f </> g -> rational-functions-valued ;
coherence ;

end;

theorem :: VALUED_2:74

proof end;

definition

let X1, X2 be set ;
let Y1, Y2 be complex-functions-membered set ;
let f be PartFunc of X1,Y1;
let g be PartFunc of X2,Y2;
deffunc H₁( set ) -> set = (f . $1) + (g . $1);
func f <++> g -> Function means :Def44: :: VALUED_2:def 44
( dom it = (dom f) /\ (dom g) & ( for x being set st x in dom it holds
it . x = (f . x) + (g . x) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def44 defines <++> VALUED_2:def 44 :

registration

let X1, X2 be set ;
let Y1, Y2 be complex-functions-membered set ;
let f be PartFunc of X1,Y1;
let g be PartFunc of X2,Y2;
cluster f <++> g -> complex-functions-valued ;
coherence

proof end;

end;

registration

let X1, X2 be set ;
let Y1, Y2 be real-functions-membered set ;
let f be PartFunc of X1,Y1;
let g be PartFunc of X2,Y2;
cluster f <++> g -> real-functions-valued ;
coherence

proof end;

end;

registration

let X1, X2 be set ;
let Y1, Y2 be rational-functions-membered set ;
let f be PartFunc of X1,Y1;
let g be PartFunc of X2,Y2;
cluster f <++> g -> rational-functions-valued ;
coherence

proof end;

end;

registration

let X1, X2 be set ;
let Y1, Y2 be integer-functions-membered set ;
let f be PartFunc of X1,Y1;
let g be PartFunc of X2,Y2;
cluster f <++> g -> integer-functions-valued ;
coherence

proof end;

end;

registration

let X1, X2 be set ;
let Y1, Y2 be natural-functions-membered set ;
let f be PartFunc of X1,Y1;
let g be PartFunc of X2,Y2;
cluster f <++> g -> natural-functions-valued ;
coherence

proof end;

end;

theorem Th43: :: VALUED_2:75

for X1, X2 being set
for Y1, Y2 being complex-functions-membered set
for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2 holds f1 <++> f2 = f2 <++> f1

proof end;

theorem :: VALUED_2:76

for X, X1, X2, X3, X4 being set
for Y, Y1, Y2, Y3, Y4 being complex-functions-membered set
for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2
for f3 being PartFunc of X3,Y3
for f4 being PartFunc of X4,Y4 st f3 = f <++> f1 & f4 = f1 <++> f2 holds
f3 <++> f2 = f <++> f4

proof end;

theorem :: VALUED_2:77

for X1, X2, X3, X4, X5 being set
for Y1, Y2, Y3, Y4, Y5 being complex-functions-membered set
for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2
for f3 being PartFunc of X3,Y3
for f4 being PartFunc of X4,Y4
for f5 being PartFunc of X5,Y5 st f3 = f1 <++> f2 & f4 = <-> f1 & f5 = <-> f2 holds
<-> f3 = f4 <++> f5

proof end;

definition

let X1, X2 be set ;
let Y1, Y2 be complex-functions-membered set ;
let f be PartFunc of X1,Y1;
let g be PartFunc of X2,Y2;
deffunc H₁( set ) -> set = (f . $1) - (g . $1);
func f <--> g -> Function means :Def45: :: VALUED_2:def 45
( dom it = (dom f) /\ (dom g) & ( for x being set st x in dom it holds
it . x = (f . x) - (g . x) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def45 defines <--> VALUED_2:def 45 :

registration

let X1, X2 be set ;
let Y1, Y2 be complex-functions-membered set ;
let f be PartFunc of X1,Y1;
let g be PartFunc of X2,Y2;
cluster f <--> g -> complex-functions-valued ;
coherence

proof end;

end;

registration

let X1, X2 be set ;
let Y1, Y2 be real-functions-membered set ;
let f be PartFunc of X1,Y1;
let g be PartFunc of X2,Y2;
cluster f <--> g -> real-functions-valued ;
coherence

proof end;

end;

registration

let X1, X2 be set ;
let Y1, Y2 be rational-functions-membered set ;
let f be PartFunc of X1,Y1;
let g be PartFunc of X2,Y2;
cluster f <--> g -> rational-functions-valued ;
coherence

proof end;

end;

registration

let X1, X2 be set ;
let Y1, Y2 be integer-functions-membered set ;
let f be PartFunc of X1,Y1;
let g be PartFunc of X2,Y2;
cluster f <--> g -> integer-functions-valued ;
coherence

proof end;

end;

theorem :: VALUED_2:78

for X, X1, X2 being set
for Y, Y1, Y2 being complex-functions-membered set
for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2 st f = f2 <--> f1 holds
f1 <--> f2 = <-> f

proof end;

theorem :: VALUED_2:79

for X1, X2, X3, X4 being set
for Y1, Y2, Y3, Y4 being complex-functions-membered set
for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2
for f3 being PartFunc of X3,Y3
for f4 being PartFunc of X4,Y4 st f3 = f1 <--> f2 & f4 = <-> f1 holds
<-> f3 = f4 <++> f2

proof end;

theorem :: VALUED_2:80

proof end;

theorem :: VALUED_2:81

for X, X1, X2, X3, X4 being set
for Y, Y1, Y2, Y3, Y4 being complex-functions-membered set
for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2
for f3 being PartFunc of X3,Y3
for f4 being PartFunc of X4,Y4 st f3 = f <--> f1 & f4 = f1 <--> f2 holds
f3 <++> f2 = f <--> f4

proof end;

theorem :: VALUED_2:82

for X, X1, X2, X3, X4 being set
for Y, Y1, Y2, Y3, Y4 being complex-functions-membered set
for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2
for f3 being PartFunc of X3,Y3
for f4 being PartFunc of X4,Y4 st f3 = f <--> f1 & f4 = f1 <++> f2 holds
f3 <--> f2 = f <--> f4

proof end;

theorem :: VALUED_2:83

for X, X1, X2, X3, X4 being set
for Y, Y1, Y2, Y3, Y4 being complex-functions-membered set
for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2
for f3 being PartFunc of X3,Y3
for f4 being PartFunc of X4,Y4 st f3 = f <--> f1 & f4 = f <--> f2 holds
f3 <--> f2 = f4 <--> f1

proof end;

definition

let X1, X2 be set ;
let Y1, Y2 be complex-functions-membered set ;
let f be PartFunc of X1,Y1;
let g be PartFunc of X2,Y2;
deffunc H₁( set ) -> set = (f . $1) (#) (g . $1);
func f <##> g -> Function means :Def46: :: VALUED_2:def 46
( dom it = (dom f) /\ (dom g) & ( for x being set st x in dom it holds
it . x = (f . x) (#) (g . x) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def46 defines <##> VALUED_2:def 46 :

registration

let X1, X2 be set ;
let Y1, Y2 be complex-functions-membered set ;
let f be PartFunc of X1,Y1;
let g be PartFunc of X2,Y2;
cluster f <##> g -> complex-functions-valued ;
coherence

proof end;

end;

registration

let X1, X2 be set ;
let Y1, Y2 be real-functions-membered set ;
let f be PartFunc of X1,Y1;
let g be PartFunc of X2,Y2;
cluster f <##> g -> real-functions-valued ;
coherence

proof end;

end;

registration

let X1, X2 be set ;
let Y1, Y2 be rational-functions-membered set ;
let f be PartFunc of X1,Y1;
let g be PartFunc of X2,Y2;
cluster f <##> g -> rational-functions-valued ;
coherence

proof end;

end;

registration

let X1, X2 be set ;
let Y1, Y2 be integer-functions-membered set ;
let f be PartFunc of X1,Y1;
let g be PartFunc of X2,Y2;
cluster f <##> g -> integer-functions-valued ;
coherence

proof end;

end;

registration

let X1, X2 be set ;
let Y1, Y2 be natural-functions-membered set ;
let f be PartFunc of X1,Y1;
let g be PartFunc of X2,Y2;
cluster f <##> g -> natural-functions-valued ;
coherence

proof end;

end;

theorem Th49: :: VALUED_2:84

for X1, X2 being set
for Y1, Y2 being complex-functions-membered set
for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2 holds f1 <##> f2 = f2 <##> f1

proof end;

theorem :: VALUED_2:85

for X, X1, X2, X3, X4 being set
for Y, Y1, Y2, Y3, Y4 being complex-functions-membered set
for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2
for f3 being PartFunc of X3,Y3
for f4 being PartFunc of X4,Y4 st f3 = f <##> f1 & f4 = f1 <##> f2 holds
f3 <##> f2 = f <##> f4

proof end;

theorem :: VALUED_2:86

proof end;

theorem :: VALUED_2:87

proof end;

theorem Th51: :: VALUED_2:88

for X, X1, X2, X3, X4, X5 being set
for Y, Y1, Y2, Y3, Y4, Y5 being complex-functions-membered set
for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2
for f3 being PartFunc of X3,Y3
for f4 being PartFunc of X4,Y4
for f5 being PartFunc of X5,Y5 st f3 = f <##> f1 & f4 = f <##> f2 & f5 = f1 <++> f2 holds
f <##> f5 = f3 <++> f4

proof end;

theorem :: VALUED_2:89

for X, X1, X2, X3, X4, X5 being set
for Y, Y1, Y2, Y3, Y4, Y5 being complex-functions-membered set
for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2
for f3 being PartFunc of X3,Y3
for f4 being PartFunc of X4,Y4
for f5 being PartFunc of X5,Y5 st f3 = f1 <##> f & f4 = f2 <##> f & f5 = f1 <++> f2 holds
f5 <##> f = f3 <++> f4

proof end;

theorem Th53: :: VALUED_2:90

proof end;

theorem :: VALUED_2:91

for X, X1, X2, X3, X4, X5 being set
for Y, Y1, Y2, Y3, Y4, Y5 being complex-functions-membered set
for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2
for f3 being PartFunc of X3,Y3
for f4 being PartFunc of X4,Y4
for f5 being PartFunc of X5,Y5 st f3 = f1 <##> f & f4 = f2 <##> f & f5 = f1 <--> f2 holds
f5 <##> f = f3 <--> f4

proof end;

definition

let X1, X2 be set ;
let Y1, Y2 be complex-functions-membered set ;
let f be PartFunc of X1,Y1;
let g be PartFunc of X2,Y2;
deffunc H₁( set ) -> set = (f . $1) /" (g . $1);
func f <//> g -> Function means :Def47: :: VALUED_2:def 47
( dom it = (dom f) /\ (dom g) & ( for x being set st x in dom it holds
it . x = (f . x) /" (g . x) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def47 defines <//> VALUED_2:def 47 :

registration

let X1, X2 be set ;
let Y1, Y2 be complex-functions-membered set ;
let f be PartFunc of X1,Y1;
let g be PartFunc of X2,Y2;
cluster f <//> g -> complex-functions-valued ;
coherence

proof end;

end;

registration

let X1, X2 be set ;
let Y1, Y2 be real-functions-membered set ;
let f be PartFunc of X1,Y1;
let g be PartFunc of X2,Y2;
cluster f <//> g -> real-functions-valued ;
coherence

proof end;

end;

registration

let X1, X2 be set ;
let Y1, Y2 be rational-functions-membered set ;
let f be PartFunc of X1,Y1;
let g be PartFunc of X2,Y2;
cluster f <//> g -> rational-functions-valued ;
coherence

proof end;

end;

theorem :: VALUED_2:92

proof end;

theorem :: VALUED_2:93

proof end;

theorem :: VALUED_2:94

for X, X1, X2, X3, X4 being set
for Y, Y1, Y2, Y3, Y4 being complex-functions-membered set
for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2
for f3 being PartFunc of X3,Y3
for f4 being PartFunc of X4,Y4 st f3 = f <##> f1 & f4 = f1 <//> f2 holds
f3 <//> f2 = f <##> f4

proof end;

theorem :: VALUED_2:95

for X, X1, X2, X3, X4 being set
for Y, Y1, Y2, Y3, Y4 being complex-functions-membered set
for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2
for f3 being PartFunc of X3,Y3
for f4 being PartFunc of X4,Y4 st f3 = f <//> f1 & f4 = f <##> f2 holds
f3 <##> f2 = f4 <//> f1

proof end;

theorem :: VALUED_2:96

for X, X1, X2, X3, X4 being set
for Y, Y1, Y2, Y3, Y4 being complex-functions-membered set
for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2
for f3 being PartFunc of X3,Y3
for f4 being PartFunc of X4,Y4 st f3 = f <//> f1 & f4 = f1 <##> f2 holds
f3 <//> f2 = f <//> f4

proof end;

theorem :: VALUED_2:97

for X, X1, X2, X3, X4, X5 being set
for Y, Y1, Y2, Y3, Y4, Y5 being complex-functions-membered set
for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2
for f3 being PartFunc of X3,Y3
for f4 being PartFunc of X4,Y4
for f5 being PartFunc of X5,Y5 st f3 = f1 <//> f & f4 = f2 <//> f & f5 = f1 <++> f2 holds
f5 <//> f = f3 <++> f4

proof end;

theorem :: VALUED_2:98

for X, X1, X2, X3, X4, X5 being set
for Y, Y1, Y2, Y3, Y4, Y5 being complex-functions-membered set
for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2
for f3 being PartFunc of X3,Y3
for f4 being PartFunc of X4,Y4
for f5 being PartFunc of X5,Y5 st f3 = f1 <//> f & f4 = f2 <//> f & f5 = f1 <--> f2 holds
f5 <//> f = f3 <--> f4

proof end;