VALUED_2: Arithmetic Operations on Functions from Sets into Functional Sets

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

begin

Lm1: now

let X1, X2, X3 be set ; :: thesis:
thus X1 /\ (X2 /\ X3) = ((X1 /\ X1) /\ X2) /\ X3 by XBOOLE_1:16
.= (X1 /\ (X1 /\ X2)) /\ X3 by XBOOLE_1:16
.= (X1 /\ X2) /\ (X1 /\ X3) by XBOOLE_1:16 ; :: thesis:

end;

definition

let Y be functional set ;
func DOMS Y -> set equals :: VALUED_2:def 1
union { (dom f) where f is Element of Y : verum } ;
coherence ;

end;

:: deftheorem defines DOMS VALUED_2:def 1 :

definition

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

end;

:: deftheorem Def2 defines complex-functions-membered VALUED_2:def 2 :

definition

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

end;

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

definition

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

end;

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

definition

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

end;

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

definition

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

end;

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

definition

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

end;

:: deftheorem Def7 defines natural-functions-membered VALUED_2:def 7 :

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;

set ff = the 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 K21(X);
coherence

proof end;

end;

registration

let X be ext-real-functions-membered set ;
cluster -> ext-real-functions-membered Element of K21(X);
coherence

proof end;

end;

registration

let X be real-functions-membered set ;
cluster -> real-functions-membered Element of K21(X);
coherence

proof end;

end;

registration

let X be rational-functions-membered set ;
cluster -> rational-functions-membered Element of K21(X);
coherence

proof end;

end;

registration

let X be integer-functions-membered set ;
cluster -> integer-functions-membered Element of K21(X);
coherence

proof end;

end;

registration

let X be natural-functions-membered set ;
cluster -> natural-functions-membered Element of K21(X);
coherence

proof end;

end;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines C_PFuncs VALUED_2:def 8 :

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines C_Funcs VALUED_2:def 9 :

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines E_PFuncs VALUED_2:def 10 :

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines E_Funcs VALUED_2:def 11 :

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines R_PFuncs VALUED_2:def 12 :

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines R_Funcs VALUED_2:def 13 :

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines Q_PFuncs VALUED_2:def 14 :

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines Q_Funcs VALUED_2:def 15 :

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def16 defines I_PFuncs VALUED_2:def 16 :

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def17 defines I_Funcs VALUED_2:def 17 :

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def18 defines N_PFuncs VALUED_2:def 18 :

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def19 defines N_Funcs VALUED_2:def 19 :

theorem Th1: :: VALUED_2:1

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

proof end;

theorem Th2: :: VALUED_2:2

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

proof end;

theorem Th3: :: VALUED_2:3

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

proof end;

theorem Th4: :: VALUED_2:4

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

proof end;

theorem Th5: :: VALUED_2:5

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

proof end;

theorem Th6: :: VALUED_2:6

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 :Def20: :: VALUED_2:def 20
rng R is complex-functions-membered ;
attr R is ext-real-functions-valued means :Def21: :: VALUED_2:def 21
rng R is ext-real-functions-membered ;
attr R is real-functions-valued means :Def22: :: VALUED_2:def 22
rng R is real-functions-membered ;
attr R is rational-functions-valued means :Def23: :: VALUED_2:def 23
rng R is rational-functions-membered ;
attr R is integer-functions-valued means :Def24: :: VALUED_2:def 24
rng R is integer-functions-membered ;
attr R is natural-functions-valued means :Def25: :: VALUED_2:def 25
rng R is natural-functions-membered ;

end;

:: deftheorem Def20 defines complex-functions-valued VALUED_2:def 20 :

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

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

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

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

:: deftheorem Def25 defines natural-functions-valued VALUED_2:def 25 :

definition

let f be Function;
redefine attr f is complex-functions-valued means :: VALUED_2:def 26
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 27
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 28
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 29
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 30
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 31
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 26 :

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

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

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

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

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

registration

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

end;

registration

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

proof end;

end;

registration

cluster Relation-like Function-like natural-functions-valued set ;
existence

proof end;

end;

