:: by Artur Korni{\l}owicz

::

:: Received October 15, 2008

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

begin

Lm1: now :: thesis: for X1, X2, X3 being set holds X1 /\ (X2 /\ X3) = (X1 /\ X2) /\ (X1 /\ X3)

let X1, X2, X3 be set ; :: thesis: X1 /\ (X2 /\ X3) = (X1 /\ X2) /\ (X1 /\ X3)

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

end;
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: verum

definition
end;

:: deftheorem defines DOMS VALUED_2:def 1 :

for Y being functional set holds DOMS Y = union { (dom f) where f is Element of Y : verum } ;

for Y being functional set holds DOMS Y = union { (dom f) where f is Element of Y : verum } ;

definition

let X be set ;

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

for x being set st x in X holds

x is complex-valued Function;

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

for X being set holds

( X is complex-functions-membered iff for x being set st x in X holds

x is complex-valued Function );

for X being set holds

( X is complex-functions-membered iff for x being set st x in X holds

x is complex-valued Function );

definition

let X be set ;

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

for x being set st x in X holds

x is ext-real-valued Function;

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

for X being set holds

( X is ext-real-functions-membered iff for x being set st x in X holds

x is ext-real-valued Function );

for X being set holds

( X is ext-real-functions-membered iff for x being set st x in X holds

x is ext-real-valued Function );

definition

let X be set ;

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

for x being set st x in X holds

x is real-valued Function;

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

for X being set holds

( X is real-functions-membered iff for x being set st x in X holds

x is real-valued Function );

for X being set holds

( X is real-functions-membered iff for x being set st x in X holds

x is real-valued Function );

definition

let X be set ;

end;
attr X is rational-functions-membered means :Def5: :: VALUED_2:def 5

for x being set st x in X holds

x is RAT -valued Function;

for x being set st x in X holds

x is RAT -valued Function;

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

for X being set holds

( X is rational-functions-membered iff for x being set st x in X holds

x is RAT -valued Function );

for X being set holds

( X is rational-functions-membered iff for x being set st x in X holds

x is RAT -valued Function );

definition

let X be set ;

end;
attr X is integer-functions-membered means :Def6: :: VALUED_2:def 6

for x being set st x in X holds

x is INT -valued Function;

for x being set st x in X holds

x is INT -valued Function;

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

for X being set holds

( X is integer-functions-membered iff for x being set st x in X holds

x is INT -valued Function );

for X being set holds

( X is integer-functions-membered iff for x being set st x in X holds

x is INT -valued Function );

definition

let X be set ;

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

for x being set st x in X holds

x is natural-valued Function;

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

for X being set holds

( X is natural-functions-membered iff for x being set st x in X holds

x is natural-valued Function );

for X being set holds

( X is natural-functions-membered iff for x being set st x in X holds

x is natural-valued Function );

registration

coherence

for b_{1} being set st b_{1} is natural-functions-membered holds

b_{1} is integer-functions-membered

for b_{1} being set st b_{1} is integer-functions-membered holds

b_{1} is rational-functions-membered

for b_{1} being set st b_{1} is rational-functions-membered holds

b_{1} is real-functions-membered

for b_{1} being set st b_{1} is real-functions-membered holds

b_{1} is complex-functions-membered

for b_{1} being set st b_{1} is real-functions-membered holds

b_{1} is ext-real-functions-membered

end;
for b

b

proof end;

coherence for b

b

proof end;

coherence for b

b

proof end;

coherence for b

b

proof end;

coherence for b

b

proof end;

registration

coherence

for b_{1} being set st b_{1} is empty holds

b_{1} is natural-functions-membered

end;
for b

b

proof end;

registration
end;

registration

coherence

for b_{1} being set st b_{1} is complex-functions-membered holds

b_{1} is functional

for b_{1} being set st b_{1} is ext-real-functions-membered holds

b_{1} is functional

end;
for b

b

proof end;

coherence for b

b

proof end;

set ff = the natural-valued Function;

registration

existence

ex b_{1} being set st

( b_{1} is natural-functions-membered & not b_{1} is empty )

end;
ex b