registration

let R be complex-functions-valued Relation;
cluster proj2 R -> complex-functions-membered ;
coherence by Def20;

end;

registration

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

end;

registration

let R be real-functions-valued Relation;
cluster proj2 R -> real-functions-membered ;
coherence by Def22;

end;

registration

let R be rational-functions-valued Relation;
cluster proj2 R -> rational-functions-membered ;
coherence by Def23;

end;

registration

let R be integer-functions-valued Relation;
cluster proj2 R -> integer-functions-membered ;
coherence by Def24;

end;

registration

let R be natural-functions-valued Relation;
cluster proj2 R -> natural-functions-membered ;
coherence by Def25;

end;

registration

let X be set ;
let Y be complex-functions-membered set ;
cluster Function-like -> complex-functions-valued Element of K21(K22(X,Y));
coherence

proof end;

end;

registration

let X be set ;
let Y be ext-real-functions-membered set ;
cluster Function-like -> ext-real-functions-valued Element of K21(K22(X,Y));
coherence

proof end;

end;

registration

let X be set ;
let Y be real-functions-membered set ;
cluster Function-like -> real-functions-valued Element of K21(K22(X,Y));
coherence

proof end;

end;

registration

let X be set ;
let Y be rational-functions-membered set ;
cluster Function-like -> rational-functions-valued Element of K21(K22(X,Y));
coherence

proof end;

end;

registration

let X be set ;
let Y be integer-functions-membered set ;
cluster Function-like -> integer-functions-valued Element of K21(K22(X,Y));
coherence

proof end;

end;

registration