( b

proof end;

registration

let X be complex-functions-membered set ;

coherence

for b_{1} being Subset of X holds b_{1} is complex-functions-membered

end;
coherence

for b

proof end;

registration

let X be ext-real-functions-membered set ;

coherence

for b_{1} being Subset of X holds b_{1} is ext-real-functions-membered

end;
coherence

for b

proof end;

registration

let X be real-functions-membered set ;

coherence

for b_{1} being Subset of X holds b_{1} is real-functions-membered

end;
coherence

for b

proof end;

registration

let X be rational-functions-membered set ;

coherence

for b_{1} being Subset of X holds b_{1} is rational-functions-membered

end;
coherence

for b

proof end;

registration

let X be integer-functions-membered set ;

coherence

for b_{1} being Subset of X holds b_{1} is integer-functions-membered

end;
coherence

for b

proof end;

registration

let X be natural-functions-membered set ;

coherence

for b_{1} being Subset of X holds b_{1} is natural-functions-membered

end;
coherence

for b

proof end;

definition

set A = COMPLEX ;

let D be set ;

defpred S_{1}[ set ] means $1 is PartFunc of D,COMPLEX;

ex b_{1} being set st

for f being set holds

( f in b_{1} iff f is PartFunc of D,COMPLEX )

for b_{1}, b_{2} being set st ( for f being set holds

( f in b_{1} iff f is PartFunc of D,COMPLEX ) ) & ( for f being set holds

( f in b_{2} iff f is PartFunc of D,COMPLEX ) ) holds

b_{1} = b_{2}

end;
let D be set ;

defpred S

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 for f being set holds

( f in it iff f is PartFunc of D,COMPLEX );

ex b

for f being set holds

( f in b

proof end;

uniqueness for b

( f in b

( f in b

b

proof end;

:: deftheorem Def8 defines C_PFuncs VALUED_2:def 8 :

for D, b_{2} being set holds

( b_{2} = C_PFuncs D iff for f being set holds

( f in b_{2} iff f is PartFunc of D,COMPLEX ) );

for D, b

( b

( f in b

definition

set A = COMPLEX ;

let D be set ;

defpred S_{1}[ set ] means $1 is Function of D,COMPLEX;

ex b_{1} being set st

for f being set holds

( f in b_{1} iff f is Function of D,COMPLEX )

for b_{1}, b_{2} being set st ( for f being set holds

( f in b_{1} iff f is Function of D,COMPLEX ) ) & ( for f being set holds

( f in b_{2} iff f is Function of D,COMPLEX ) ) holds

b_{1} = b_{2}

end;
let D be set ;

defpred S

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 for f being set holds

( f in it iff f is Function of D,COMPLEX );

ex b

for f being set holds

( f in b

proof end;

uniqueness for b

( f in b

( f in b

b

proof end;

:: deftheorem Def9 defines C_Funcs VALUED_2:def 9 :

for D, b_{2} being set holds

( b_{2} = C_Funcs D iff for f being set holds

( f in b_{2} iff f is Function of D,COMPLEX ) );

for D, b

( b

( f in b

definition

set A = ExtREAL ;

let D be set ;

defpred S_{1}[ set ] means $1 is PartFunc of D,ExtREAL;

ex b_{1} being set st

for f being set holds

( f in b_{1} iff f is PartFunc of D,ExtREAL )

for b_{1}, b_{2} being set st ( for f being set holds

( f in b_{1} iff f is PartFunc of D,ExtREAL ) ) & ( for f being set holds

( f in b_{2} iff f is PartFunc of D,ExtREAL ) ) holds

b_{1} = b_{2}

end;
let D be set ;

defpred S

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 for f being set holds

( f in it iff f is PartFunc of D,ExtREAL );

ex b

for f being set holds

( f in b

proof end;

uniqueness for b

( f in b

( f in b

b

proof end;

:: deftheorem Def10 defines E_PFuncs VALUED_2:def 10 :

for D, b_{2} being set holds

( b_{2} = E_PFuncs D iff for f being set holds

( f in b_{2} iff f is PartFunc of D,ExtREAL ) );

for D, b

( b

( f in b

definition

set A = ExtREAL ;

let D be set ;

defpred S_{1}[ set ] means $1 is Function of D,ExtREAL;

ex b_{1} being set st

for f being set holds

( f in b_{1} iff f is Function of D,ExtREAL )

for b_{1}, b_{2} being set st ( for f being set holds

( f in b_{1} iff f is Function of D,ExtREAL ) ) & ( for f being set holds

( f in b_{2} iff f is Function of D,ExtREAL ) ) holds

b_{1} = b_{2}

end;
let D be set ;

defpred S

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 for f being set holds

( f in it iff f is Function of D,ExtREAL );

ex b

for f being set holds

( f in b

proof end;

uniqueness for b

( f in b

( f in b

b

proof end;

:: deftheorem Def11 defines E_Funcs VALUED_2:def 11 :

for D, b_{2} being set holds

( b_{2} = E_Funcs D iff for f being set holds

( f in b_{2} iff f is Function of D,ExtREAL ) );

for D, b

( b

( f in b

definition

set A = REAL ;

let D be set ;

defpred S_{1}[ set ] means $1 is PartFunc of D,REAL;

ex b_{1} being set st

for f being set holds

( f in b_{1} iff f is PartFunc of D,REAL )

for b_{1}, b_{2} being set st ( for f being set holds

( f in b_{1} iff f is PartFunc of D,REAL ) ) & ( for f being set holds

( f in b_{2} iff f is PartFunc of D,REAL ) ) holds

b_{1} = b_{2}

end;
let D be set ;

defpred S

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 for f being set holds

( f in it iff f is PartFunc of D,REAL );

ex b

for f being set holds

( f in b

proof end;

uniqueness for b

( f in b

( f in b

b

proof end;

:: deftheorem Def12 defines R_PFuncs VALUED_2:def 12 :

for D, b_{2} being set holds

( b_{2} = R_PFuncs D iff for f being set holds

( f in b_{2} iff f is PartFunc of D,REAL ) );

for D, b

( b

( f in b

definition

set A = REAL ;

let D be set ;

defpred S_{1}[ set ] means $1 is Function of D,REAL;

ex b_{1} being set st

for f being set holds

( f in b_{1} iff f is Function of D,REAL )

for b_{1}, b_{2} being set st ( for f being set holds

( f in b_{1} iff f is Function of D,REAL ) ) & ( for f being set holds

( f in b_{2} iff f is Function of D,REAL ) ) holds

b_{1} = b_{2}

end;
let D be set ;

defpred S

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 for f being set holds

( f in it iff f is Function of D,REAL );

ex b

for f being set holds

( f in b

proof end;

uniqueness for b

( f in b

( f in b

b

proof end;

:: deftheorem Def13 defines R_Funcs VALUED_2:def 13 :

for D, b_{2} being set holds

( b_{2} = R_Funcs D iff for f being set holds

( f in b_{2} iff f is Function of D,REAL ) );

for D, b

( b

( f in b

definition

set A = RAT ;

let D be set ;

defpred S_{1}[ set ] means $1 is PartFunc of D,RAT;

ex b_{1} being set st

for f being set holds

( f in b_{1} iff f is PartFunc of D,RAT )

for b_{1}, b_{2} being set st ( for f being set holds

( f in b_{1} iff f is PartFunc of D,RAT ) ) & ( for f being set holds

( f in b_{2} iff f is PartFunc of D,RAT ) ) holds

b_{1} = b_{2}

end;
let D be set ;

defpred S

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 for f being set holds

( f in it iff f is PartFunc of D,RAT );

ex b

for f being set holds

( f in b

proof end;

uniqueness for b

( f in b

( f in b

b

proof end;

:: deftheorem Def14 defines Q_PFuncs VALUED_2:def 14 :

for D, b_{2} being set holds

( b_{2} = Q_PFuncs D iff for f being set holds

( f in b_{2} iff f is PartFunc of D,RAT ) );

for D, b

( b

( f in b

definition

set A = RAT ;

let D be set ;

defpred S_{1}[ set ] means $1 is Function of D,RAT;

ex b_{1} being set st

for f being set holds

( f in b_{1} iff f is Function of D,RAT )

for b_{1}, b_{2} being set st ( for f being set holds

( f in b_{1} iff f is Function of D,RAT ) ) & ( for f being set holds

( f in b_{2} iff f is Function of D,RAT ) ) holds

b_{1} = b_{2}

end;
let D be set ;

defpred S

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 for f being set holds

( f in it iff f is Function of D,RAT );

ex b

for f being set holds

( f in b

proof end;

uniqueness for b

( f in b

( f in b

b

proof end;

:: deftheorem Def15 defines Q_Funcs VALUED_2:def 15 :

for D, b_{2} being set holds

( b_{2} = Q_Funcs D iff for f being set holds

( f in b_{2} iff f is Function of D,RAT ) );

for D, b

( b

( f in b

definition

set A = INT ;

let D be set ;

defpred S_{1}[ set ] means $1 is PartFunc of D,INT;

ex b_{1} being set st

for f being set holds

( f in b_{1} iff f is PartFunc of D,INT )

for b_{1}, b_{2} being set st ( for f being set holds

( f in b_{1} iff f is PartFunc of D,INT ) ) & ( for f being set holds

( f in b_{2} iff f is PartFunc of D,INT ) ) holds

b_{1} = b_{2}

end;
let D be set ;

defpred S

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 for f being set holds

( f in it iff f is PartFunc of D,INT );

ex b

for f being set holds

( f in b

proof end;

uniqueness for b

( f in b

( f in b

b

proof end;

:: deftheorem Def16 defines I_PFuncs VALUED_2:def 16 :

for D, b_{2} being set holds

( b_{2} = I_PFuncs D iff for f being set holds

( f in b_{2} iff f is PartFunc of D,INT ) );

for D, b

( b

( f in b

definition

set A = INT ;

let D be set ;

defpred S_{1}[ set ] means $1 is Function of D,INT;

ex b_{1} being set st

for f being set holds

( f in b_{1} iff f is Function of D,INT )

for b_{1}, b_{2} being set st ( for f being set holds

( f in b_{1} iff f is Function of D,INT ) ) & ( for f being set holds

( f in b_{2} iff f is Function of D,INT ) ) holds

b_{1} = b_{2}

end;
let D be set ;

defpred S

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 for f being set holds

( f in it iff f is Function of D,INT );

ex b

for f being set holds

( f in b

proof end;

uniqueness for b

( f in b

( f in b

b

proof end;

:: deftheorem Def17 defines I_Funcs VALUED_2:def 17 :

for D, b_{2} being set holds

( b_{2} = I_Funcs D iff for f being set holds

( f in b_{2} iff f is Function of D,INT ) );

for D, b

( b

( f in b

definition

set A = NAT ;

let D be set ;

defpred S_{1}[ set ] means $1 is PartFunc of D,NAT;

ex b_{1} being set st

for f being set holds

( f in b_{1} iff f is PartFunc of D,NAT )

for b_{1}, b_{2} being set st ( for f being set holds

( f in b_{1} iff f is PartFunc of D,NAT ) ) & ( for f being set holds

( f in b_{2} iff f is PartFunc of D,NAT ) ) holds

b_{1} = b_{2}

end;
let D be set ;

defpred S

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 for f being set holds

( f in it iff f is PartFunc of D,NAT );

ex b

for f being set holds

( f in b

proof end;

uniqueness for b

( f in b

( f in b

b

proof end;

:: deftheorem Def18 defines N_PFuncs VALUED_2:def 18 :

for D, b_{2} being set holds

( b_{2} = N_PFuncs D iff for f being set holds

( f in b_{2} iff f is PartFunc of D,NAT ) );

for D, b

( b

( f in b

definition

set A = NAT ;

let D be set ;

defpred S_{1}[ set ] means $1 is Function of D,NAT;

ex b_{1} being set st

for f being set holds

( f in b_{1} iff f is Function of D,NAT )

for b_{1}, b_{2} being set st ( for f being set holds

( f in b_{1} iff f is Function of D,NAT ) ) & ( for f being set holds

( f in b_{2} iff f is Function of D,NAT ) ) holds

b_{1} = b_{2}

end;
let D be set ;

defpred S

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 for f being set holds

( f in it iff f is Function of D,NAT );

ex b

for f being set holds

( f in b

proof end;

uniqueness for b

( f in b

( f in b

b

proof end;

:: deftheorem Def19 defines N_Funcs VALUED_2:def 19 :

for D, b_{2} being set holds

( b_{2} = N_Funcs D iff for f being set holds

( f in b_{2} iff f is Function of D,NAT ) );

for D, b

( b

( f in b

registration

let X be set ;

coherence

C_PFuncs X is complex-functions-membered

C_Funcs X is complex-functions-membered

E_PFuncs X is ext-real-functions-membered

E_Funcs X is ext-real-functions-membered

R_PFuncs X is real-functions-membered

R_Funcs X is real-functions-membered

Q_PFuncs X is rational-functions-membered

Q_Funcs X is rational-functions-membered

I_PFuncs X is integer-functions-membered

I_Funcs X is integer-functions-membered

N_PFuncs X is natural-functions-membered

N_Funcs X is natural-functions-membered

end;
coherence

C_PFuncs X is complex-functions-membered

proof end;

coherence C_Funcs X is complex-functions-membered

proof end;

coherence E_PFuncs X is ext-real-functions-membered

proof end;

coherence E_Funcs X is ext-real-functions-membered

proof end;

coherence R_PFuncs X is real-functions-membered

proof end;

coherence R_Funcs X is real-functions-membered

proof end;

coherence Q_PFuncs X is rational-functions-membered

proof end;

coherence Q_Funcs X is rational-functions-membered

proof end;

coherence I_PFuncs X is integer-functions-membered

proof end;

coherence I_Funcs X is integer-functions-membered

proof end;

coherence N_PFuncs X is natural-functions-membered

proof end;

coherence N_Funcs X is natural-functions-membered

proof end;

registration

let X be complex-functions-membered set ;

coherence

for b_{1} being Element of X holds b_{1} is complex-valued

end;
coherence

for b

proof end;

registration

let X be ext-real-functions-membered set ;

coherence

for b_{1} being Element of X holds b_{1} is ext-real-valued

end;
coherence

for b

proof end;

registration

let X be real-functions-membered set ;

coherence

for b_{1} being Element of X holds b_{1} is real-valued

end;
coherence

for b

proof end;

registration

let X be rational-functions-membered set ;

coherence

for b_{1} being Element of X holds b_{1} is RAT -valued

end;
coherence

for b

proof end;

registration

let X be integer-functions-membered set ;

coherence

for b_{1} being Element of X holds b_{1} is INT -valued

end;
coherence

for b

proof end;

registration

let X be natural-functions-membered set ;

coherence

for b_{1} being Element of X holds b_{1} is natural-valued

end;
coherence

for b

proof end;

registration

let X, x be set ;

let Y be complex-functions-membered set ;

let f be PartFunc of X,Y;

coherence

( f . x is Function-like & f . x is Relation-like ) ;

end;
let Y be complex-functions-membered set ;

let f be PartFunc of X,Y;

coherence

( f . x is Function-like & f . x is Relation-like ) ;

registration

let X, x be set ;

let Y be ext-real-functions-membered set ;

let f be PartFunc of X,Y;

coherence

( f . x is Function-like & f . x is Relation-like ) ;

end;
let Y be ext-real-functions-membered set ;

let f be PartFunc of X,Y;

coherence

( f . x is Function-like & f . x is Relation-like ) ;

registration

let X, x be set ;

let Y be complex-functions-membered set ;

let f be PartFunc of X,Y;

coherence

f . x is complex-valued

end;
let Y be complex-functions-membered set ;

let f be PartFunc of X,Y;

coherence

f . x is complex-valued

proof end;

registration

let X, x be set ;

let Y be ext-real-functions-membered set ;

let f be PartFunc of X,Y;

coherence

f . x is ext-real-valued

end;
let Y be ext-real-functions-membered set ;

let f be PartFunc of X,Y;

coherence

f . x is ext-real-valued

proof end;

registration

let X, x be set ;

let Y be real-functions-membered set ;

let f be PartFunc of X,Y;

coherence

f . x is real-valued

end;
let Y be real-functions-membered set ;

let f be PartFunc of X,Y;

coherence

f . x is real-valued

proof end;

registration

let X, x be set ;

let Y be rational-functions-membered set ;

let f be PartFunc of X,Y;

coherence

f . x is RAT -valued

end;
let Y be rational-functions-membered set ;

let f be PartFunc of X,Y;

coherence

f . x is RAT -valued

proof end;

registration

let X, x be set ;

let Y be integer-functions-membered set ;

let f be PartFunc of X,Y;

coherence

f . x is INT -valued

end;
let Y be integer-functions-membered set ;

let f be PartFunc of X,Y;

coherence

f . x is INT -valued

proof end;

registration

let X, x be set ;

let Y be natural-functions-membered set ;

let f be PartFunc of X,Y;

coherence

f . x is natural-valued

end;
let Y be natural-functions-membered set ;

let f be PartFunc of X,Y;

coherence

f . x is natural-valued

proof end;

registration

let X be set ;

let Y be complex-membered set ;

coherence

PFuncs (X,Y) is complex-functions-membered

end;
let Y be complex-membered set ;

coherence

PFuncs (X,Y) is complex-functions-membered

proof end;

registration

let X be set ;

let Y be ext-real-membered set ;

coherence

PFuncs (X,Y) is ext-real-functions-membered

end;
let Y be ext-real-membered set ;

coherence

PFuncs (X,Y) is ext-real-functions-membered

proof end;

registration

let X be set ;

let Y be real-membered set ;

coherence

PFuncs (X,Y) is real-functions-membered

end;
let Y be real-membered set ;

coherence

PFuncs (X,Y) is real-functions-membered

proof end;

registration

let X be set ;

let Y be rational-membered set ;

coherence

PFuncs (X,Y) is rational-functions-membered

end;
let Y be rational-membered set ;

coherence

PFuncs (X,Y) is rational-functions-membered

proof end;

registration

let X be set ;

let Y be integer-membered set ;

coherence

PFuncs (X,Y) is integer-functions-membered

end;
let Y be integer-membered set ;

coherence

PFuncs (X,Y) is integer-functions-membered

proof end;

registration

let X be set ;

let Y be natural-membered set ;

coherence

PFuncs (X,Y) is natural-functions-membered

end;
let Y be natural-membered set ;

coherence

PFuncs (X,Y) is natural-functions-membered

proof end;

registration

let X be set ;

let Y be complex-membered set ;

coherence

Funcs (X,Y) is complex-functions-membered

end;
let Y be complex-membered set ;

coherence

Funcs (X,Y) is complex-functions-membered

proof end;

registration

let X be set ;

let Y be ext-real-membered set ;

coherence

Funcs (X,Y) is ext-real-functions-membered

end;
let Y be ext-real-membered set ;

coherence

Funcs (X,Y) is ext-real-functions-membered

proof end;

registration

let X be set ;

let Y be real-membered set ;

coherence

Funcs (X,Y) is real-functions-membered

end;
let Y be real-membered set ;

coherence

Funcs (X,Y) is real-functions-membered

proof end;

registration

let X be set ;

let Y be rational-membered set ;

coherence

Funcs (X,Y) is rational-functions-membered

end;
let Y be rational-membered set ;

coherence

Funcs (X,Y) is rational-functions-membered

proof end;

registration

let X be set ;

let Y be integer-membered set ;

coherence

Funcs (X,Y) is integer-functions-membered

end;
let Y be integer-membered set ;

coherence

Funcs (X,Y) is integer-functions-membered

proof end;

registration

let X be set ;

let Y be natural-membered set ;

coherence

Funcs (X,Y) is natural-functions-membered

end;
let Y be natural-membered set ;

coherence

Funcs (X,Y) is natural-functions-membered

proof end;

definition

let R be Relation;

end;
attr R is complex-functions-valued means :Def20: :: VALUED_2:def 20

rng R is complex-functions-membered ;

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 ;

rng R is ext-real-functions-membered ;

attr R is rational-functions-valued means :Def23: :: VALUED_2:def 23

rng R is rational-functions-membered ;

rng R is rational-functions-membered ;

attr R is integer-functions-valued means :Def24: :: VALUED_2:def 24

rng R is integer-functions-membered ;

rng R is integer-functions-membered ;

attr R is natural-functions-valued means :Def25: :: VALUED_2:def 25

rng R is natural-functions-membered ;

rng R is natural-functions-membered ;

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

for R being Relation holds

( R is complex-functions-valued iff rng R is complex-functions-membered );

for R being Relation holds

( R is complex-functions-valued iff rng R is complex-functions-membered );

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

for R being Relation holds

( R is ext-real-functions-valued iff rng R is ext-real-functions-membered );

for R being Relation holds

( R is ext-real-functions-valued iff rng R is ext-real-functions-membered );

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

for R being Relation holds

( R is real-functions-valued iff rng R is real-functions-membered );

for R being Relation holds

( R is real-functions-valued iff rng R is real-functions-membered );

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

for R being Relation holds

( R is rational-functions-valued iff rng R is rational-functions-membered );

for R being Relation holds

( R is rational-functions-valued iff rng R is rational-functions-membered );

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

for R being Relation holds

( R is integer-functions-valued iff rng R is integer-functions-membered );

for R being Relation holds

( R is integer-functions-valued iff rng R is integer-functions-membered );

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

for R being Relation holds

( R is natural-functions-valued iff rng R is natural-functions-membered );

for R being Relation holds

( R is natural-functions-valued iff rng R is natural-functions-membered );

registration

let Y be complex-functions-membered set ;

coherence

for b_{1} being Y -valued Function holds b_{1} is complex-functions-valued

end;
coherence

for b

proof end;

definition

let f be Function;

( f is complex-functions-valued iff for x being set st x in dom f holds

f . x is complex-valued Function )

( f is ext-real-functions-valued iff for x being set st x in dom f holds

f . x is ext-real-valued Function )

( f is real-functions-valued iff for x being set st x in dom f holds

f . x is real-valued Function )

( f is rational-functions-valued iff for x being set st x in dom f holds

f . x is RAT -valued Function )

( f is integer-functions-valued iff for x being set st x in dom f holds

f . x is INT -valued Function )

( f is natural-functions-valued iff for x being set st x in dom f holds

f . x is natural-valued Function )

end;
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 for x being set st x in dom f holds

f . x is complex-valued Function;

( f is complex-functions-valued iff for x being set st x in dom f holds

f . x is complex-valued Function )

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 for x being set st x in dom f holds

f . x is ext-real-valued Function;

( f is ext-real-functions-valued iff for x being set st x in dom f holds

f . x is ext-real-valued Function )

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 for x being set st x in dom f holds

f . x is real-valued Function;

( f is real-functions-valued iff for x being set st x in dom f holds

f . x is real-valued Function )

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 RAT -valued Function;

compatibility for x being set st x in dom f holds

f . x is RAT -valued Function;

( f is rational-functions-valued iff for x being set st x in dom f holds

f . x is RAT -valued Function )

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 INT -valued Function;

compatibility for x being set st x in dom f holds

f . x is INT -valued Function;

( f is integer-functions-valued iff for x being set st x in dom f holds

f . x is INT -valued Function )

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 for x being set st x in dom f holds

f . x is natural-valued Function;

( f is natural-functions-valued iff for x being set st x in dom f holds

f . x is natural-valued Function )

proof end;

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

for f being Function holds

( f is complex-functions-valued iff for x being set st x in dom f holds

f . x is complex-valued Function );

for f being Function holds

( f is complex-functions-valued iff for x being set st x in dom f holds

f . x is complex-valued Function );

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

for f being Function holds

( f is ext-real-functions-valued iff for x being set st x in dom f holds

f . x is ext-real-valued Function );

for f being Function holds

( f is ext-real-functions-valued iff for x being set st x in dom f holds

f . x is ext-real-valued Function );

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

for f being Function holds

( f is real-functions-valued iff for x being set st x in dom f holds

f . x is real-valued Function );

for f being Function holds

( f is real-functions-valued iff for x being set st x in dom f holds

f . x is real-valued Function );

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

for f being Function holds

( f is rational-functions-valued iff for x being set st x in dom f holds

f . x is RAT -valued Function );

for f being Function holds

( f is rational-functions-valued iff for x being set st x in dom f holds

f . x is RAT -valued Function );

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

for f being Function holds

( f is integer-functions-valued iff for x being set st x in dom f holds

f . x is INT -valued Function );

for f being Function holds

( f is integer-functions-valued iff for x being set st x in dom f holds

f . x is INT -valued Function );

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

for f being Function holds

( f is natural-functions-valued iff for x being set st x in dom f holds

f . x is natural-valued Function );

for f being Function holds

( f is natural-functions-valued iff for x being set st x in dom f holds

f . x is natural-valued Function );

registration

coherence

for b_{1} being Relation st b_{1} is natural-functions-valued holds

b_{1} is integer-functions-valued

for b_{1} being Relation st b_{1} is integer-functions-valued holds

b_{1} is rational-functions-valued

for b_{1} being Relation st b_{1} is rational-functions-valued holds

b_{1} is real-functions-valued

for b_{1} being Relation st b_{1} is real-functions-valued holds

b_{1} is ext-real-functions-valued

for b_{1} being Relation st b_{1} is real-functions-valued holds

b_{1} is complex-functions-valued

end;
for b

b

proof end;

coherence for b

b

proof end;

coherence for b

b

proof end;

coherence for b

b

proof end;

coherence for b

b

proof end;

registration

coherence

for b_{1} being Relation st b_{1} is empty holds

b_{1} is natural-functions-valued

end;
for b

b

proof end;

registration
end;

registration

let R be ext-real-functions-valued Relation;

coherence

rng R is ext-real-functions-membered by Def21;

end;
coherence

rng R is ext-real-functions-membered by Def21;

registration
end;

registration

let R be rational-functions-valued Relation;

coherence

rng R is rational-functions-membered by Def23;

end;
coherence

rng R is rational-functions-membered by Def23;

registration
end;

registration
end;

registration

let X be set ;

let Y be complex-functions-membered set ;

coherence

for b_{1} being PartFunc of X,Y holds b_{1} is complex-functions-valued
;

end;
let Y be complex-functions-membered set ;

coherence

for b

registration

let X be set ;

let Y be ext-real-functions-membered set ;

coherence

for b_{1} being PartFunc of X,Y holds b_{1} is ext-real-functions-valued

end;
let Y be ext-real-functions-membered set ;

coherence

for b

proof end;

registration

let X be set ;

let Y be real-functions-membered set ;

coherence

for b_{1} being PartFunc of X,Y holds b_{1} is real-functions-valued

end;
let Y be real-functions-membered set ;

coherence

for b

proof end;

registration

let X be set ;

let Y be rational-functions-membered set ;

coherence

for b_{1} being PartFunc of X,Y holds b_{1} is rational-functions-valued

end;
let Y be rational-functions-membered set ;

coherence

for b

proof end;

registration

let X be set ;

let Y be integer-functions-membered set ;

coherence

for b_{1} being PartFunc of X,Y holds b_{1} is integer-functions-valued

end;
let Y be integer-functions-membered set ;

coherence

for b

proof end;

registration

let X be set ;

let Y be natural-functions-membered set ;

coherence

for b_{1} being PartFunc of X,Y holds b_{1} is natural-functions-valued

end;
let Y be natural-functions-membered set ;

coherence

for b

proof end;

registration

let f be complex-functions-valued Function;

let x be set ;

coherence

( f . x is Function-like & f . x is Relation-like )

end;
let x be set ;

coherence

( f . x is Function-like & f . x is Relation-like )

proof end;

registration

let f be ext-real-functions-valued Function;

let x be set ;

coherence

( f . x is Function-like & f . x is Relation-like )

end;
let x be set ;

coherence

( f . x is Function-like & f . x is Relation-like )

proof end;

registration

let f be complex-functions-valued Function;

let x be set ;

coherence

f . x is complex-valued

end;
let x be set ;

coherence

f . x is complex-valued

proof end;

registration

let f be ext-real-functions-valued Function;

let x be set ;

coherence

f . x is ext-real-valued

end;
let x be set ;

coherence

f . x is ext-real-valued

proof end;

registration
end;

registration

let f be rational-functions-valued Function;

let x be set ;

coherence

f . x is RAT -valued

end;
let x be set ;

coherence

f . x is RAT -valued

proof end;

registration
end;

registration

let f be natural-functions-valued Function;

let x be set ;

coherence

f . x is natural-valued

end;
let x be set ;

coherence

f . x is natural-valued

proof 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

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

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

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

c1 = c2

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)

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)

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)

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)

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)

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

proof end;

definition
end;

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

for f being complex-valued Function

for c being complex number holds f (/) c = (1 / c) (#) f;

for f being complex-valued Function

for c being complex number holds f (/) c = (1 / c) (#) f;

registration
end;

registration
end;

registration
end;

registration

let f be complex-valued FinSequence;

let c be complex number ;

coherence

f (/) c is FinSequence-like ;

end;
let c be complex number ;

coherence

f (/) c is FinSequence-like ;

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;

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

theorem :: VALUED_2:29

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

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)

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

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)

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)

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)

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)

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)

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

proof end;

definition

let f be complex-functions-valued Function;

deffunc H_{1}( set ) -> set = - (f . $1);

ex b_{1} being Function st

( dom b_{1} = dom f & ( for x being set st x in dom b_{1} holds

b_{1} . x = - (f . x) ) )

for b_{1}, b_{2} being Function st dom b_{1} = dom f & ( for x being set st x in dom b_{1} holds

b_{1} . x = - (f . x) ) & dom b_{2} = dom f & ( for x being set st x in dom b_{2} holds

b_{2} . x = - (f . x) ) holds

b_{1} = b_{2}

end;
deffunc H

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 ( dom it = dom f & ( for x being set st x in dom it holds

it . x = - (f . x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def33 defines <-> VALUED_2:def 33 :

for f being complex-functions-valued Function

for b_{2} being Function holds

( b_{2} = <-> f iff ( dom b_{2} = dom f & ( for x being set st x in dom b_{2} holds

b_{2} . x = - (f . x) ) ) );

for f being complex-functions-valued Function

for b

( b

b

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

<-> f is PartFunc of X,(C_PFuncs (DOMS Y))

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

<-> f is PartFunc of X,(C_PFuncs (DOMS Y))

proof 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

<-> f is PartFunc of X,(R_PFuncs (DOMS Y))

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

<-> f is PartFunc of X,(R_PFuncs (DOMS Y))

proof 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

<-> f is PartFunc of X,(Q_PFuncs (DOMS Y))

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

<-> f is PartFunc of X,(Q_PFuncs (DOMS Y))

proof 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

<-> f is PartFunc of X,(I_PFuncs (DOMS Y))

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

<-> f is PartFunc of X,(I_PFuncs (DOMS Y))

proof end;

registration

let Y be complex-functions-membered set ;

let f be FinSequence of Y;

coherence

<-> f is FinSequence-like

end;
let f be FinSequence of Y;

coherence

<-> f is FinSequence-like

proof 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

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

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_{1}[ set , set ] means ex a being complex-valued Function st

( $1 = a & $2 = f . (- a) );

ex b_{1} being Function st

( dom b_{1} = dom f & ( for x being complex-valued Function st x in dom b_{1} holds

b_{1} . x = f . (- x) ) )

for b_{1}, b_{2} being Function st dom b_{1} = dom f & ( for x being complex-valued Function st x in dom b_{1} holds

b_{1} . x = f . (- x) ) & dom b_{2} = dom f & ( for x being complex-valued Function st x in dom b_{2} holds

b_{2} . x = f . (- x) ) holds

b_{1} = b_{2}

end;
let Y be set ;

let f be PartFunc of X,Y;

defpred S

( $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 ( dom it = dom f & ( for x being complex-valued Function st x in dom it holds

it . x = f . (- x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

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

for X being complex-functions-membered set

for Y being set

for f being PartFunc of X,Y

for b_{4} being Function holds

( b_{4} = f (-) iff ( dom b_{4} = dom f & ( for x being complex-valued Function st x in dom b_{4} holds

b_{4} . x = f . (- x) ) ) );

for X being complex-functions-membered set

for Y being set

for f being PartFunc of X,Y

for b

( b

b

definition

let f be complex-functions-valued Function;

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

ex b_{1} being Function st

( dom b_{1} = dom f & ( for x being set st x in dom b_{1} holds

b_{1} . x = (f . x) " ) )

for b_{1}, b_{2} being Function st dom b_{1} = dom f & ( for x being set st x in dom b_{1} holds

b_{1} . x = (f . x) " ) & dom b_{2} = dom f & ( for x being set st x in dom b_{2} holds

b_{2} . x = (f . x) " ) holds

b_{1} = b_{2}

end;
deffunc H

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 ( dom it = dom f & ( for x being set st x in dom it holds

it . x = (f . x) " ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def35 defines </> VALUED_2:def 35 :

for f being complex-functions-valued Function

for b_{2} being Function holds

( b_{2} = </> f iff ( dom b_{2} = dom f & ( for x being set st x in dom b_{2} holds

b_{2} . x = (f . x) " ) ) );

for f being complex-functions-valued Function

for b

( b

b

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

</> f is PartFunc of X,(C_PFuncs (DOMS Y))

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

</> f is PartFunc of X,(C_PFuncs (DOMS Y))

proof 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

</> f is PartFunc of X,(R_PFuncs (DOMS Y))

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

</> f is PartFunc of X,(R_PFuncs (DOMS Y))

proof 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

</> f is PartFunc of X,(Q_PFuncs (DOMS Y))

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

</> f is PartFunc of X,(Q_PFuncs (DOMS Y))

proof end;

registration

let Y be complex-functions-membered set ;

let f be FinSequence of Y;

coherence

</> f is FinSequence-like

end;
let f be FinSequence of Y;

coherence

</> f is FinSequence-like

proof 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

for Y being complex-functions-membered set

for f being PartFunc of X,Y holds </> (</> f) = f

proof end;

definition

let f be complex-functions-valued Function;

deffunc H_{1}( set ) -> set = abs (f . $1);

ex b_{1} being Function st

( dom b_{1} = dom f & ( for x being set st x in dom b_{1} holds

b_{1} . x = abs (f . x) ) )

for b_{1}, b_{2} being Function st dom b_{1} = dom f & ( for x being set st x in dom b_{1} holds

b_{1} . x = abs (f . x) ) & dom b_{2} = dom f & ( for x being set st x in dom b_{2} holds

b_{2} . x = abs (f . x) ) holds

b_{1} = b_{2}

end;
deffunc H

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 ( dom it = dom f & ( for x being set st x in dom it holds

it . x = abs (f . x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def36 defines abs VALUED_2:def 36 :

for f being complex-functions-valued Function

for b_{2} being Function holds

( b_{2} = abs f iff ( dom b_{2} = dom f & ( for x being set st x in dom b_{2} holds

b_{2} . x = abs (f . x) ) ) );

for f being complex-functions-valued Function

for b

( b

b

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

abs f is PartFunc of X,(C_PFuncs (DOMS Y))

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

abs f is PartFunc of X,(C_PFuncs (DOMS Y))

proof 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

abs f is PartFunc of X,(R_PFuncs (DOMS Y))

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

abs f is PartFunc of X,(R_PFuncs (DOMS Y))

proof 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

abs f is PartFunc of X,(Q_PFuncs (DOMS Y))

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

abs f is PartFunc of X,(Q_PFuncs (DOMS Y))

proof 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

abs f is PartFunc of X,(N_PFuncs (DOMS Y))

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

abs f is PartFunc of X,(N_PFuncs (DOMS Y))

proof end;

registration

let Y be complex-functions-membered set ;

let f be FinSequence of Y;

coherence

abs f is FinSequence-like

end;
let f be FinSequence of Y;

coherence

abs f is FinSequence-like

proof 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

for Y being complex-functions-membered set

for f being PartFunc of X,Y holds abs (abs f) = abs f

proof end;

definition

let Y be complex-functions-membered set ;

let f be Y -valued Function;

let c be complex number ;

deffunc H_{1}( set ) -> set = c + (f . $1);

ex b_{1} being Function st

( dom b_{1} = dom f & ( for x being set st x in dom b_{1} holds

b_{1} . x = c + (f . x) ) )

for b_{1}, b_{2} being Function st dom b_{1} = dom f & ( for x being set st x in dom b_{1} holds

b_{1} . x = c + (f . x) ) & dom b_{2} = dom f & ( for x being set st x in dom b_{2} holds

b_{2} . x = c + (f . x) ) holds

b_{1} = b_{2}

end;
let f be Y -valued Function;

let c be complex number ;

deffunc H

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 ( dom it = dom f & ( for x being set st x in dom it holds

it . x = c + (f . x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def37 defines [+] VALUED_2:def 37 :

for Y being complex-functions-membered set

for f being b_{1} -valued Function

for c being complex number

for b_{4} being Function holds

( b_{4} = f [+] c iff ( dom b_{4} = dom f & ( for x being set st x in dom b_{4} holds

b_{4} . x = c + (f . x) ) ) );

for Y being complex-functions-membered set

for f being b

for c being complex number

for b

( b

b

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

f [+] c is PartFunc of X,(C_PFuncs (DOMS Y))

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

f [+] c is PartFunc of X,(C_PFuncs (DOMS Y))

proof 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

f [+] c is PartFunc of X,(R_PFuncs (DOMS Y))

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

f [+] c is PartFunc of X,(R_PFuncs (DOMS Y))

proof 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

f [+] c is PartFunc of X,(Q_PFuncs (DOMS Y))

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

f [+] c is PartFunc of X,(Q_PFuncs (DOMS Y))

proof 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

f [+] c is PartFunc of X,(I_PFuncs (DOMS Y))

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

f [+] c is PartFunc of X,(I_PFuncs (DOMS Y))

proof end;

definition

let X be set ;

let Y be natural-functions-membered set ;

let f be PartFunc of X,Y;

let c be Nat;

:: original: [+]

redefine func f [+] c -> PartFunc of X,(N_PFuncs (DOMS Y));

coherence

f [+] c is PartFunc of X,(N_PFuncs (DOMS Y))

end;
let Y be natural-functions-membered set ;

let f be PartFunc of X,Y;

let c be Nat;

:: original: [+]

redefine func f [+] c -> PartFunc of X,(N_PFuncs (DOMS Y));

coherence

f [+] c is PartFunc of X,(N_PFuncs (DOMS Y))

proof 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)

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

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 Y be complex-functions-membered set ;

let f be Y -valued Function;

let c be complex number ;

coherence

f [+] (- c) is Function ;

end;
let f be Y -valued Function;

let c be complex number ;

coherence

f [+] (- c) is Function ;

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

for Y being complex-functions-membered set

for f being b_{1} -valued Function

for c being complex number holds f [-] c = f [+] (- c);

for Y being complex-functions-membered set

for f being b

for c being complex number holds f [-] c = f [+] (- c);

theorem :: VALUED_2:47

theorem :: VALUED_2:48

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

f [-] c is PartFunc of X,(C_PFuncs (DOMS Y))

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

f [-] c is PartFunc of X,(C_PFuncs (DOMS Y))

proof 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

f [-] c is PartFunc of X,(R_PFuncs (DOMS Y))

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

f [-] c is PartFunc of X,(R_PFuncs (DOMS Y))

proof 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

f [-] c is PartFunc of X,(Q_PFuncs (DOMS Y))

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

f [-] c is PartFunc of X,(Q_PFuncs (DOMS Y))

proof 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

f [-] c is PartFunc of X,(I_PFuncs (DOMS Y))

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

f [-] c is PartFunc of X,(I_PFuncs (DOMS Y))

proof 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

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)

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)

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)

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 Y be complex-functions-membered set ;

let f be Y -valued Function;

let c be complex number ;

deffunc H_{1}( set ) -> set = c (#) (f . $1);

ex b_{1} being Function st

( dom b_{1} = dom f & ( for x being set st x in dom b_{1} holds

b_{1} . x = c (#) (f . x) ) )

for b_{1}, b_{2} being Function st dom b_{1} = dom f & ( for x being set st x in dom b_{1} holds

b_{1} . x = c (#) (f . x) ) & dom b_{2} = dom f & ( for x being set st x in dom b_{2} holds

b_{2} . x = c (#) (f . x) ) holds

b_{1} = b_{2}

end;
let f be Y -valued Function;

let c be complex number ;

deffunc H

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 ( dom it = dom f & ( for x being set st x in dom it holds

it . x = c (#) (f . x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def39 defines [#] VALUED_2:def 39 :

for Y being complex-functions-membered set

for f being b_{1} -valued Function

for c being complex number

for b_{4} being Function holds

( b_{4} = f [#] c iff ( dom b_{4} = dom f & ( for x being set st x in dom b_{4} holds

b_{4} . x = c (#) (f . x) ) ) );

for Y being complex-functions-membered set

for f being b

for c being complex number

for b

( b

b

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

f [#] c is PartFunc of X,(C_PFuncs (DOMS Y))

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

f [#] c is PartFunc of X,(C_PFuncs (DOMS Y))

proof 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

f [#] c is PartFunc of X,(R_PFuncs (DOMS Y))

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

f [#] c is PartFunc of X,(R_PFuncs (DOMS Y))

proof 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

f [#] c is PartFunc of X,(Q_PFuncs (DOMS Y))

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

f [#] c is PartFunc of X,(Q_PFuncs (DOMS Y))

proof 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

f [#] c is PartFunc of X,(I_PFuncs (DOMS Y))

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

f [#] c is PartFunc of X,(I_PFuncs (DOMS Y))

proof end;

definition

let X be set ;

let Y be natural-functions-membered set ;

let f be PartFunc of X,Y;

let c be Nat;

:: original: [#]

redefine func f [#] c -> PartFunc of X,(N_PFuncs (DOMS Y));

coherence

f [#] c is PartFunc of X,(N_PFuncs (DOMS Y))

end;
let Y be natural-functions-membered set ;

let f be PartFunc of X,Y;

let c be Nat;

:: original: [#]

redefine func f [#] c -> PartFunc of X,(N_PFuncs (DOMS Y));

coherence

f [#] c is PartFunc of X,(N_PFuncs (DOMS Y))

proof 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)

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

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 Y be complex-functions-membered set ;

let f be Y -valued Function;

let c be complex number ;

coherence

f [#] (c ") is Function ;

end;
let f be Y -valued Function;

let c be complex number ;

coherence

f [#] (c ") is Function ;

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

for Y being complex-functions-membered set

for f being b_{1} -valued Function

for c being complex number holds f [/] c = f [#] (c ");

for Y being complex-functions-membered set

for f being b

for c being complex number holds f [/] c = f [#] (c ");

theorem :: VALUED_2:55

theorem :: VALUED_2:56

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

f [/] c is PartFunc of X,(C_PFuncs (DOMS Y))

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

f [/] c is PartFunc of X,(C_PFuncs (DOMS Y))

proof 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

f [/] c is PartFunc of X,(R_PFuncs (DOMS Y))

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

f [/] c is PartFunc of X,(R_PFuncs (DOMS Y))

proof 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

f [/] c is PartFunc of X,(Q_PFuncs (DOMS Y))

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

f [/] c is PartFunc of X,(Q_PFuncs (DOMS Y))

proof 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)

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

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

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 Y be complex-functions-membered set ;

let f be Y -valued Function;

let g be complex-valued Function;

deffunc H_{1}( set ) -> set = (f . $1) + (g . $1);

ex b_{1} being Function st

( dom b_{1} = (dom f) /\ (dom g) & ( for x being set st x in dom b_{1} holds

b_{1} . x = (f . x) + (g . x) ) )

for b_{1}, b_{2} being Function st dom b_{1} = (dom f) /\ (dom g) & ( for x being set st x in dom b_{1} holds

b_{1} . x = (f . x) + (g . x) ) & dom b_{2} = (dom f) /\ (dom g) & ( for x being set st x in dom b_{2} holds

b_{2} . x = (f . x) + (g . x) ) holds

b_{1} = b_{2}

end;
let f be Y -valued Function;

let g be complex-valued Function;

deffunc H

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 ( dom it = (dom f) /\ (dom g) & ( for x being set st x in dom it holds

it . x = (f . x) + (g . x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def41 defines <+> VALUED_2:def 41 :

for Y being complex-functions-membered set

for f being b_{1} -valued Function

for g being complex-valued Function

for b_{4} being Function holds

( b_{4} = f <+> g iff ( dom b_{4} = (dom f) /\ (dom g) & ( for x being set st x in dom b_{4} holds

b_{4} . x = (f . x) + (g . x) ) ) );

for Y being complex-functions-membered set

for f being b

for g being complex-valued Function

for b

( b

b

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

f <+> g is PartFunc of (X /\ (dom g)),(C_PFuncs (DOMS Y))

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

f <+> g is PartFunc of (X /\ (dom g)),(C_PFuncs (DOMS Y))

proof 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

f <+> g is PartFunc of (X /\ (dom g)),(R_PFuncs (DOMS Y))

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

f <+> g is PartFunc of (X /\ (dom g)),(R_PFuncs (DOMS Y))

proof end;

definition

let X be set ;

let Y be rational-functions-membered set ;

let f be PartFunc of X,Y;

let g be RAT -valued Function;

:: original: <+>

redefine func f <+> g -> PartFunc of (X /\ (dom g)),(Q_PFuncs (DOMS Y));

coherence

f <+> g is PartFunc of (X /\ (dom g)),(Q_PFuncs (DOMS Y))

end;
let Y be rational-functions-membered set ;

let f be PartFunc of X,Y;

let g be RAT -valued Function;

:: original: <+>

redefine func f <+> g -> PartFunc of (X /\ (dom g)),(Q_PFuncs (DOMS Y));

coherence

f <+> g is PartFunc of (X /\ (dom g)),(Q_PFuncs (DOMS Y))

proof end;

definition

let X be set ;

let Y be integer-functions-membered set ;

let f be PartFunc of X,Y;

let g be INT -valued Function;

:: original: <+>

redefine func f <+> g -> PartFunc of (X /\ (dom g)),(I_PFuncs (DOMS Y));

coherence

f <+> g is PartFunc of (X /\ (dom g)),(I_PFuncs (DOMS Y))

end;
let Y be integer-functions-membered set ;

let f be PartFunc of X,Y;

let g be INT -valued Function;

:: original: <+>

redefine func f <+> g -> PartFunc of (X /\ (dom g)),(I_PFuncs (DOMS Y));

coherence

f <+> g is PartFunc of (X /\ (dom g)),(I_PFuncs (DOMS Y))

proof 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

f <+> g is PartFunc of (X /\ (dom g)),(N_PFuncs (DOMS Y))

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

f <+> g is PartFunc of (X /\ (dom g)),(N_PFuncs (DOMS Y))

proof 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)

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)

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 Y be complex-functions-membered set ;

let f be Y -valued Function;

let g be complex-valued Function;

coherence

f <+> (- g) is Function ;

end;
let f be Y -valued Function;

let g be complex-valued Function;

coherence

f <+> (- g) is Function ;

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

for Y being complex-functions-membered set

for f being b_{1} -valued Function

for g being complex-valued Function holds f <-> g = f <+> (- g);

for Y being complex-functions-membered set

for f being b

for g being complex-valued Function holds f <-> g = f <+> (- g);

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)

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)

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

f <-> g is PartFunc of (X /\ (dom g)),(C_PFuncs (DOMS Y))

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

f <-> g is PartFunc of (X /\ (dom g)),(C_PFuncs (DOMS Y))

proof 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

f <-> g is PartFunc of (X /\ (dom g)),(R_PFuncs (DOMS Y))

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

f <-> g is PartFunc of (X /\ (dom g)),(R_PFuncs (DOMS Y))

proof end;

definition

let X be set ;

let Y be rational-functions-membered set ;

let f be PartFunc of X,Y;

let g be RAT -valued Function;

:: original: <->

redefine func f <-> g -> PartFunc of (X /\ (dom g)),(Q_PFuncs (DOMS Y));

coherence

f <-> g is PartFunc of (X /\ (dom g)),(Q_PFuncs (DOMS Y))

end;
let Y be rational-functions-membered set ;

let f be PartFunc of X,Y;

let g be RAT -valued Function;

:: original: <->

redefine func f <-> g -> PartFunc of (X /\ (dom g)),(Q_PFuncs (DOMS Y));

coherence

f <-> g is PartFunc of (X /\ (dom g)),(Q_PFuncs (DOMS Y))

proof end;

definition

let X be set ;

let Y be integer-functions-membered set ;

let f be PartFunc of X,Y;

let g be INT -valued Function;

:: original: <->

redefine func f <-> g -> PartFunc of (X /\ (dom g)),(I_PFuncs (DOMS Y));

coherence

f <-> g is PartFunc of (X /\ (dom g)),(I_PFuncs (DOMS Y))

end;
let Y be integer-functions-membered set ;

let f be PartFunc of X,Y;

let g be INT -valued Function;

:: original: <->

redefine func f <-> g -> PartFunc of (X /\ (dom g)),(I_PFuncs (DOMS Y));

coherence

f <-> g is PartFunc of (X /\ (dom g)),(I_PFuncs (DOMS Y))

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

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

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)

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)

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)

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 Y be complex-functions-membered set ;

let f be Y -valued Function;

let g be complex-valued Function;

deffunc H_{1}( set ) -> set = (f . $1) (#) (g . $1);

ex b_{1} being Function st

( dom b_{1} = (dom f) /\ (dom g) & ( for x being set st x in dom b_{1} holds

b_{1} . x = (f . x) (#) (g . x) ) )

for b_{1}, b_{2} being Function st dom b_{1} = (dom f) /\ (dom g) & ( for x being set st x in dom b_{1} holds

b_{1} . x = (f . x) (#) (g . x) ) & dom b_{2} = (dom f) /\ (dom g) & ( for x being set st x in dom b_{2} holds

b_{2} . x = (f . x) (#) (g . x) ) holds

b_{1} = b_{2}

end;
let f be Y -valued Function;

let g be complex-valued Function;

deffunc H

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 ( dom it = (dom f) /\ (dom g) & ( for x being set st x in dom it holds

it . x = (f . x) (#) (g . x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def43 defines <#> VALUED_2:def 43 :

for Y being complex-functions-membered set

for f being b_{1} -valued Function

for g being complex-valued Function

for b_{4} being Function holds

( b_{4} = f <#> g iff ( dom b_{4} = (dom f) /\ (dom g) & ( for x being set st x in dom b_{4} holds

b_{4} . x = (f . x) (#) (g . x) ) ) );

for Y being complex-functions-membered set

for f being b

for g being complex-valued Function

for b

( b

b

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

f <#> g is PartFunc of (X /\ (dom g)),(C_PFuncs (DOMS Y))

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

f <#> g is PartFunc of (X /\ (dom g)),(C_PFuncs (DOMS Y))

proof 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

f <#> g is PartFunc of (X /\ (dom g)),(R_PFuncs (DOMS Y))

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

f <#> g is PartFunc of (X /\ (dom g)),(R_PFuncs (DOMS Y))

proof end;

definition

let X be set ;

let Y be rational-functions-membered set ;

let f be PartFunc of X,Y;

let g be RAT -valued Function;

:: original: <#>

redefine func f <#> g -> PartFunc of (X /\ (dom g)),(Q_PFuncs (DOMS Y));

coherence

f <#> g is PartFunc of (X /\ (dom g)),(Q_PFuncs (DOMS Y))

end;
let Y be rational-functions-membered set ;

let f be PartFunc of X,Y;

let g be RAT -valued Function;

:: original: <#>

redefine func f <#> g -> PartFunc of (X /\ (dom g)),(Q_PFuncs (DOMS Y));

coherence

f <#> g is PartFunc of (X /\ (dom g)),(Q_PFuncs (DOMS Y))

proof end;

definition

let X be set ;

let Y be integer-functions-membered set ;

let f be PartFunc of X,Y;

let g be INT -valued Function;

:: original: <#>

redefine func f <#> g -> PartFunc of (X /\ (dom g)),(I_PFuncs (DOMS Y));

coherence

f <#> g is PartFunc of (X /\ (dom g)),(I_PFuncs (DOMS Y))

end;
let Y be integer-functions-membered set ;

let f be PartFunc of X,Y;

let g be INT -valued Function;

:: original: <#>

redefine func f <#> g -> PartFunc of (X /\ (dom g)),(I_PFuncs (DOMS Y));

coherence

f <#> g is PartFunc of (X /\ (dom g)),(I_PFuncs (DOMS Y))

proof 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

f <#> g is PartFunc of (X /\ (dom g)),(N_PFuncs (DOMS Y))

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

f <#> g is PartFunc of (X /\ (dom g)),(N_PFuncs (DOMS Y))

proof 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

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)

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)

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 Y be complex-functions-membered set ;

let f be Y -valued Function;

let g be complex-valued Function;

coherence

f <#> (g ") is Function ;

end;
let f be Y -valued Function;

let g be complex-valued Function;

coherence

f <#> (g ") is Function ;

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

for Y being complex-functions-membered set

for f being b_{1} -valued Function

for g being complex-valued Function holds f </> g = f <#> (g ");

for Y being complex-functions-membered set

for f being b

for g being complex-valued Function holds f </> g = f <#> (g ");

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)

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)

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

f </> g is PartFunc of (X /\ (dom g)),(C_PFuncs (DOMS Y))

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

f </> g is PartFunc of (X /\ (dom g)),(C_PFuncs (DOMS Y))

proof 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

f </> g is PartFunc of (X /\ (dom g)),(R_PFuncs (DOMS Y))

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

f </> g is PartFunc of (X /\ (dom g)),(R_PFuncs (DOMS Y))

proof end;

definition

let X be set ;

let Y be rational-functions-membered set ;

let f be PartFunc of X,Y;

let g be RAT -valued Function;

:: original: </>

redefine func f </> g -> PartFunc of (X /\ (dom g)),(Q_PFuncs (DOMS Y));

coherence

f </> g is PartFunc of (X /\ (dom g)),(Q_PFuncs (DOMS Y))

end;
let Y be rational-functions-membered set ;

let f be PartFunc of X,Y;

let g be RAT -valued Function;

:: original: </>

redefine func f </> g -> PartFunc of (X /\ (dom g)),(Q_PFuncs (DOMS Y));

coherence

f </> g is PartFunc of (X /\ (dom g)),(Q_PFuncs (DOMS Y))

proof 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)

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 Y1, Y2 be complex-functions-membered set ;

let f be Y1 -valued Function;

let g be Y2 -valued Function;

deffunc H_{1}( set ) -> set = (f . $1) + (g . $1);

ex b_{1} being Function st

( dom b_{1} = (dom f) /\ (dom g) & ( for x being set st x in dom b_{1} holds

b_{1} . x = (f . x) + (g . x) ) )

for b_{1}, b_{2} being Function st dom b_{1} = (dom f) /\ (dom g) & ( for x being set st x in dom b_{1} holds

b_{1} . x = (f . x) + (g . x) ) & dom b_{2} = (dom f) /\ (dom g) & ( for x being set st x in dom b_{2} holds

b_{2} . x = (f . x) + (g . x) ) holds

b_{1} = b_{2}

end;
let f be Y1 -valued Function;

let g be Y2 -valued Function;

deffunc H

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 ( dom it = (dom f) /\ (dom g) & ( for x being set st x in dom it holds

it . x = (f . x) + (g . x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

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

for Y1, Y2 being complex-functions-membered set

for f being b_{1} -valued Function

for g being b_{2} -valued Function

for b_{5} being Function holds

( b_{5} = f <++> g iff ( dom b_{5} = (dom f) /\ (dom g) & ( for x being set st x in dom b_{5} holds

b_{5} . x = (f . x) + (g . x) ) ) );

for Y1, Y2 being complex-functions-membered set

for f being b

for g being b

for b

( b

b

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

f <++> g is PartFunc of (X1 /\ X2),(C_PFuncs ((DOMS Y1) /\ (DOMS Y2)))

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

f <++> g is PartFunc of (X1 /\ X2),(C_PFuncs ((DOMS Y1) /\ (DOMS Y2)))

proof 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

f <++> g is PartFunc of (X1 /\ X2),(R_PFuncs ((DOMS Y1) /\ (DOMS Y2)))

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

f <++> g is PartFunc of (X1 /\ X2),(R_PFuncs ((DOMS Y1) /\ (DOMS Y2)))

proof 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

f <++> g is PartFunc of (X1 /\ X2),(Q_PFuncs ((DOMS Y1) /\ (DOMS Y2)))

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

f <++> g is PartFunc of (X1 /\ X2),(Q_PFuncs ((DOMS Y1) /\ (DOMS Y2)))

proof 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

f <++> g is PartFunc of (X1 /\ X2),(I_PFuncs ((DOMS Y1) /\ (DOMS Y2)))

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

f <++> g is PartFunc of (X1 /\ X2),(I_PFuncs ((DOMS Y1) /\ (DOMS Y2)))

proof 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

f <++> g is PartFunc of (X1 /\ X2),(N_PFuncs ((DOMS Y1) /\ (DOMS Y2)))

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

f <++> g is PartFunc of (X1 /\ X2),(N_PFuncs ((DOMS Y1) /\ (DOMS Y2)))

proof 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

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)

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)

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 Y1, Y2 be complex-functions-membered set ;

let f be Y1 -valued Function;

let g be Y2 -valued Function;

deffunc H_{1}( set ) -> set = (f . $1) - (g . $1);

ex b_{1} being Function st

( dom b_{1} = (dom f) /\ (dom g) & ( for x being set st x in dom b_{1} holds

b_{1} . x = (f . x) - (g . x) ) )

for b_{1}, b_{2} being Function st dom b_{1} = (dom f) /\ (dom g) & ( for x being set st x in dom b_{1} holds

b_{1} . x = (f . x) - (g . x) ) & dom b_{2} = (dom f) /\ (dom g) & ( for x being set st x in dom b_{2} holds

b_{2} . x = (f . x) - (g . x) ) holds

b_{1} = b_{2}

end;
let f be Y1 -valued Function;

let g be Y2 -valued Function;

deffunc H

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 ( dom it = (dom f) /\ (dom g) & ( for x being set st x in dom it holds

it . x = (f . x) - (g . x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

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

for Y1, Y2 being complex-functions-membered set

for f being b_{1} -valued Function

for g being b_{2} -valued Function

for b_{5} being Function holds

( b_{5} = f <--> g iff ( dom b_{5} = (dom f) /\ (dom g) & ( for x being set st x in dom b_{5} holds

b_{5} . x = (f . x) - (g . x) ) ) );

for Y1, Y2 being complex-functions-membered set

for f being b

for g being b

for b

( b

b

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

f <--> g is PartFunc of (X1 /\ X2),(C_PFuncs ((DOMS Y1) /\ (DOMS Y2)))

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

f <--> g is PartFunc of (X1 /\ X2),(C_PFuncs ((DOMS Y1) /\ (DOMS Y2)))

proof 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

f <--> g is PartFunc of (X1 /\ X2),(R_PFuncs ((DOMS Y1) /\ (DOMS Y2)))

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

f <--> g is PartFunc of (X1 /\ X2),(R_PFuncs ((DOMS Y1) /\ (DOMS Y2)))

proof 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

f <--> g is PartFunc of (X1 /\ X2),(Q_PFuncs ((DOMS Y1) /\ (DOMS Y2)))

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

f <--> g is PartFunc of (X1 /\ X2),(Q_PFuncs ((DOMS Y1) /\ (DOMS Y2)))

proof 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

f <--> g is PartFunc of (X1 /\ X2),(I_PFuncs ((DOMS Y1) /\ (DOMS Y2)))

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

f <--> g is PartFunc of (X1 /\ X2),(I_PFuncs ((DOMS Y1) /\ (DOMS Y2)))

proof 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)

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

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)

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)

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)

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

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

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;

definition

let Y1, Y2 be complex-functions-membered set ;

let f be Y1 -valued Function;

let g be Y2 -valued Function;

deffunc H_{1}( set ) -> set = (f . $1) (#) (g . $1);

ex b_{1} being Function st

( dom b_{1} = (dom f) /\ (dom g) & ( for x being set st x in dom b_{1} holds

b_{1} . x = (f . x) (#) (g . x) ) )

for b_{1}, b_{2} being Function st dom b_{1} = (dom f) /\ (dom g) & ( for x being set st x in dom b_{1} holds

b_{1} . x = (f . x) (#) (g . x) ) & dom b_{2} = (dom f) /\ (dom g) & ( for x being set st x in dom b_{2} holds

b_{2} . x = (f . x) (#) (g . x) ) holds

b_{1} = b_{2}

end;
let f be Y1 -valued Function;

let g be Y2 -valued Function;

deffunc H

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 ( dom it = (dom f) /\ (dom g) & ( for x being set st x in dom it holds

it . x = (f . x) (#) (g . x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

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

for Y1, Y2 being complex-functions-membered set

for f being b_{1} -valued Function

for g being b_{2} -valued Function

for b_{5} being Function holds

( b_{5} = f <##> g iff ( dom b_{5} = (dom f) /\ (dom g) & ( for x being set st x in dom b_{5} holds

b_{5} . x = (f . x) (#) (g . x) ) ) );

for Y1, Y2 being complex-functions-membered set

for f being b

for g being b

for b

( b

b

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

f <##> g is PartFunc of (X1 /\ X2),(C_PFuncs ((DOMS Y1) /\ (DOMS Y2)))

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

f <##> g is PartFunc of (X1 /\ X2),(C_PFuncs ((DOMS Y1) /\ (DOMS Y2)))

proof 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

f <##> g is PartFunc of (X1 /\ X2),(R_PFuncs ((DOMS Y1) /\ (DOMS Y2)))

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

f <##> g is PartFunc of (X1 /\ X2),(R_PFuncs ((DOMS Y1) /\ (DOMS Y2)))

proof 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

f <##> g is PartFunc of (X1 /\ X2),(Q_PFuncs ((DOMS Y1) /\ (DOMS Y2)))

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

f <##> g is PartFunc of (X1 /\ X2),(Q_PFuncs ((DOMS Y1) /\ (DOMS Y2)))

proof 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

f <##> g is PartFunc of (X1 /\ X2),(I_PFuncs ((DOMS Y1) /\ (DOMS Y2)))

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

f <##> g is PartFunc of (X1 /\ X2),(I_PFuncs ((DOMS Y1) /\ (DOMS Y2)))

proof 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

f <##> g is PartFunc of (X1 /\ X2),(N_PFuncs ((DOMS Y1) /\ (DOMS Y2)))

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

f <##> g is PartFunc of (X1 /\ X2),(N_PFuncs ((DOMS Y1) /\ (DOMS Y2)))

proof 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

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)

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)

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)

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)

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)

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)

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)

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 Y1, Y2 be complex-functions-membered set ;

let f be Y1 -valued Function;

let g be Y2 -valued Function;

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

ex b_{1} being Function st

( dom b_{1} = (dom f) /\ (dom g) & ( for x being set st x in dom b_{1} holds

b_{1} . x = (f . x) /" (g . x) ) )

for b_{1}, b_{2} being Function st dom b_{1} = (dom f) /\ (dom g) & ( for x being set st x in dom b_{1} holds

b_{1} . x = (f . x) /" (g . x) ) & dom b_{2} = (dom f) /\ (dom g) & ( for x being set st x in dom b_{2} holds

b_{2} . x = (f . x) /" (g . x) ) holds

b_{1} = b_{2}

end;
let f be Y1 -valued Function;

let g be Y2 -valued Function;

deffunc H

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 ( dom it = (dom f) /\ (dom g) & ( for x being set st x in dom it holds

it . x = (f . x) /" (g . x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def48 defines <//> VALUED_2:def 48 :

for Y1, Y2 being complex-functions-membered set

for f being b_{1} -valued Function

for g being b_{2} -valued Function

for b_{5} being Function holds

( b_{5} = f <//> g iff ( dom b_{5} = (dom f) /\ (dom g) & ( for x being set st x in dom b_{5} holds

b_{5} . x = (f . x) /" (g . x) ) ) );

for Y1, Y2 being complex-functions-membered set

for f being b

for g being b

for b

( b

b

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

f <//> g is PartFunc of (X1 /\ X2),(C_PFuncs ((DOMS Y1) /\ (DOMS Y2)))

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

f <//> g is PartFunc of (X1 /\ X2),(C_PFuncs ((DOMS Y1) /\ (DOMS Y2)))

proof 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

f <//> g is PartFunc of (X1 /\ X2),(R_PFuncs ((DOMS Y1) /\ (DOMS Y2)))

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

f <//> g is PartFunc of (X1 /\ X2),(R_PFuncs ((DOMS Y1) /\ (DOMS Y2)))

proof 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

f <//> g is PartFunc of (X1 /\ X2),(Q_PFuncs ((DOMS Y1) /\ (DOMS Y2)))

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

f <//> g is PartFunc of (X1 /\ X2),(Q_PFuncs ((DOMS Y1) /\ (DOMS Y2)))

proof 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)

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)

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)

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

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)

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

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)

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

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)

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;