let X be set ;
let Y be natural-functions-membered set ;
cluster Function-like -> natural-functions-valued Element of K21(K22(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;

begin

theorem Th7: :: VALUED_2:7

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

proof end;

theorem Th8: :: 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 Th9: :: VALUED_2:9

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 Th10: :: VALUED_2:10

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

proof end;

theorem Th11: :: VALUED_2:11

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

proof end;

theorem Th12: :: VALUED_2:12

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

proof end;

theorem Th13: :: 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 Th14: :: 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 Th15: :: 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 Th16: :: 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 Th17: :: VALUED_2:17

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

proof end;

theorem Th18: :: VALUED_2:18

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

proof end;

theorem Th19: :: VALUED_2:19

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

proof end;

theorem Th20: :: VALUED_2:20

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

proof end;

theorem Th21: :: VALUED_2:21

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

proof end;

theorem Th22: :: VALUED_2:22

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

proof end;

theorem Th23: :: VALUED_2:23

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

proof end;

theorem Th24: :: VALUED_2:24

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

proof end;

theorem Th25: :: VALUED_2:25

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

proof end;

theorem :: VALUED_2:26

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

proof end;

theorem Th27: :: VALUED_2:27

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 32
(1 / c) (#) f;
coherence ;

end;

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

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 rational-valued Function;
let r be rational number ;
cluster f (/) r -> rational-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:28

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:29

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 Th30: :: VALUED_2:30

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

proof end;

theorem Th31: :: VALUED_2:31

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

proof end;

theorem :: VALUED_2:32

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

proof end;

theorem Th33: :: VALUED_2:33

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:34

for c1, c2 being complex number
for g being complex-valued Function holds (g (#) c1) (/) c2 = g (#) (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 (#) c2) (/) c1

proof end;

theorem :: VALUED_2:36

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

proof end;

theorem :: VALUED_2:37

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

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 :Def33: :: VALUED_2:def 33
( 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 Def33 defines <-> VALUED_2:def 33 :

definition

let X be set ;
let Y be complex-functions-membered set ;
let f be PartFunc of X,Y;
:: original: <->
redefine func <-> f -> PartFunc of X,(C_PFuncs (DOMS Y));
coherence

proof end;

end;

definition

let X be set ;
let Y be real-functions-membered set ;
let f be PartFunc of X,Y;
:: original: <->
redefine func <-> f -> PartFunc of X,(R_PFuncs (DOMS Y));
coherence

proof end;

end;

definition

let X be set ;
let Y be rational-functions-membered set ;
let f be PartFunc of X,Y;
:: original: <->
redefine func <-> f -> PartFunc of X,(Q_PFuncs (DOMS Y));
coherence

proof end;

end;

definition

let X be set ;
let Y be integer-functions-membered set ;
let f be PartFunc of X,Y;
:: original: <->
redefine func <-> f -> PartFunc of X,(I_PFuncs (DOMS Y));
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:41

for X being set
for Y being complex-functions-membered set
for f being PartFunc of X,Y holds <-> (<-> f) = f

proof end;

theorem :: VALUED_2:42

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 34
( 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 34 :

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 :Def35: :: VALUED_2:def 35
( 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 Def35 defines </> VALUED_2:def 35 :

definition

let X be set ;
let Y be complex-functions-membered set ;
let f be PartFunc of X,Y;
:: original: </>
redefine func </> f -> PartFunc of X,(C_PFuncs (DOMS Y));
coherence

proof end;

end;

definition

let X be set ;
let Y be real-functions-membered set ;
let f be PartFunc of X,Y;
:: original: </>
redefine func </> f -> PartFunc of X,(R_PFuncs (DOMS Y));
coherence

proof end;

end;

definition

let X be set ;
let Y be rational-functions-membered set ;
let f be PartFunc of X,Y;
:: original: </>
redefine func </> f -> PartFunc of X,(Q_PFuncs (DOMS Y));
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:43

for X being set
for Y being complex-functions-membered set
for f being PartFunc of X,Y holds </> (</> f) = 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 :Def36: :: VALUED_2:def 36
( 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 Def36 defines abs VALUED_2:def 36 :

definition

let X be set ;
let Y be complex-functions-membered set ;
let f be PartFunc of X,Y;
:: original: abs
redefine func abs f -> PartFunc of X,(C_PFuncs (DOMS Y));
coherence

proof end;

end;

definition

let X be set ;
let Y be real-functions-membered set ;
let f be PartFunc of X,Y;
:: original: abs
redefine func abs f -> PartFunc of X,(R_PFuncs (DOMS Y));
coherence

proof end;

end;

definition

let X be set ;
let Y be rational-functions-membered set ;
let f be PartFunc of X,Y;
:: original: abs
redefine func abs f -> PartFunc of X,(Q_PFuncs (DOMS Y));
coherence

proof end;

end;

definition

let X be set ;
let Y be integer-functions-membered set ;
let f be PartFunc of X,Y;
:: original: abs
redefine func abs f -> PartFunc of X,(N_PFuncs (DOMS Y));
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:44

for X being set
for Y being complex-functions-membered set
for f being PartFunc of X,Y holds abs (abs f) = 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 :Def37: :: VALUED_2:def 37
( 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 Def37 defines [+] VALUED_2:def 37 :

definition

let X be set ;
let Y be complex-functions-membered set ;
let f be PartFunc of X,Y;
let c be complex number ;
:: original: [+]
redefine func f [+] c -> PartFunc of X,(C_PFuncs (DOMS Y));
coherence

proof end;

end;

definition

let X be set ;
let Y be real-functions-membered set ;
let f be PartFunc of X,Y;
let c be real number ;
:: original: [+]
redefine func f [+] c -> PartFunc of X,(R_PFuncs (DOMS Y));
coherence

proof end;

end;

definition

let X be set ;
let Y be rational-functions-membered set ;
let f be PartFunc of X,Y;
let c be rational number ;
:: original: [+]
redefine func f [+] c -> PartFunc of X,(Q_PFuncs (DOMS Y));
coherence

proof end;

end;

definition

let X be set ;
let Y be integer-functions-membered set ;
let f be PartFunc of X,Y;
let c be integer number ;
:: original: [+]
redefine func f [+] c -> PartFunc of X,(I_PFuncs (DOMS Y));
coherence

proof end;

end;

definition

let X be set ;
let Y be natural-functions-membered set ;
let f be PartFunc of X,Y;
let c be natural number ;
:: original: [+]
redefine func f [+] c -> PartFunc of X,(N_PFuncs (DOMS Y));
coherence

proof end;

end;

theorem :: VALUED_2:45

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

proof end;

theorem :: VALUED_2:46

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 38
f [+] (- c);
coherence ;

end;

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

theorem :: VALUED_2:47

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

theorem :: VALUED_2:48

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

definition

let X be set ;
let Y be complex-functions-membered set ;
let f be PartFunc of X,Y;
let c be complex number ;
:: original: [-]
redefine func f [-] c -> PartFunc of X,(C_PFuncs (DOMS Y));
coherence ;

end;

definition

let X be set ;
let Y be real-functions-membered set ;
let f be PartFunc of X,Y;
let c be real number ;
:: original: [-]
redefine func f [-] c -> PartFunc of X,(R_PFuncs (DOMS Y));
coherence

proof end;

end;

definition

let X be set ;
let Y be rational-functions-membered set ;
let f be PartFunc of X,Y;
let c be rational number ;
:: original: [-]
redefine func f [-] c -> PartFunc of X,(Q_PFuncs (DOMS Y));
coherence

proof end;

end;

definition

let X be set ;
let Y be integer-functions-membered set ;
let f be PartFunc of X,Y;
let c be integer number ;
:: original: [-]
redefine func f [-] c -> PartFunc of X,(I_PFuncs (DOMS Y));
coherence

proof end;

end;

theorem :: VALUED_2:49

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: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 holds (f [+] c1) [-] c2 = f [+] (c1 - c2)

proof end;

theorem :: VALUED_2:51

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

proof end;

theorem :: VALUED_2:52

for X being set
for Y being complex-functions-membered set
for c1, c2 being complex number
for f being PartFunc of X,Y holds (f [-] c1) [-] 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 :Def39: :: VALUED_2:def 39
( 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 Def39 defines [#] VALUED_2:def 39 :

definition

let X be set ;
let Y be complex-functions-membered set ;
let f be PartFunc of X,Y;
let c be complex number ;
:: original: [#]
redefine func f [#] c -> PartFunc of X,(C_PFuncs (DOMS Y));
coherence

proof end;

end;

definition

let X be set ;
let Y be real-functions-membered set ;
let f be PartFunc of X,Y;
let c be real number ;
:: original: [#]
redefine func f [#] c -> PartFunc of X,(R_PFuncs (DOMS Y));
coherence

proof end;

end;

definition

let X be set ;
let Y be rational-functions-membered set ;
let f be PartFunc of X,Y;
let c be rational number ;
:: original: [#]
redefine func f [#] c -> PartFunc of X,(Q_PFuncs (DOMS Y));
coherence

proof end;

end;

definition

let X be set ;
let Y be integer-functions-membered set ;
let f be PartFunc of X,Y;
let c be integer number ;
:: original: [#]
redefine func f [#] c -> PartFunc of X,(I_PFuncs (DOMS Y));
coherence

proof end;

end;

definition

let X be set ;
let Y be natural-functions-membered set ;
let f be PartFunc of X,Y;
let c be natural number ;
:: original: [#]
redefine func f [#] c -> PartFunc of X,(N_PFuncs (DOMS Y));
coherence

proof end;

end;

theorem :: VALUED_2:53

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

proof end;

theorem :: VALUED_2:54

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 40
f [#] (c ");
coherence ;

end;

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

theorem :: VALUED_2:55

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

theorem :: VALUED_2:56

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

definition

let X be set ;
let Y be complex-functions-membered set ;
let f be PartFunc of X,Y;
let c be complex number ;
:: original: [/]
redefine func f [/] c -> PartFunc of X,(C_PFuncs (DOMS Y));
coherence ;

end;

definition

let X be set ;
let Y be real-functions-membered set ;
let f be PartFunc of X,Y;
let c be real number ;
:: original: [/]
redefine func f [/] c -> PartFunc of X,(R_PFuncs (DOMS Y));
coherence

proof end;

end;

definition

let X be set ;
let Y be rational-functions-membered set ;
let f be PartFunc of X,Y;
let c be rational number ;
:: original: [/]
redefine func f [/] c -> PartFunc of X,(Q_PFuncs (DOMS Y));
coherence

proof end;

end;

theorem :: VALUED_2:57

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

proof end;

theorem :: VALUED_2:58

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 :Def41: :: VALUED_2:def 41
( 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 Def41 defines <+> VALUED_2:def 41 :

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;
:: original: <+>
redefine func f <+> g -> PartFunc of (X /\ (dom g)),(C_PFuncs (DOMS Y));
coherence

proof end;

end;

definition

let X be set ;
let Y be real-functions-membered set ;
let f be PartFunc of X,Y;
let g be real-valued Function;
:: original: <+>
redefine func f <+> g -> PartFunc of (X /\ (dom g)),(R_PFuncs (DOMS Y));
coherence

proof end;

end;

definition

let X be set ;
let Y be rational-functions-membered set ;
let f be PartFunc of X,Y;
let g be rational-valued Function;
:: original: <+>
redefine func f <+> g -> PartFunc of (X /\ (dom g)),(Q_PFuncs (DOMS Y));
coherence

proof end;

end;

definition

let X be set ;
let Y be integer-functions-membered set ;
let f be PartFunc of X,Y;
let g be integer-valued Function;
:: original: <+>
redefine func f <+> g -> PartFunc of (X /\ (dom g)),(I_PFuncs (DOMS Y));
coherence

proof end;

end;

definition

let X be set ;
let Y be natural-functions-membered set ;
let f be PartFunc of X,Y;
let g be natural-valued Function;
:: original: <+>
redefine func f <+> g -> PartFunc of (X /\ (dom g)),(N_PFuncs (DOMS Y));
coherence

proof end;

end;

theorem :: VALUED_2:59

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

proof end;

theorem :: VALUED_2:60

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)

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 42
f <+> (- g);
coherence ;

end;

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

theorem Th61: :: VALUED_2:61

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 Th62: :: VALUED_2:62

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;

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;
:: original: <->
redefine func f <-> g -> PartFunc of (X /\ (dom g)),(C_PFuncs (DOMS Y));
coherence

proof end;

end;

definition

let X be set ;
let Y be real-functions-membered set ;
let f be PartFunc of X,Y;
let g be real-valued Function;
:: original: <->
redefine func f <-> g -> PartFunc of (X /\ (dom g)),(R_PFuncs (DOMS Y));
coherence

proof end;

end;

definition

let X be set ;
let Y be rational-functions-membered set ;
let f be PartFunc of X,Y;
let g be rational-valued Function;
:: original: <->
redefine func f <-> g -> PartFunc of (X /\ (dom g)),(Q_PFuncs (DOMS Y));
coherence

proof end;

end;

definition

let X be set ;
let Y be integer-functions-membered set ;
let f be PartFunc of X,Y;
let g be integer-valued Function;
:: original: <->
redefine func f <-> g -> PartFunc of (X /\ (dom g)),(I_PFuncs (DOMS Y));
coherence

proof end;

end;

theorem :: VALUED_2:63

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

proof end;

theorem :: VALUED_2:65

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

proof end;

theorem :: VALUED_2:66

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

proof end;

theorem :: VALUED_2:67

for X being set
for Y being complex-functions-membered set
for f being PartFunc of X,Y
for g, h being complex-valued Function holds (f <-> g) <-> 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;
deffunc H₁( set ) -> set = (f . $1) (#) (g . $1);
func f <#> g -> Function means :Def43: :: VALUED_2:def 43
( 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 Def43 defines <#> VALUED_2:def 43 :

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;
:: original: <#>
redefine func f <#> g -> PartFunc of (X /\ (dom g)),(C_PFuncs (DOMS Y));
coherence

proof end;

end;

definition

let X be set ;
let Y be real-functions-membered set ;
let f be PartFunc of X,Y;
let g be real-valued Function;
:: original: <#>
redefine func f <#> g -> PartFunc of (X /\ (dom g)),(R_PFuncs (DOMS Y));
coherence

proof end;

end;

definition

let X be set ;
let Y be rational-functions-membered set ;
let f be PartFunc of X,Y;
let g be rational-valued Function;
:: original: <#>
redefine func f <#> g -> PartFunc of (X /\ (dom g)),(Q_PFuncs (DOMS Y));
coherence

proof end;

end;

definition

let X be set ;
let Y be integer-functions-membered set ;
let f be PartFunc of X,Y;
let g be integer-valued Function;
:: original: <#>
redefine func f <#> g -> PartFunc of (X /\ (dom g)),(I_PFuncs (DOMS Y));
coherence

proof end;

end;

definition

let X be set ;
let Y be natural-functions-membered set ;
let f be PartFunc of X,Y;
let g be natural-valued Function;
:: original: <#>
redefine func f <#> g -> PartFunc of (X /\ (dom g)),(N_PFuncs (DOMS Y));
coherence

proof end;

end;

theorem :: VALUED_2:68

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

proof end;

theorem :: VALUED_2:69

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)

proof end;

theorem :: VALUED_2:70

for X being set
for Y being complex-functions-membered set
for f being PartFunc of X,Y
for g, h being complex-valued Function holds (f <#> g) <#> 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 44
f <#> (g ");
coherence ;

end;

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

theorem Th71: :: VALUED_2:71

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 Th72: :: VALUED_2:72

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;

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;
:: original: </>
redefine func f </> g -> PartFunc of (X /\ (dom g)),(C_PFuncs (DOMS Y));
coherence by VALUED_1:def 7;

end;

definition

let X be set ;
let Y be real-functions-membered set ;
let f be PartFunc of X,Y;
let g be real-valued Function;
:: original: </>
redefine func f </> g -> PartFunc of (X /\ (dom g)),(R_PFuncs (DOMS Y));
coherence

proof end;

end;

definition

let X be set ;
let Y be rational-functions-membered set ;
let f be PartFunc of X,Y;
let g be rational-valued Function;
:: original: </>
redefine func f </> g -> PartFunc of (X /\ (dom g)),(Q_PFuncs (DOMS Y));
coherence

proof end;

end;

theorem :: VALUED_2:73

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

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 :

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;
:: original: <++>
redefine func f <++> g -> PartFunc of (X1 /\ X2),(C_PFuncs ((DOMS Y1) /\ (DOMS Y2)));
coherence

proof end;

end;

definition

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;
:: original: <++>
redefine func f <++> g -> PartFunc of (X1 /\ X2),(R_PFuncs ((DOMS Y1) /\ (DOMS Y2)));
coherence

proof end;

end;

definition

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;
:: original: <++>
redefine func f <++> g -> PartFunc of (X1 /\ X2),(Q_PFuncs ((DOMS Y1) /\ (DOMS Y2)));
coherence

proof end;

end;

definition

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;
:: original: <++>
redefine func f <++> g -> PartFunc of (X1 /\ X2),(I_PFuncs ((DOMS Y1) /\ (DOMS Y2)));
coherence

proof end;

end;

definition

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;
:: original: <++>
redefine func f <++> g -> PartFunc of (X1 /\ X2),(N_PFuncs ((DOMS Y1) /\ (DOMS Y2)));
coherence

proof end;

end;

theorem :: VALUED_2:74

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:75

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 holds (f <++> f1) <++> f2 = f <++> (f1 <++> f2)

proof end;

theorem :: VALUED_2:76

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) = (<-> f1) <++> (<-> f2)

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 :

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;
:: original: <-->
redefine func f <--> g -> PartFunc of (X1 /\ X2),(C_PFuncs ((DOMS Y1) /\ (DOMS Y2)));
coherence

proof end;

end;

definition

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;
:: original: <-->
redefine func f <--> g -> PartFunc of (X1 /\ X2),(R_PFuncs ((DOMS Y1) /\ (DOMS Y2)));
coherence

proof end;

end;

definition

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;
:: original: <-->
redefine func f <--> g -> PartFunc of (X1 /\ X2),(Q_PFuncs ((DOMS Y1) /\ (DOMS Y2)));
coherence

proof end;

end;

definition

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;
:: original: <-->
redefine func f <--> g -> PartFunc of (X1 /\ X2),(I_PFuncs ((DOMS Y1) /\ (DOMS Y2)));
coherence

proof end;

end;

theorem :: VALUED_2:77

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:78

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) = (<-> f1) <++> f2

proof end;

theorem :: VALUED_2:79

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 holds (f <++> f1) <--> f2 = f <++> (f1 <--> f2)

proof end;

theorem :: VALUED_2:80

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 holds (f <--> f1) <++> f2 = f <--> (f1 <--> f2)

proof end;

theorem :: VALUED_2:81

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 holds (f <--> f1) <--> f2 = f <--> (f1 <++> f2)

proof end;

theorem :: VALUED_2:82

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 :

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;
:: original: <##>
redefine func f <##> g -> PartFunc of (X1 /\ X2),(C_PFuncs ((DOMS Y1) /\ (DOMS Y2)));
coherence

proof end;

end;

definition

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;
:: original: <##>
redefine func f <##> g -> PartFunc of (X1 /\ X2),(R_PFuncs ((DOMS Y1) /\ (DOMS Y2)));
coherence

proof end;

end;

definition

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;
:: original: <##>
redefine func f <##> g -> PartFunc of (X1 /\ X2),(Q_PFuncs ((DOMS Y1) /\ (DOMS Y2)));
coherence

proof end;

end;

definition

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;
:: original: <##>
redefine func f <##> g -> PartFunc of (X1 /\ X2),(I_PFuncs ((DOMS Y1) /\ (DOMS Y2)));
coherence

proof end;

end;

definition

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;
:: original: <##>
redefine func f <##> g -> PartFunc of (X1 /\ X2),(N_PFuncs ((DOMS Y1) /\ (DOMS Y2)));
coherence

proof end;

end;

theorem Th83: :: VALUED_2:83

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:84

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 holds (f <##> f1) <##> f2 = f <##> (f1 <##> f2)

proof end;

theorem :: VALUED_2:85

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 = <-> (f1 <##> f2)

proof end;

theorem :: VALUED_2:86

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) = <-> (f1 <##> f2)

proof end;

theorem Th87: :: VALUED_2:87

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 holds f <##> (f1 <++> f2) = (f <##> f1) <++> (f <##> f2)

proof end;

theorem :: VALUED_2:88

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 holds (f1 <++> f2) <##> f = (f1 <##> f) <++> (f2 <##> f)

proof end;

theorem Th89: :: VALUED_2:89

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 holds f <##> (f1 <--> f2) = (f <##> f1) <--> (f <##> f2)

proof end;

theorem :: VALUED_2:90

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 holds (f1 <--> f2) <##> f = (f1 <##> f) <--> (f2 <##> f)

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 :Def48: :: VALUED_2:def 48
( 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 Def48 defines <//> VALUED_2:def 48 :

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;
:: original: <//>
redefine func f <//> g -> PartFunc of (X1 /\ X2),(C_PFuncs ((DOMS Y1) /\ (DOMS Y2)));
coherence

proof end;

end;

definition

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;
:: original: <//>
redefine func f <//> g -> PartFunc of (X1 /\ X2),(R_PFuncs ((DOMS Y1) /\ (DOMS Y2)));
coherence

proof end;

end;

definition

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;
:: original: <//>
redefine func f <//> g -> PartFunc of (X1 /\ X2),(Q_PFuncs ((DOMS Y1) /\ (DOMS Y2)));
coherence

proof end;

end;

theorem :: VALUED_2:91

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 = <-> (f1 <//> f2)

proof end;

theorem :: VALUED_2:92

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) = <-> (f1 <//> f2)

proof end;

theorem :: VALUED_2:93

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 holds (f <##> f1) <//> f2 = f <##> (f1 <//> f2)

proof end;

theorem :: VALUED_2:94

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 holds (f <//> f1) <##> f2 = (f <##> f2) <//> f1

proof end;

theorem :: VALUED_2:95

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 holds (f <//> f1) <//> f2 = f <//> (f1 <##> f2)

proof end;

theorem :: VALUED_2:96

proof end;

theorem :: VALUED_2:97

proof end;