:: Arithmetic Operations on Functions from Sets into Functional Sets
:: by Artur Korni{\l}owicz
::
:: Received October 15, 2008
:: Copyright (c) 2008-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, FUNCT_1, TARSKI, RELAT_1, SUBSET_1, VALUED_0,
PARTFUN1, FUNCT_2, MEMBERED, XCMPLX_0, ARYTM_3, ARYTM_1, VALUED_1, RAT_1,
FINSEQ_1, NAT_1, COMPLEX1, INT_1, VALUED_2, FUNCOP_1, REAL_1;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
FUNCT_2, ORDINAL1, NUMBERS, FUNCOP_1, BINOP_1, VALUED_0, VALUED_1, INT_1,
NAT_1, XCMPLX_0, XREAL_0, RAT_1, MEMBERED, FINSEQ_1;
constructors RELAT_2, PARTFUN1, MCART_1, FUNCT_2, VALUED_0, VALUED_1, NAT_1,
ARYTM_0, XCMPLX_0, FINSEQ_1, ARYTM_2, NUMBERS, XXREAL_0, XREAL_0,
COMPLEX1, RELSET_1, FUNCOP_1, BINOP_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, VALUED_0, VALUED_1, RELSET_1,
MEMBERED, ORDINAL1, XCMPLX_0, NUMBERS, RAT_1, XREAL_0, INT_1;
requirements SUBSET, BOOLE, NUMERALS, ARITHM;
definitions TARSKI, FUNCT_1, FUNCOP_1;
equalities XCMPLX_0, VALUED_1, BINOP_1, ORDINAL1;
expansions TARSKI;
theorems TARSKI, SUBSET_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, VALUED_1,
XCMPLX_1, XBOOLE_0, XBOOLE_1, RFUNCT_1, FINSEQ_1, RELAT_1, ZFMISC_1,
XCMPLX_0, XREAL_0, RAT_1, INT_1, ORDINAL1;
schemes XBOOLE_0, FUNCT_1, CLASSES1;
begin :: Functional sets
reserve x, y for object, X, X1, X2 for set;
Lm1: now
let X1,X2,X3 be set;
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;
end;
definition
let Y be functional set;
func DOMS(Y) -> set equals
union the set of all dom f where f is Element of Y;
coherence;
end;
definition
let X;
attr X is complex-functions-membered means
:Def2:
x in X implies x is complex-valued Function;
end;
definition
let X;
attr X is ext-real-functions-membered means
:Def3:
x in X implies x is ext-real-valued Function;
end;
definition
let X;
attr X is real-functions-membered means
:Def4:
x in X implies x is real-valued Function;
end;
definition
let X;
attr X is rational-functions-membered means
:Def5:
x in X implies x is RAT-valued Function;
end;
definition
let X;
attr X is integer-functions-membered means
:Def6:
x in X implies x is INT-valued Function;
end;
definition
let X;
attr X is natural-functions-membered means
:Def7:
x in X implies x is natural-valued Function;
end;
registration
cluster natural-functions-membered -> integer-functions-membered for set;
coherence
proof
let X;
assume
A1: for x being object st x in X holds x is natural-valued Function;
let x;
assume x in X;
then x is natural-valued Function by A1;
hence thesis;
end;
cluster integer-functions-membered -> rational-functions-membered for set;
coherence
proof
let X;
assume
A2: for x being object st x in X holds x is INT-valued Function;
let x;
assume x in X;
then x is INT-valued Function by A2;
hence thesis;
end;
cluster rational-functions-membered -> real-functions-membered for set;
coherence;
cluster real-functions-membered -> complex-functions-membered for set;
coherence;
cluster real-functions-membered -> ext-real-functions-membered for set;
coherence;
end;
registration
cluster empty -> natural-functions-membered for set;
coherence;
end;
registration
let f be complex-valued Function;
cluster {f} -> complex-functions-membered;
coherence
by TARSKI:def 1;
end;
registration
cluster complex-functions-membered -> functional for set;
coherence
proof
let X;
assume
A1: X is complex-functions-membered;
let x;
thus thesis by A1;
end;
cluster ext-real-functions-membered -> functional for set;
coherence
proof
let X;
assume
A2: X is ext-real-functions-membered;
let x;
thus thesis by A2;
end;
end;
set ff = the natural-valued Function;
registration
cluster natural-functions-membered non empty for set;
existence
proof
take {ff};
thus for x being object st x in {ff} holds x is natural-valued Function by
TARSKI:def 1;
thus thesis;
end;
end;
registration
let X be complex-functions-membered set;
cluster -> complex-functions-membered for Subset of X;
coherence
by Def2;
end;
registration
let X be ext-real-functions-membered set;
cluster -> ext-real-functions-membered for Subset of X;
coherence
by Def3;
end;
registration
let X be real-functions-membered set;
cluster -> real-functions-membered for Subset of X;
coherence
by Def4;
end;
registration
let X be rational-functions-membered set;
cluster -> rational-functions-membered for Subset of X;
coherence
by Def5;
end;
registration
let X be integer-functions-membered set;
cluster -> integer-functions-membered for Subset of X;
coherence
by Def6;
end;
registration
let X be natural-functions-membered set;
cluster -> natural-functions-membered for Subset of X;
coherence
by Def7;
end;
definition
set A = COMPLEX;
let D be set;
defpred P[object] means $1 is PartFunc of D,A;
func C_PFuncs(D) -> set means
:Def8:
for f being object holds f in it iff f is PartFunc of D,COMPLEX;
existence
proof
consider X being set such that
A1: for x being object holds x in X iff x in PFuncs(D,A) & P[x] from
XBOOLE_0:sch 1;
take X;
let f be object;
thus f in X implies f is PartFunc of D,A by A1;
assume
A2: f is PartFunc of D,A;
then f in PFuncs(D,A) by PARTFUN1:45;
hence thesis by A1,A2;
end;
uniqueness
proof
let P, Q be set;
assume for f being object holds f in P iff f is PartFunc of D,A;
then
A3: for f being object holds f in P iff P[f];
assume for f being object holds f in Q iff f is PartFunc of D,A;
then
A4: for f being object holds f in Q iff P[f];
thus P = Q from XBOOLE_0:sch 2(A3,A4);
end;
end;
definition
set A = COMPLEX;
let D be set;
defpred P[object] means $1 is Function of D,A;
func C_Funcs(D) -> set means
:Def9:
for f being object holds f in it iff f is Function of D,COMPLEX;
existence
proof
consider X being set such that
A1: for x being object holds x in X iff x in Funcs(D,A) & P[x] from
XBOOLE_0:sch 1;
take X;
let f be object;
thus f in X implies f is Function of D,A by A1;
assume
A2: f is Function of D,A;
then f in Funcs(D,A) by FUNCT_2:8;
hence thesis by A1,A2;
end;
uniqueness
proof
let P, Q be set;
assume for f being object holds f in P iff f is Function of D,A;
then
A3: for f being object holds f in P iff P[f];
assume for f being object holds f in Q iff f is Function of D,A;
then
A4: for f being object holds f in Q iff P[f];
thus P = Q from XBOOLE_0:sch 2(A3,A4);
end;
end;
definition
set A = ExtREAL;
let D be set;
defpred P[object] means $1 is PartFunc of D,A;
func E_PFuncs(D) -> set means
:Def10:
for f being object holds f in it iff f is PartFunc of D,ExtREAL;
existence
proof
consider X being set such that
A1: for x being object holds x in X iff x in PFuncs(D,A) & P[x] from
XBOOLE_0:sch 1;
take X;
let f be object;
thus f in X implies f is PartFunc of D,A by A1;
assume
A2: f is PartFunc of D,A;
then f in PFuncs(D,A) by PARTFUN1:45;
hence thesis by A1,A2;
end;
uniqueness
proof
let P, Q be set;
assume for f being object holds f in P iff f is PartFunc of D,A;
then
A3: for f being object holds f in P iff P[f];
assume for f being object holds f in Q iff f is PartFunc of D,A;
then
A4: for f being object holds f in Q iff P[f];
thus P = Q from XBOOLE_0:sch 2(A3,A4);
end;
end;
definition
set A = ExtREAL;
let D be set;
defpred P[object] means $1 is Function of D,A;
func E_Funcs(D) -> set means
:Def11:
for f being object holds f in it iff f is Function of D,ExtREAL;
existence
proof
consider X being set such that
A1: for x being object holds x in X iff x in Funcs(D,A) & P[x] from
XBOOLE_0:sch 1;
take X;
let f be object;
thus f in X implies f is Function of D,A by A1;
assume
A2: f is Function of D,A;
then f in Funcs(D,A) by FUNCT_2:8;
hence thesis by A1,A2;
end;
uniqueness
proof
let P, Q be set;
assume for f being object holds f in P iff f is Function of D,A;
then
A3: for f being object holds f in P iff P[f];
assume for f being object holds f in Q iff f is Function of D,A;
then
A4: for f being object holds f in Q iff P[f];
thus P = Q from XBOOLE_0:sch 2(A3,A4);
end;
end;
definition
set A = REAL;
let D be set;
defpred P[object] means $1 is PartFunc of D,A;
func R_PFuncs(D) -> set means
:Def12:
for f being object holds f in it iff f is PartFunc of D,REAL;
existence
proof
consider X being set such that
A1: for x being object holds x in X iff x in PFuncs(D,A) & P[x] from
XBOOLE_0:sch 1;
take X;
let f be object;
thus f in X implies f is PartFunc of D,A by A1;
assume
A2: f is PartFunc of D,A;
then f in PFuncs(D,A) by PARTFUN1:45;
hence thesis by A1,A2;
end;
uniqueness
proof
let P, Q be set;
assume for f being object holds f in P iff f is PartFunc of D,A;
then
A3: for f being object holds f in P iff P[f];
assume for f being object holds f in Q iff f is PartFunc of D,A;
then
A4: for f being object holds f in Q iff P[f];
thus P = Q from XBOOLE_0:sch 2(A3,A4);
end;
end;
definition
set A = REAL;
let D be set;
defpred P[object] means $1 is Function of D,A;
func R_Funcs(D) -> set means
:Def13:
for f being object holds f in it iff f is Function of D,REAL;
existence
proof
consider X being set such that
A1: for x being object holds x in X iff x in Funcs(D,A) & P[x] from
XBOOLE_0:sch 1;
take X;
let f be object;
thus f in X implies f is Function of D,A by A1;
assume
A2: f is Function of D,A;
then f in Funcs(D,A) by FUNCT_2:8;
hence thesis by A1,A2;
end;
uniqueness
proof
let P, Q be set;
assume for f being object holds f in P iff f is Function of D,A;
then
A3: for f being object holds f in P iff P[f];
assume for f being object holds f in Q iff f is Function of D,A;
then
A4: for f being object holds f in Q iff P[f];
thus P = Q from XBOOLE_0:sch 2(A3,A4);
end;
end;
definition
set A = RAT;
let D be set;
defpred P[object] means $1 is PartFunc of D,A;
func Q_PFuncs(D) -> set means
:Def14:
for f being object holds f in it iff f is PartFunc of D,RAT;
existence
proof
consider X being set such that
A1: for x being object holds x in X iff x in PFuncs(D,A) & P[x] from
XBOOLE_0:sch 1;
take X;
let f be object;
thus f in X implies f is PartFunc of D,A by A1;
assume
A2: f is PartFunc of D,A;
then f in PFuncs(D,A) by PARTFUN1:45;
hence thesis by A1,A2;
end;
uniqueness
proof
let P, Q be set;
assume for f being object holds f in P iff f is PartFunc of D,A;
then
A3: for f being object holds f in P iff P[f];
assume for f being object holds f in Q iff f is PartFunc of D,A;
then
A4: for f being object holds f in Q iff P[f];
thus P = Q from XBOOLE_0:sch 2(A3,A4);
end;
end;
definition
set A = RAT;
let D be set;
defpred P[object] means $1 is Function of D,A;
func Q_Funcs(D) -> set means
:Def15:
for f being object holds f in it iff f is Function of D,RAT;
existence
proof
consider X being set such that
A1: for x being object holds x in X iff x in Funcs(D,A) & P[x] from
XBOOLE_0:sch 1;
take X;
let f be object;
thus f in X implies f is Function of D,A by A1;
assume
A2: f is Function of D,A;
then f in Funcs(D,A) by FUNCT_2:8;
hence thesis by A1,A2;
end;
uniqueness
proof
let P, Q be set;
assume for f being object holds f in P iff f is Function of D,A;
then
A3: for f being object holds f in P iff P[f];
assume for f being object holds f in Q iff f is Function of D,A;
then
A4: for f being object holds f in Q iff P[f];
thus P = Q from XBOOLE_0:sch 2(A3,A4);
end;
end;
definition
set A = INT;
let D be set;
defpred P[object] means $1 is PartFunc of D,A;
func I_PFuncs(D) -> set means
:Def16:
for f being object holds f in it iff f is PartFunc of D,INT;
existence
proof
consider X being set such that
A1: for x being object holds x in X iff x in PFuncs(D,A) & P[x] from
XBOOLE_0:sch 1;
take X;
let f be object;
thus f in X implies f is PartFunc of D,A by A1;
assume
A2: f is PartFunc of D,A;
then f in PFuncs(D,A) by PARTFUN1:45;
hence thesis by A1,A2;
end;
uniqueness
proof
let P, Q be set;
assume for f being object holds f in P iff f is PartFunc of D,A;
then
A3: for f being object holds f in P iff P[f];
assume for f being object holds f in Q iff f is PartFunc of D,A;
then
A4: for f being object holds f in Q iff P[f];
thus P = Q from XBOOLE_0:sch 2(A3,A4);
end;
end;
definition
set A = INT;
let D be set;
defpred P[object] means $1 is Function of D,A;
func I_Funcs(D) -> set means
:Def17:
for f being object holds f in it iff f is Function of D,INT;
existence
proof
consider X being set such that
A1: for x being object holds x in X iff x in Funcs(D,A) & P[x] from
XBOOLE_0:sch 1;
take X;
let f be object;
thus f in X implies f is Function of D,A by A1;
assume
A2: f is Function of D,A;
then f in Funcs(D,A) by FUNCT_2:8;
hence thesis by A1,A2;
end;
uniqueness
proof
let P, Q be set;
assume for f being object holds f in P iff f is Function of D,A;
then
A3: for f being object holds f in P iff P[f];
assume for f being object holds f in Q iff f is Function of D,A;
then
A4: for f being object holds f in Q iff P[f];
thus P = Q from XBOOLE_0:sch 2(A3,A4);
end;
end;
definition
set A = NAT;
let D be set;
defpred P[object] means $1 is PartFunc of D,A;
func N_PFuncs(D) -> set means
:Def18:
for f being object holds f in it iff f is PartFunc of D,NAT;
existence
proof
consider X being set such that
A1: for x being object holds x in X iff x in PFuncs(D,A) & P[x] from
XBOOLE_0:sch 1;
take X;
let f be object;
thus f in X implies f is PartFunc of D,A by A1;
assume
A2: f is PartFunc of D,A;
then f in PFuncs(D,A) by PARTFUN1:45;
hence thesis by A1,A2;
end;
uniqueness
proof
let P, Q be set;
assume for f being object holds f in P iff f is PartFunc of D,A;
then
A3: for f being object holds f in P iff P[f];
assume for f being object holds f in Q iff f is PartFunc of D,A;
then
A4: for f being object holds f in Q iff P[f];
thus P = Q from XBOOLE_0:sch 2(A3,A4);
end;
end;
definition
set A = NAT;
let D be set;
defpred P[object] means $1 is Function of D,A;
func N_Funcs(D) -> set means
:Def19:
for f being object holds f in it iff f is Function of D,NAT;
existence
proof
consider X being set such that
A1: for x being object holds x in X iff x in Funcs(D,A) & P[x] from
XBOOLE_0:sch 1;
take X;
let f be object;
thus f in X implies f is Function of D,A by A1;
assume
A2: f is Function of D,A;
then f in Funcs(D,A) by FUNCT_2:8;
hence thesis by A1,A2;
end;
uniqueness
proof
let P, Q be set;
assume for f being object holds f in P iff f is Function of D,A;
then
A3: for f being object holds f in P iff P[f];
assume for f being object holds f in Q iff f is Function of D,A;
then
A4: for f being object holds f in Q iff P[f];
thus P = Q from XBOOLE_0:sch 2(A3,A4);
end;
end;
theorem Th1:
C_Funcs(X) is Subset of C_PFuncs(X)
proof
C_Funcs(X) c= C_PFuncs(X)
proof
let x be object;
assume x in C_Funcs(X);
then x is Function of X,COMPLEX by Def9;
hence thesis by Def8;
end;
hence thesis;
end;
theorem Th2:
E_Funcs(X) is Subset of E_PFuncs(X)
proof
E_Funcs(X) c= E_PFuncs(X)
proof
let x be object;
assume x in E_Funcs(X);
then x is Function of X,ExtREAL by Def11;
hence thesis by Def10;
end;
hence thesis;
end;
theorem Th3:
R_Funcs(X) is Subset of R_PFuncs(X)
proof
R_Funcs(X) c= R_PFuncs(X)
proof
let x be object;
assume x in R_Funcs(X);
then x is Function of X,REAL by Def13;
hence thesis by Def12;
end;
hence thesis;
end;
theorem Th4:
Q_Funcs(X) is Subset of Q_PFuncs(X)
proof
Q_Funcs(X) c= Q_PFuncs(X)
proof
let x be object;
assume x in Q_Funcs(X);
then x is Function of X,RAT by Def15;
hence thesis by Def14;
end;
hence thesis;
end;
theorem Th5:
I_Funcs(X) is Subset of I_PFuncs(X)
proof
I_Funcs(X) c= I_PFuncs(X)
proof
let x be object;
assume x in I_Funcs(X);
then x is Function of X,INT by Def17;
hence thesis by Def16;
end;
hence thesis;
end;
theorem Th6:
N_Funcs(X) is Subset of N_PFuncs(X)
proof
N_Funcs(X) c= N_PFuncs(X)
proof
let x be object;
assume x in N_Funcs(X);
then x is Function of X,NAT by Def19;
hence thesis by Def18;
end;
hence thesis;
end;
registration
let X;
cluster C_PFuncs(X) -> complex-functions-membered;
coherence
by Def8;
cluster C_Funcs(X) -> complex-functions-membered;
coherence
proof
reconsider C = C_Funcs(X) as Subset of C_PFuncs(X) by Th1;
C is complex-functions-membered;
hence thesis;
end;
cluster E_PFuncs(X) -> ext-real-functions-membered;
coherence
by Def10;
cluster E_Funcs(X) -> ext-real-functions-membered;
coherence
proof
reconsider C = E_Funcs(X) as Subset of E_PFuncs(X) by Th2;
C is ext-real-functions-membered;
hence thesis;
end;
cluster R_PFuncs(X) -> real-functions-membered;
coherence
by Def12;
cluster R_Funcs(X) -> real-functions-membered;
coherence
proof
reconsider C = R_Funcs(X) as Subset of R_PFuncs(X) by Th3;
C is real-functions-membered;
hence thesis;
end;
cluster Q_PFuncs(X) -> rational-functions-membered;
coherence
by Def14;
cluster Q_Funcs(X) -> rational-functions-membered;
coherence
proof
reconsider C = Q_Funcs(X) as Subset of Q_PFuncs(X) by Th4;
C is rational-functions-membered;
hence thesis;
end;
cluster I_PFuncs(X) -> integer-functions-membered;
coherence
by Def16;
cluster I_Funcs(X) -> integer-functions-membered;
coherence
proof
reconsider C = I_Funcs(X) as Subset of I_PFuncs(X) by Th5;
C is integer-functions-membered;
hence thesis;
end;
cluster N_PFuncs(X) -> natural-functions-membered;
coherence
by Def18;
cluster N_Funcs(X) -> natural-functions-membered;
coherence
proof
reconsider C = N_Funcs(X) as Subset of N_PFuncs(X) by Th6;
C is natural-functions-membered;
hence thesis;
end;
end;
registration
let X be complex-functions-membered set;
cluster -> complex-valued for Element of X;
coherence
proof
X is empty or X is non empty;
hence thesis by Def2,SUBSET_1:def 1;
end;
end;
registration
let X be ext-real-functions-membered set;
cluster -> ext-real-valued for Element of X;
coherence
proof
X is empty or X is non empty;
hence thesis by Def3,SUBSET_1:def 1;
end;
end;
registration
let X be real-functions-membered set;
cluster -> real-valued for Element of X;
coherence
proof
X is empty or X is non empty;
hence thesis by Def4,SUBSET_1:def 1;
end;
end;
registration
let X be rational-functions-membered set;
cluster -> RAT-valued for Element of X;
coherence
proof
X is empty or X is non empty;
hence thesis by Def5,SUBSET_1:def 1;
end;
end;
registration
let X be integer-functions-membered set;
cluster -> INT-valued for Element of X;
coherence
proof
X is empty or X is non empty;
hence thesis by Def6,SUBSET_1:def 1;
end;
end;
registration
let X be natural-functions-membered set;
cluster -> natural-valued for Element of X;
coherence
proof
X is empty or X is non empty;
hence thesis by Def7,SUBSET_1:def 1;
end;
end;
registration
let X be set, x be object;
let Y be complex-functions-membered set;
let f be PartFunc of X,Y;
cluster f.x -> Function-like Relation-like;
coherence;
end;
registration
let X be set, x be object;
let Y be ext-real-functions-membered set;
let f be PartFunc of X,Y;
cluster f.x -> Function-like Relation-like;
coherence;
end;
registration
let X be set, x be object;
let Y be complex-functions-membered set;
let f be PartFunc of X,Y;
cluster f.x -> complex-valued;
coherence
proof
per cases;
suppose
x in dom f;
then f.x in rng f by FUNCT_1:def 3;
hence thesis;
end;
suppose
not x in dom f;
hence thesis by FUNCT_1:def 2;
end;
end;
end;
registration
let X be set, x be object;
let Y be ext-real-functions-membered set;
let f be PartFunc of X,Y;
cluster f.x -> ext-real-valued;
coherence
proof
per cases;
suppose
x in dom f;
then f.x in rng f by FUNCT_1:def 3;
hence thesis;
end;
suppose
not x in dom f;
hence thesis by FUNCT_1:def 2;
end;
end;
end;
registration
let X be set, x be object;
let Y be real-functions-membered set;
let f be PartFunc of X,Y;
cluster f.x -> real-valued;
coherence
proof
per cases;
suppose
x in dom f;
then f.x in rng f by FUNCT_1:def 3;
hence thesis;
end;
suppose
not x in dom f;
hence thesis by FUNCT_1:def 2;
end;
end;
end;
registration
let X be set, x be object;
let Y be rational-functions-membered set;
let f be PartFunc of X,Y;
cluster f.x -> RAT-valued;
coherence
proof
per cases;
suppose
x in dom f;
then f.x in rng f by FUNCT_1:def 3;
hence thesis;
end;
suppose
not x in dom f;
hence thesis by FUNCT_1:def 2;
end;
end;
end;
registration
let X be set, x be object;
let Y be integer-functions-membered set;
let f be PartFunc of X,Y;
cluster f.x -> INT-valued;
coherence
proof
per cases;
suppose
x in dom f;
then f.x in rng f by FUNCT_1:def 3;
hence thesis;
end;
suppose
not x in dom f;
hence thesis by FUNCT_1:def 2;
end;
end;
end;
registration
let X be set, x be object;
let Y be natural-functions-membered set;
let f be PartFunc of X,Y;
cluster f.x -> natural-valued;
coherence
proof
per cases;
suppose
x in dom f;
then f.x in rng f by FUNCT_1:def 3;
hence thesis;
end;
suppose
not x in dom f;
hence thesis by FUNCT_1:def 2;
end;
end;
end;
registration
let X;
let Y be complex-membered set;
cluster PFuncs(X,Y) -> complex-functions-membered;
coherence
proof
let x;
assume x in PFuncs(X,Y);
then consider f being Function such that
A1: x = f and
A2: dom f c= X & rng f c= Y by PARTFUN1:def 3;
reconsider f as PartFunc of X,Y by A2,RELSET_1:4;
f is set;
hence thesis by A1;
end;
end;
registration
let X;
let Y be ext-real-membered set;
cluster PFuncs(X,Y) -> ext-real-functions-membered;
coherence
proof
let x;
assume x in PFuncs(X,Y);
then consider f being Function such that
A1: x = f and
A2: dom f c= X & rng f c= Y by PARTFUN1:def 3;
reconsider f as PartFunc of X,Y by A2,RELSET_1:4;
f is set;
hence thesis by A1;
end;
end;
registration
let X;
let Y be real-membered set;
cluster PFuncs(X,Y) -> real-functions-membered;
coherence
proof
let x;
assume x in PFuncs(X,Y);
then consider f being Function such that
A1: x = f and
A2: dom f c= X & rng f c= Y by PARTFUN1:def 3;
reconsider f as PartFunc of X,Y by A2,RELSET_1:4;
f is set;
hence thesis by A1;
end;
end;
registration
let X;
let Y be rational-membered set;
cluster PFuncs(X,Y) -> rational-functions-membered;
coherence
proof
let x;
assume x in PFuncs(X,Y);
then consider f being Function such that
A1: x = f and
A2: dom f c= X & rng f c= Y by PARTFUN1:def 3;
reconsider f as PartFunc of X,Y by A2,RELSET_1:4;
f is set;
hence thesis by A1;
end;
end;
registration
let X;
let Y be integer-membered set;
cluster PFuncs(X,Y) -> integer-functions-membered;
coherence
proof
let x;
assume x in PFuncs(X,Y);
then consider f being Function such that
A1: x = f and
A2: dom f c= X & rng f c= Y by PARTFUN1:def 3;
reconsider f as PartFunc of X,Y by A2,RELSET_1:4;
f is set;
hence thesis by A1;
end;
end;
registration
let X;
let Y be natural-membered set;
cluster PFuncs(X,Y) -> natural-functions-membered;
coherence
proof
let x;
assume x in PFuncs(X,Y);
then consider f being Function such that
A1: x = f and
A2: dom f c= X & rng f c= Y by PARTFUN1:def 3;
reconsider f as PartFunc of X,Y by A2,RELSET_1:4;
f is set;
hence thesis by A1;
end;
end;
registration
let X;
let Y be complex-membered set;
cluster Funcs(X,Y) -> complex-functions-membered;
coherence
proof
let x;
assume x in Funcs(X,Y);
then consider f being Function such that
A1: x = f and
A2: dom f = X & rng f c= Y by FUNCT_2:def 2;
reconsider f as PartFunc of X,Y by A2,RELSET_1:4;
f is set;
hence thesis by A1;
end;
end;
registration
let X;
let Y be ext-real-membered set;
cluster Funcs(X,Y) -> ext-real-functions-membered;
coherence
proof
let x;
assume x in Funcs(X,Y);
then consider f being Function such that
A1: x = f and
A2: dom f = X & rng f c= Y by FUNCT_2:def 2;
reconsider f as PartFunc of X,Y by A2,RELSET_1:4;
f is set;
hence thesis by A1;
end;
end;
registration
let X;
let Y be real-membered set;
cluster Funcs(X,Y) -> real-functions-membered;
coherence
proof
let x;
assume x in Funcs(X,Y);
then consider f being Function such that
A1: x = f and
A2: dom f = X & rng f c= Y by FUNCT_2:def 2;
reconsider f as PartFunc of X,Y by A2,RELSET_1:4;
f is set;
hence thesis by A1;
end;
end;
registration
let X;
let Y be rational-membered set;
cluster Funcs(X,Y) -> rational-functions-membered;
coherence
proof
let x;
assume x in Funcs(X,Y);
then consider f being Function such that
A1: x = f and
A2: dom f = X & rng f c= Y by FUNCT_2:def 2;
reconsider f as PartFunc of X,Y by A2,RELSET_1:4;
f is set;
hence thesis by A1;
end;
end;
registration
let X;
let Y be integer-membered set;
cluster Funcs(X,Y) -> integer-functions-membered;
coherence
proof
let x;
assume x in Funcs(X,Y);
then consider f being Function such that
A1: x = f and
A2: dom f = X & rng f c= Y by FUNCT_2:def 2;
reconsider f as PartFunc of X,Y by A2,RELSET_1:4;
f is set;
hence thesis by A1;
end;
end;
registration
let X;
let Y be natural-membered set;
cluster Funcs(X,Y) -> natural-functions-membered;
coherence
proof
let x;
assume x in Funcs(X,Y);
then consider f being Function such that
A1: x = f and
A2: dom f = X & rng f c= Y by FUNCT_2:def 2;
reconsider f as PartFunc of X,Y by A2,RELSET_1:4;
f is set;
hence thesis by A1;
end;
end;
definition
let R be Relation;
attr R is complex-functions-valued means
:Def20:
rng R is complex-functions-membered;
attr R is ext-real-functions-valued means
:Def21:
rng R is ext-real-functions-membered;
attr R is real-functions-valued means
:Def22:
rng R is real-functions-membered;
attr R is rational-functions-valued means
:Def23:
rng R is rational-functions-membered;
attr R is integer-functions-valued means
:Def24:
rng R is integer-functions-membered;
attr R is natural-functions-valued means
:Def25:
rng R is natural-functions-membered;
end;
registration
let Y be complex-functions-membered set;
cluster -> complex-functions-valued for Y-valued Function;
coherence
proof let f be Y-valued Function;
thus rng f is complex-functions-membered;
end;
end;
definition
let f be Function;
redefine attr f is complex-functions-valued means :: redefines complex-functions-valued (VALUED_2, definition)
for x being object st x in dom f holds f.x is complex-valued Function;
compatibility
proof
thus f is complex-functions-valued implies
for x being object st x in dom f
holds f.x is complex-valued Function
proof
assume
A1: rng f is complex-functions-membered;
let x;
assume x in dom f;
then f.x in rng f by FUNCT_1:def 3;
hence thesis by A1;
end;
assume
A2: for x being object st x in dom f holds f.x is complex-valued Function;
let y be object;
assume y in rng f;
then ex x being object st x in dom f & f.x = y by FUNCT_1:def 3;
hence thesis by A2;
end;
redefine attr f is ext-real-functions-valued means :: redefines ext-real-functions-valued (VALUED_2, definition)
for x being object st x in dom f holds f.x is ext-real-valued Function;
compatibility
proof
thus f is ext-real-functions-valued implies
for x being object st x in dom f
holds f.x is ext-real-valued Function
proof
assume
A3: rng f is ext-real-functions-membered;
let x;
assume x in dom f;
then f.x in rng f by FUNCT_1:def 3;
hence thesis by A3;
end;
assume
A4: for x being object st x in dom f holds f.x is ext-real-valued Function;
let y be object;
assume y in rng f;
then ex x being object st x in dom f & f.x = y by FUNCT_1:def 3;
hence thesis by A4;
end;
redefine attr f is real-functions-valued means :: redefines real-functions-valued (VALUED_2, definition)
for x being object st x in dom f holds f.x is real-valued Function;
compatibility
proof
thus f is real-functions-valued implies
for x being object st x in dom f
holds f.x is real-valued Function
proof
assume
A5: rng f is real-functions-membered;
let x;
assume x in dom f;
then f.x in rng f by FUNCT_1:def 3;
hence thesis by A5;
end;
assume
A6: for x being object st x in dom f holds f.x is real-valued Function;
let y be object;
assume y in rng f;
then ex x being object st x in dom f & f.x = y by FUNCT_1:def 3;
hence thesis by A6;
end;
redefine attr f is rational-functions-valued means :: redefines rational-functions-valued (VALUED_2, definition)
for x being object st x in dom f holds f.x is RAT-valued Function;
compatibility
proof
thus f is rational-functions-valued implies
for x being object st x in dom f
holds f.x is RAT-valued Function
proof
assume
A7: rng f is rational-functions-membered;
let x;
assume x in dom f;
then f.x in rng f by FUNCT_1:def 3;
hence thesis by A7;
end;
assume
A8: for x being object st x in dom f holds f.x is RAT-valued Function;
let y be object;
assume y in rng f;
then ex x being object st x in dom f & f.x = y by FUNCT_1:def 3;
hence thesis by A8;
end;
redefine attr f is integer-functions-valued means :: redefines integer-functions-valued (VALUED_2, definition)
for x being object st x in dom f holds f.x is INT-valued Function;
compatibility
proof
thus f is integer-functions-valued implies
for x being object st x in dom f
holds f.x is INT-valued Function
proof
assume
A9: rng f is integer-functions-membered;
let x;
assume x in dom f;
then f.x in rng f by FUNCT_1:def 3;
hence thesis by A9;
end;
assume
A10: for x being object st x in dom f holds f.x is INT-valued Function;
let y be object;
assume y in rng f;
then ex x being object st x in dom f & f.x = y by FUNCT_1:def 3;
hence thesis by A10;
end;
redefine attr f is natural-functions-valued means :: redefines natural-functions-valued (VALUED_2, definition)
for x being object st x in dom f holds f.x is natural-valued Function;
compatibility
proof
thus f is natural-functions-valued implies
for x being object st x in dom f
holds f.x is natural-valued Function
proof
assume
A11: rng f is natural-functions-membered;
let x;
assume x in dom f;
then f.x in rng f by FUNCT_1:def 3;
hence thesis by A11;
end;
assume
A12: for x being object st x in dom f holds f.x is natural-valued Function;
let y be object;
assume y in rng f;
then ex x being object st x in dom f & f.x = y by FUNCT_1:def 3;
hence thesis by A12;
end;
end;
registration
cluster natural-functions-valued -> integer-functions-valued for Relation;
coherence;
cluster integer-functions-valued -> rational-functions-valued for Relation;
coherence;
cluster rational-functions-valued -> real-functions-valued for Relation;
coherence;
cluster real-functions-valued -> ext-real-functions-valued for Relation;
coherence;
cluster real-functions-valued -> complex-functions-valued for Relation;
coherence;
end;
registration
cluster empty -> natural-functions-valued for Relation;
coherence;
end;
registration
cluster natural-functions-valued for Function;
existence
proof
take {};
thus thesis;
end;
end;
registration
let R be complex-functions-valued Relation;
cluster rng R -> complex-functions-membered;
coherence by Def20;
end;
registration
let R be ext-real-functions-valued Relation;
cluster rng R -> ext-real-functions-membered;
coherence by Def21;
end;
registration
let R be real-functions-valued Relation;
cluster rng R -> real-functions-membered;
coherence by Def22;
end;
registration
let R be rational-functions-valued Relation;
cluster rng R -> rational-functions-membered;
coherence by Def23;
end;
registration
let R be integer-functions-valued Relation;
cluster rng R -> integer-functions-membered;
coherence by Def24;
end;
registration
let R be natural-functions-valued Relation;
cluster rng R -> natural-functions-membered;
coherence by Def25;
end;
registration
let X;
let Y be complex-functions-membered set;
cluster -> complex-functions-valued for PartFunc of X,Y;
coherence;
end;
registration
let X;
let Y be ext-real-functions-membered set;
cluster -> ext-real-functions-valued for PartFunc of X,Y;
coherence;
end;
registration
let X;
let Y be real-functions-membered set;
cluster -> real-functions-valued for PartFunc of X,Y;
coherence;
end;
registration
let X;
let Y be rational-functions-membered set;
cluster -> rational-functions-valued for PartFunc of X,Y;
coherence;
end;
registration
let X;
let Y be integer-functions-membered set;
cluster -> integer-functions-valued for PartFunc of X,Y;
coherence;
end;
registration
let X;
let Y be natural-functions-membered set;
cluster -> natural-functions-valued for PartFunc of X,Y;
coherence;
end;
registration
cluster complex-functions-valued -> Function-yielding for Function;
coherence
proof let f be Function such that
A1: f is complex-functions-valued;
let x be object;
thus thesis by A1;
end;
cluster real-functions-valued -> Function-yielding for Function;
coherence;
cluster ext-real-functions-valued -> Function-yielding for Function;
coherence
proof let f be Function such that
A2: f is ext-real-functions-valued;
let x be object;
thus thesis by A2;
end;
end;
registration
let f be complex-functions-valued Function;
let x be object;
cluster f.x -> Function-like Relation-like;
coherence
proof
per cases;
suppose
x in dom f;
then f.x in rng f by FUNCT_1:def 3;
hence thesis;
end;
suppose
not x in dom f;
hence thesis by FUNCT_1:def 2;
end;
end;
end;
registration
let f be ext-real-functions-valued Function;
let x be object;
cluster f.x -> Function-like Relation-like;
coherence
proof
per cases;
suppose
x in dom f;
then f.x in rng f by FUNCT_1:def 3;
hence thesis;
end;
suppose
not x in dom f;
hence thesis by FUNCT_1:def 2;
end;
end;
end;
registration
let f be complex-functions-valued Function;
let x be object;
cluster f.x -> complex-valued;
coherence
proof
per cases;
suppose
x in dom f;
then f.x in rng f by FUNCT_1:def 3;
hence thesis;
end;
suppose
not x in dom f;
hence thesis by FUNCT_1:def 2;
end;
end;
end;
registration
let f be ext-real-functions-valued Function;
let x be object;
cluster f.x -> ext-real-valued;
coherence
proof
per cases;
suppose
x in dom f;
then f.x in rng f by FUNCT_1:def 3;
hence thesis;
end;
suppose
not x in dom f;
hence thesis by FUNCT_1:def 2;
end;
end;
end;
registration
let f be real-functions-valued Function;
let x be object;
cluster f.x -> real-valued;
coherence
proof
per cases;
suppose
x in dom f;
then f.x in rng f by FUNCT_1:def 3;
hence thesis;
end;
suppose
not x in dom f;
hence thesis by FUNCT_1:def 2;
end;
end;
end;
registration
let f be rational-functions-valued Function;
let x be object;
cluster f.x -> RAT-valued;
coherence
proof
per cases;
suppose
x in dom f;
then f.x in rng f by FUNCT_1:def 3;
hence thesis;
end;
suppose
not x in dom f;
hence thesis by FUNCT_1:def 2;
end;
end;
end;
registration
let f be integer-functions-valued Function;
let x be object;
cluster f.x -> INT-valued;
coherence
proof
per cases;
suppose
x in dom f;
then f.x in rng f by FUNCT_1:def 3;
hence thesis;
end;
suppose
not x in dom f;
hence thesis by FUNCT_1:def 2;
end;
end;
end;
registration
let f be natural-functions-valued Function;
let x be object;
cluster f.x -> natural-valued;
coherence
proof
per cases;
suppose
x in dom f;
then f.x in rng f by FUNCT_1:def 3;
hence thesis;
end;
suppose
not x in dom f;
hence thesis by FUNCT_1:def 2;
end;
end;
end;
registration
let f be real-functions-valued Function;
let x,y;
cluster f.(x,y) -> real-valued for Function;
coherence;
end;
begin :: Operations
reserve Y, Y1, Y2 for complex-functions-membered set,
c, c1, c2 for Complex,
f for PartFunc of X,Y,
f1 for PartFunc of X1,Y1,
f2 for PartFunc of X2, Y2,
g, h, k for complex-valued Function;
theorem Th7:
g <> {} & g + c1 = g + c2 implies c1 = c2
proof
assume that
A1: g <> {} and
A2: g+c1 = g+c2;
consider x being object such that
A3: x in dom g by A1,XBOOLE_0:def 1;
dom g = dom(g+c2) by VALUED_1:def 2;
then
A4: (g+c2).x = g.x+c2 by A3,VALUED_1:def 2;
dom g = dom(g+c1) by VALUED_1:def 2;
then (g+c1).x = g.x+c1 by A3,VALUED_1:def 2;
hence c1 = c2 by A2,A4;
end;
theorem Th8:
g <> {} & g - c1 = g - c2 implies c1 = c2
proof
assume that
A1: g <> {} and
A2: g-c1 = g-c2;
consider x being object such that
A3: x in dom g by A1,XBOOLE_0:def 1;
dom g = dom(g-c2) by VALUED_1:def 2;
then
A4: (g-c2).x = g.x-c2 by A3,VALUED_1:def 2;
dom g = dom(g-c1) by VALUED_1:def 2;
then (g-c1).x = g.x-c1 by A3,VALUED_1:def 2;
hence c1 = c2 by A2,A4;
end;
theorem Th9:
g <> {} & g is non-empty & g (#) c1 = g (#) c2 implies c1 = c2
proof
assume that
A1: g <> {} and
A2: g is non-empty and
A3: g(#)c1 = g(#)c2;
consider x being object such that
A4: x in dom g by A1,XBOOLE_0:def 1;
g.x in rng g by A4,FUNCT_1:def 3;
then
A5: g.x <> {} by A2,RELAT_1:def 9;
(g(#)c1).x = g.x*c1 & (g(#)c2).x = g.x*c2 by VALUED_1:6;
hence c1 = c2 by A3,A5,XCMPLX_1:5;
end;
theorem Th10:
- (g + c) = -g - c
proof
A1: dom -(g+c) = dom(g+c) by VALUED_1:8;
A2: dom(g+c) = dom g & dom(-g-c) = dom -g by VALUED_1:def 2;
hence dom -(g+c) = dom(-g-c) by A1,VALUED_1:8;
let x be object;
assume
A3: x in dom -(g+c);
A4: dom -g = dom g by VALUED_1:8;
thus (-(g+c)).x = -(g+c).x by VALUED_1:8
.= -(g.x+c) by A1,A3,VALUED_1:def 2
.= -g.x-c
.= (-g).x-c by VALUED_1:8
.= (-g-c).x by A2,A1,A4,A3,VALUED_1:def 2;
end;
theorem Th11:
- (g - c) = -g + c
proof
A1: dom -(g-c) = dom(g-c) by VALUED_1:8;
A2: dom(g-c) = dom g & dom(-g+c) = dom -g by VALUED_1:def 2;
hence dom -(g-c) = dom(-g+c) by A1,VALUED_1:8;
let x be object;
assume
A3: x in dom -(g-c);
A4: dom -g = dom g by VALUED_1:8;
thus (-(g-c)).x = -(g-c).x by VALUED_1:8
.= -(g.x-c) by A1,A3,VALUED_1:def 2
.= -g.x+c
.= (-g).x+c by VALUED_1:8
.= (-g+c).x by A2,A1,A4,A3,VALUED_1:def 2;
end;
theorem Th12:
(g + c1) + c2 = g + (c1 + c2)
proof
A1: dom((g+c1)+c2) = dom(g+c1) by VALUED_1:def 2;
A2: dom(g+c1) = dom g by VALUED_1:def 2;
hence dom((g+c1)+c2) = dom(g+(c1+c2)) by A1,VALUED_1:def 2;
let x be object;
A3: dom(g+(c1+c2)) = dom(g) by VALUED_1:def 2;
assume
A4: x in dom((g+c1)+c2);
hence ((g+c1)+c2).x = (g+c1).x+c2 by VALUED_1:def 2
.= g.x+c1+c2 by A1,A4,VALUED_1:def 2
.= g.x+(c1+c2)
.= (g+(c1+c2)).x by A1,A2,A3,A4,VALUED_1:def 2;
end;
theorem Th13:
(g + c1) - c2 = g + (c1 - c2)
proof
A1: dom((g+c1)-c2) = dom(g+c1) by VALUED_1:def 2;
A2: dom(g+c1) = dom g by VALUED_1:def 2;
hence dom((g+c1)-c2) = dom(g+(c1-c2)) by A1,VALUED_1:def 2;
let x be object;
A3: dom(g+(c1-c2)) = dom(g) by VALUED_1:def 2;
assume
A4: x in dom((g+c1)-c2);
hence ((g+c1)-c2).x = (g+c1).x-c2 by VALUED_1:def 2
.= g.x+c1-c2 by A1,A4,VALUED_1:def 2
.= g.x+(c1-c2)
.= (g+(c1-c2)).x by A1,A2,A3,A4,VALUED_1:def 2;
end;
theorem Th14:
(g - c1) + c2 = g - (c1 - c2)
proof
A1: dom((g-c1)+c2) = dom(g-c1) by VALUED_1:def 2;
A2: dom(g-c1) = dom g by VALUED_1:def 2;
hence dom((g-c1)+c2) = dom(g-(c1-c2)) by A1,VALUED_1:def 2;
let x be object;
A3: dom(g-(c1-c2)) = dom(g) by VALUED_1:def 2;
assume
A4: x in dom((g-c1)+c2);
hence ((g-c1)+c2).x = (g-c1).x+c2 by VALUED_1:def 2
.= g.x-c1+c2 by A1,A4,VALUED_1:def 2
.= g.x-(c1-c2)
.= (g-(c1-c2)).x by A1,A2,A3,A4,VALUED_1:def 2;
end;
theorem Th15:
(g - c1) - c2 = g - (c1 + c2)
proof
A1: dom((g-c1)-c2) = dom(g-c1) by VALUED_1:def 2;
A2: dom(g-c1) = dom g by VALUED_1:def 2;
hence dom((g-c1)-c2) = dom(g-(c1+c2)) by A1,VALUED_1:def 2;
let x be object;
A3: dom(g-(c1+c2)) = dom(g) by VALUED_1:def 2;
assume
A4: x in dom((g-c1)-c2);
hence ((g-c1)-c2).x = (g-c1).x-c2 by VALUED_1:def 2
.= g.x-c1-c2 by A1,A4,VALUED_1:def 2
.= g.x-(c1+c2)
.= (g-(c1+c2)).x by A1,A2,A3,A4,VALUED_1:def 2;
end;
theorem Th16:
g (#) c1 (#) c2 = g (#) (c1 * c2)
proof
dom((g(#)c1)(#)c2) = dom(g(#)c1) & dom(g(#)c1) = dom g by VALUED_1:def 5;
hence dom((g(#)c1)(#)c2) = dom(g(#)(c1*c2)) by VALUED_1:def 5;
let x be object;
assume x in dom((g(#)c1)(#)c2);
thus ((g(#)c1)(#)c2).x = (g(#)c1).x*c2 by VALUED_1:6
.= g.x*c1*c2 by VALUED_1:6
.= g.x*(c1*c2)
.= (g(#)(c1*c2)).x by VALUED_1:6;
end;
theorem Th17:
- (g + h) = (-g) - h
proof
A1: dom -(g+h) = dom(g+h) by VALUED_1:8;
dom(g+h) = dom g /\ dom h & dom(-g-h) = dom(-g) /\ dom h by VALUED_1:12,def 1
;
hence
A2: dom -(g+h) = dom(-g-h) by A1,VALUED_1:8;
let x be object;
assume
A3: x in dom -(g+h);
thus (-(g+h)).x = -(g+h).x by VALUED_1:8
.= -(g.x+h.x) by A1,A3,VALUED_1:def 1
.= -g.x-h.x
.= (-g).x-h.x by VALUED_1:8
.= (-g-h).x by A2,A3,VALUED_1:13;
end;
theorem Th18:
g - h = - (h - g)
proof
A1: dom -(h-g) = dom(h-g) by VALUED_1:8;
dom(g-h) = dom g /\ dom h by VALUED_1:12;
hence
A2: dom(g-h) = dom -(h-g) by A1,VALUED_1:12;
let x be object;
assume
A3: x in dom(g-h);
hence (g-h).x = g.x-h.x by VALUED_1:13
.= -(h.x-g.x)
.= -(h-g).x by A1,A2,A3,VALUED_1:13
.= (-(h-g)).x by VALUED_1:8;
end;
theorem Th19:
g (#) h /" k = g (#) (h /" k)
proof
A1: dom(g (#) (h /" k)) = dom g /\ dom(h /" k) & dom(g (#) h /" k) = dom(g
(#) h ) /\ dom k by VALUED_1:16,def 4;
dom(g (#) h) = dom g /\ dom h & dom(h /" k) = dom h /\ dom k by VALUED_1:16
,def 4;
hence dom(g (#) h /" k) = dom(g (#) (h /" k)) by A1,XBOOLE_1:16;
let x be object;
assume x in dom(g (#) h /" k);
thus (g (#) h /" k).x = (g (#) h).x / k.x by VALUED_1:17
.= g.x * h.x / k.x by VALUED_1:5
.= g.x * (h.x / k.x)
.= g.x * (h /" k).x by VALUED_1:17
.= (g (#) (h /" k)).x by VALUED_1:5;
end;
theorem Th20:
g /" h (#) k = g (#) k /" h
proof
A1: dom(g /" h (#) k) = dom(g /" h) /\ dom k & dom(g (#) k /" h) = dom(g (#)
k) /\ dom h by VALUED_1:16,def 4;
dom(g /" h) = dom g /\ dom h & dom(g (#) k) = dom g /\ dom k by VALUED_1:16
,def 4;
hence dom(g /" h (#) k) = dom(g (#) k /" h) by A1,XBOOLE_1:16;
let x be object;
assume x in dom(g /" h (#) k);
thus (g /" h (#) k).x = (g /" h).x * k.x by VALUED_1:5
.= g.x / h.x * k.x by VALUED_1:17
.= g.x * k.x / h.x
.= (g(#)k).x / h.x by VALUED_1:5
.= (g (#) k /" h).x by VALUED_1:17;
end;
theorem Th21:
g /" h /" k = g /" (h (#) k)
proof
A1: dom(g /" h /" k) = dom(g /" h) /\ dom k & dom(g /" (h (#) k)) = dom g /\
dom (h (#) k) by VALUED_1:16;
dom(g /" h) = dom g /\ dom h & dom(h (#) k) = dom h /\ dom k by VALUED_1:16
,def 4;
hence dom(g /" h /" k) = dom(g /" (h (#) k)) by A1,XBOOLE_1:16;
let x be object;
assume x in dom(g /" h /" k);
thus (g /" h /" k).x = (g /" h).x / k.x by VALUED_1:17
.= g.x / h.x / k.x by VALUED_1:17
.= g.x / (h.x * k.x) by XCMPLX_1:78
.= g.x / (h (#) k).x by VALUED_1:5
.= (g /" (h (#) k)).x by VALUED_1:17;
end;
theorem Th22:
c(#)-g = (-c)(#)g
proof
dom(c(#)-g) = dom -g by VALUED_1:def 5
.= dom g by VALUED_1:8;
hence dom(c(#)-g) = dom((-c)(#)g) by VALUED_1:def 5;
let x be object;
assume x in dom(c(#)-g);
thus (c(#)-g).x = c*((-g).x) by VALUED_1:6
.= c*(-g.x) by VALUED_1:8
.= (-c)*g.x
.= ((-c)(#)g).x by VALUED_1:6;
end;
theorem Th23:
c(#)-g = -(c(#)g)
proof
A1: dom(-(c(#)g)) = dom(c(#)g) by VALUED_1:8
.= dom g by VALUED_1:def 5;
dom(c(#)-g) = dom -g by VALUED_1:def 5
.= dom g by VALUED_1:8;
hence dom(c(#)-g) = dom -(c(#)g) by A1;
let x be object;
assume x in dom(c(#)-g);
thus (c(#)-g).x = c*((-g).x) by VALUED_1:6
.= c*(-g.x) by VALUED_1:8
.= -(c*g.x)
.= -(c(#)g).x by VALUED_1:6
.= (-(c(#)g)).x by VALUED_1:8;
end;
theorem Th24:
(-c)(#)g = -(c(#)g)
proof
thus (-c)(#)g = c(#)-g by Th22
.= -(c(#)g) by Th23;
end;
theorem Th25:
- (g (#) h) = (-g) (#) h
proof
A1: dom -(g(#)h) = dom(g(#)h) by VALUED_1:8;
dom(g(#)h) = dom g /\ dom h & dom((-g)(#)h) = dom(-g) /\ dom h by
VALUED_1:def 4;
hence dom -(g(#)h) = dom((-g)(#)h) by A1,VALUED_1:8;
let x be object;
assume x in dom -(g(#)h);
thus (-(g(#)h)).x = -(g(#)h).x by VALUED_1:8
.= -(g.x*h.x) by VALUED_1:5
.= (-g.x)*h.x
.= (-g).x*h.x by VALUED_1:8
.= ((-g)(#)h).x by VALUED_1:5;
end;
theorem
- (g /" h) = (-g) /" h
proof
A1: dom -(g/"h) = dom(g/"h) by VALUED_1:8;
dom(g/"h) = dom g /\ dom h & dom((-g)/"h) = dom(-g) /\ dom h by VALUED_1:16;
hence dom -(g/"h) = dom((-g)/"h) by A1,VALUED_1:8;
let x be object;
assume x in dom -(g/"h);
thus (-(g/"h)).x = -(g/"h).x by VALUED_1:8
.= -(g.x/h.x) by VALUED_1:17
.= (-g.x)/h.x
.= (-g).x/h.x by VALUED_1:8
.= ((-g)/"h).x by VALUED_1:17;
end;
theorem Th27:
- (g /" h) = g /" -h
proof
A1: dom -h = dom h by VALUED_1:8;
dom(g/"h) = dom g /\ dom h & dom(g/"-h) = dom g /\ dom -h by VALUED_1:16;
hence dom -(g/"h) = dom(g/"-h) by A1,VALUED_1:8;
let x be object;
assume x in dom -(g/"h);
thus (-(g/"h)).x = -(g/"h).x by VALUED_1:8
.= -(g.x/h.x) by VALUED_1:17
.= g.x/-h.x by XCMPLX_1:188
.= g.x/(-h).x by VALUED_1:8
.= (g/"-h).x by VALUED_1:17;
end;
definition
let f be complex-valued Function, c be Complex;
func f (/) c -> Function equals
(1/c) (#) f;
coherence;
end;
registration
let f be complex-valued Function, c be Complex;
cluster f (/) c -> complex-valued;
coherence;
end;
registration
let f be real-valued Function, r be Real;
cluster f (/) r -> real-valued;
coherence;
end;
registration
let f be RAT-valued Function, r be Rational;
cluster f (/) r -> RAT-valued;
coherence;
end;
registration
let f be complex-valued FinSequence, c be Complex;
cluster f (/) c -> FinSequence-like;
coherence;
end;
theorem
dom(g(/)c) = dom g by VALUED_1:def 5;
theorem
for x being object holds (g(/)c).x = g.x / c by VALUED_1:6;
theorem Th30:
(-g) (/) c = -(g(/)c)
proof
thus (-g) (/) c = (-(1/c)) (#) g by Th22
.= -(g(/)c) by Th24;
end;
theorem Th31:
g (/) -c = -(g(/)c)
proof
thus g (/) -c = (-1/c) (#) g by XCMPLX_1:188
.= -(g(/)c) by Th24;
end;
theorem
g (/) -c = (-g) (/) c
proof
thus g (/) -c = - (g(/)c) by Th31
.= (-g) (/) c by Th30;
end;
theorem Th33:
g <> {} & g is non-empty & g (/) c1 = g (/) c2 implies c1 = c2
proof
assume that
A1: g <> {} and
A2: g is non-empty and
A3: g(/)c1 = g(/)c2;
consider x being object such that
A4: x in dom g by A1,XBOOLE_0:def 1;
g.x in rng g by A4,FUNCT_1:def 3;
then
A5: g.x <> {} by A2,RELAT_1:def 9;
(g(/)c1).x = g.x/c1 & (g(/)c2).x = g.x/c2 by VALUED_1:6;
then c1" = c2" by A3,A5,XCMPLX_1:5;
hence c1 = c2 by XCMPLX_1:201;
end;
theorem
g (#) c1 (/) c2 = g (#) (c1 / c2)
proof
dom(g(#)c1) = dom g & dom(g(#)c1(/)c2) = dom(g(#)c1) by VALUED_1:def 5;
hence dom(g(#)c1(/)c2) = dom(g(#)(c1/c2)) by VALUED_1:def 5;
let x be object;
assume x in dom(g(#)c1(/)c2);
thus (g(#)c1(/)c2).x = (g(#)c1).x * c2" by VALUED_1:6
.= g.x * c1 * c2" by VALUED_1:6
.= g.x*(c1/c2)
.= (g(#)(c1/c2)).x by VALUED_1:6;
end;
theorem
g (/) c1 (#) c2 = g (#) c2 (/) c1
proof
A1: dom(g(/)c1(#)c2) = dom(g(/)c1) by VALUED_1:def 5;
dom(g(/)c1) = dom g & dom(g(#)c2) = dom g by VALUED_1:def 5;
hence dom(g(/)c1(#)c2) = dom(g(#)c2(/)c1) by A1,VALUED_1:def 5;
let x be object;
assume x in dom(g(/)c1(#)c2);
thus (g(/)c1(#)c2).x = (g(/)c1).x * c2 by VALUED_1:6
.= g.x * c1" * c2 by VALUED_1:6
.= (g.x*c2)*c1"
.= (g(#)c2).x*c1" by VALUED_1:6
.= (g(#)c2(/)c1).x by VALUED_1:6;
end;
theorem
g (/) c1 (/) c2 = g (/) (c1*c2)
proof
dom(g(/)c1) = dom g & dom(g(/)(c1*c2)) = dom g by VALUED_1:def 5;
hence dom(g(/)c1(/)c2) = dom(g(/)(c1*c2)) by VALUED_1:def 5;
let x be object;
assume x in dom(g(/)c1(/)c2);
thus (g(/)c1(/)c2).x = (g(/)c1).x * c2" by VALUED_1:6
.= g.x * c1" * c2" by VALUED_1:6
.= g.x * (c1" * c2")
.= g.x * (c1*c2)" by XCMPLX_1:204
.= (g(/)(c1*c2)).x by VALUED_1:6;
end;
theorem
(g+h) (/) c = g(/)c + h(/)c
proof
A1: dom((g+h)(/)c) = dom(g+h) by VALUED_1:def 5;
A2: dom(g+h) = dom g /\ dom h by VALUED_1:def 1;
dom(g(/)c) = dom g & dom(h(/)c) = dom h by VALUED_1:def 5;
hence
A3: dom((g+h)(/)c) = dom(g(/)c+h(/)c) by A1,A2,VALUED_1:def 1;
let x be object;
assume
A4: x in dom((g+h)(/)c);
thus ((g+h)(/)c).x = (g+h).x * c" by VALUED_1:6
.= (g.x+h.x)*c" by A1,A4,VALUED_1:def 1
.= g.x*c" + h.x*c"
.= (g(/)c).x + h.x*c" by VALUED_1:6
.= (g(/)c).x + (h(/)c).x by VALUED_1:6
.= (g(/)c+h(/)c).x by A3,A4,VALUED_1:def 1;
end;
theorem
(g-h) (/) c = g(/)c - h(/)c
proof
A1: dom((g-h)(/)c) = dom(g-h) by VALUED_1:def 5;
A2: dom(g-h) = dom g /\ dom h by VALUED_1:12;
dom(g(/)c) = dom g & dom(h(/)c) = dom h by VALUED_1:def 5;
hence
A3: dom((g-h)(/)c) = dom(g(/)c-h(/)c) by A1,A2,VALUED_1:12;
let x be object;
assume
A4: x in dom((g-h)(/)c);
thus ((g-h)(/)c).x = (g-h).x * c" by VALUED_1:6
.= (g.x-h.x)*c" by A1,A4,VALUED_1:13
.= g.x*c" - h.x*c"
.= (g(/)c).x - h.x*c" by VALUED_1:6
.= (g(/)c).x - (h(/)c).x by VALUED_1:6
.= (g(/)c-h(/)c).x by A3,A4,VALUED_1:13;
end;
theorem
(g(#)h) (/) c = g (#) (h(/)c)
proof
A1: dom((g(#)h)(/)c) = dom(g(#)h) by VALUED_1:def 5;
dom(g(#)h) = dom g /\ dom h & dom(h(/)c) = dom h by VALUED_1:def 4,def 5;
hence dom((g(#)h)(/)c) = dom(g(#)(h(/)c)) by A1,VALUED_1:def 4;
let x be object;
assume x in dom((g(#)h)(/)c);
thus ((g(#)h)(/)c).x = (g(#)h).x * c" by VALUED_1:6
.= g.x*h.x*c" by VALUED_1:5
.= g.x*(h.x*c")
.= g.x * (h(/)c).x by VALUED_1:6
.= (g(#)(h(/)c)).x by VALUED_1:5;
end;
theorem
(g/"h) (/) c = g /" (h(#)c)
proof
A1: dom((g/"h)(/)c) = dom(g/"h) by VALUED_1:def 5;
dom(g/"h) = dom g /\ dom h & dom(h(#)c) = dom h by VALUED_1:16,def 5;
hence dom((g/"h)(/)c) = dom(g/"(h(#)c)) by A1,VALUED_1:16;
let x be object;
assume x in dom((g/"h)(/)c);
thus ((g/"h)(/)c).x = (g/"h).x * c" by VALUED_1:6
.= g.x/h.x/c by VALUED_1:17
.= g.x/(h.x*c) by XCMPLX_1:78
.= g.x / (h(#)c).x by VALUED_1:6
.= (g/"(h(#)c)).x by VALUED_1:17;
end;
definition
let f be complex-functions-valued Function;
deffunc F(object) = -f.$1;
func <->f -> Function means
:Def33:
dom it = dom f & for x being object st x in dom it holds it.x = -f.x;
existence
proof
ex F being Function st dom F = dom f & for x being object st x in dom f
holds F.x = F(x) from FUNCT_1:sch 3;
hence thesis;
end;
uniqueness
proof
let F,G be Function such that
A1: dom F = dom f and
A2: for x being object st x in dom F holds F.x = F(x) and
A3: dom G = dom f and
A4: for x being object st x in dom G holds G.x = F(x);
thus dom F = dom G by A1,A3;
let x be object;
assume
A5: x in dom F;
hence F.x = F(x) by A2
.= G.x by A1,A3,A4,A5;
end;
end;
definition
let X;
let Y be complex-functions-membered set;
let f be PartFunc of X,Y;
redefine func <->f -> PartFunc of X, C_PFuncs(DOMS(Y)); :: redefines <-> (VALUED_2, definition)
coherence
proof
set h = <->f;
A1: dom h = dom f by Def33;
rng h c= C_PFuncs(DOMS(Y))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
A4: h.x = -f.x by A2,Def33;
then reconsider y as Function by A3;
A5: rng y c= COMPLEX
by A3,A4,XCMPLX_0:def 2;
f.x in Y by A1,A2,PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y;
then
A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74;
dom y = dom(f.x) by A3,A4,VALUED_1:8;
then y is PartFunc of DOMS(Y),COMPLEX by A6,A5,RELSET_1:4;
hence thesis by Def8;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
definition
let X;
let Y be real-functions-membered set;
let f be PartFunc of X,Y;
redefine func <->f -> PartFunc of X, R_PFuncs(DOMS(Y)); :: redefines <-> (VALUED_2, definition)
coherence
proof
set h = <->f;
A1: dom h = dom f by Def33;
rng h c= R_PFuncs(DOMS(Y))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = -f.x by A2,Def33;
A5: rng y c= REAL
by A3,A4,XREAL_0:def 1;
f.x in Y by A1,A2,PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y;
then
A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74;
dom y = dom(f.x) by A3,A4,VALUED_1:8;
then y is PartFunc of DOMS(Y),REAL by A6,A5,RELSET_1:4;
hence thesis by Def12;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
definition
let X;
let Y be rational-functions-membered set;
let f be PartFunc of X,Y;
redefine func <->f -> PartFunc of X, Q_PFuncs(DOMS(Y)); :: redefines <-> (VALUED_2, definition)
coherence
proof
set h = <->f;
A1: dom h = dom f by Def33;
rng h c= Q_PFuncs(DOMS(Y))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = -f.x by A2,Def33;
A5: rng y c= RAT
by A3,A4,RAT_1:def 2;
f.x in Y by A1,A2,PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y;
then
A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74;
dom y = dom(f.x) by A3,A4,VALUED_1:8;
then y is PartFunc of DOMS(Y),RAT by A6,A5,RELSET_1:4;
hence thesis by Def14;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
definition
let X;
let Y be integer-functions-membered set;
let f be PartFunc of X,Y;
redefine func <->f -> PartFunc of X, I_PFuncs(DOMS(Y)); :: redefines <-> (VALUED_2, definition)
coherence
proof
set h = <->f;
A1: dom h = dom f by Def33;
rng h c= I_PFuncs(DOMS(Y))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = -f.x by A2,Def33;
A5: rng y c= INT
by A3,A4,INT_1:def 2;
f.x in Y by A1,A2,PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y;
then
A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74;
dom y = dom(f.x) by A3,A4,VALUED_1:8;
then y is PartFunc of DOMS(Y),INT by A6,A5,RELSET_1:4;
hence thesis by Def16;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
registration
let Y be complex-functions-membered set;
let f be FinSequence of Y;
cluster <->f -> FinSequence-like;
coherence
proof
dom<->f = dom f & ex n being Nat st dom f = Seg n by Def33,FINSEQ_1:def 2;
hence thesis by FINSEQ_1:def 2;
end;
end;
theorem
<-><->f = f
proof
set f1 = <->f;
A1: dom f1 = dom f by Def33;
hence
A2: dom<->f1 = dom f by Def33;
let x be object;
assume
A3: x in dom<->f1;
hence (<->f1).x = -f1.x by Def33
.= -(-f.x) by A1,A2,A3,Def33
.= f.x;
end;
theorem
<->f1 = <->f2 implies f1 = f2
proof
A1: dom <->f1 = dom f1 by Def33;
assume
A2: <->f1 = <->f2;
hence dom f1 = dom f2 by A1,Def33;
let x be object;
assume
A3: x in dom f1;
thus f1.x = --f1.x .= -(<->f1).x by A1,A3,Def33
.= --f2.x by A2,A1,A3,Def33
.= f2.x;
end;
definition
let X be complex-functions-membered set;
let Y be set;
let f be PartFunc of X,Y;
defpred P[object,object] means
ex a being complex-valued Function st $1 = a & $2 =
f.-a;
func f(-) -> Function means
dom it = dom f & for x being complex-valued
Function st x in dom it holds it.x = f.-x;
existence
proof
A1: for x being object st x in dom f ex y being object st P[x,y]
proof
let x be object;
assume x in dom f;
then reconsider a = x as complex-valued Function;
take f.-a, a;
thus thesis;
end;
consider F being Function such that
A2: dom F = dom f and
A3: for x being object st x in dom f holds P[x,F.x] from CLASSES1:sch 1(
A1);
take F;
thus dom F = dom f by A2;
let x be complex-valued Function;
assume x in dom F;
then P[x,F.x] by A2,A3;
hence thesis;
end;
uniqueness
proof
let F, G be Function such that
A4: dom F = dom f and
A5: for x being complex-valued Function st x in dom F holds F.x = f.- x and
A6: dom G = dom f and
A7: for x being complex-valued Function st x in dom G holds G.x = f.- x;
thus dom F = dom G by A4,A6;
let x be object;
assume
A8: x in dom F;
then reconsider y = x as complex-valued Function by A4;
thus F.x = f.-y by A5,A8
.= G.x by A4,A6,A7,A8;
end;
end;
definition
let f be complex-functions-valued Function;
deffunc F(object) = (f.$1)";
func </>f -> Function means
:Def35:
dom it = dom f & for x being object st x in dom it holds it.x = (f.x)";
existence
proof
ex F being Function st dom F = dom f & for x being object st x in dom f
holds F.x = F(x) from FUNCT_1:sch 3;
hence thesis;
end;
uniqueness
proof
let F,G be Function such that
A1: dom F = dom f and
A2: for x being object st x in dom F holds F.x = F(x) and
A3: dom G = dom f and
A4: for x being object st x in dom G holds G.x = F(x);
thus dom F = dom G by A1,A3;
let x be object;
assume
A5: x in dom F;
hence F.x = F(x) by A2
.= G.x by A1,A3,A4,A5;
end;
end;
definition
let X;
let Y be complex-functions-membered set;
let f be PartFunc of X,Y;
redefine func </>f -> PartFunc of X, C_PFuncs(DOMS(Y)); :: redefines </> (VALUED_2, definition)
coherence
proof
set h = </>f;
A1: dom h = dom f by Def35;
rng h c= C_PFuncs(DOMS(Y))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
A4: h.x = (f.x)" by A2,Def35;
then reconsider y as Function by A3;
A5: rng y c= COMPLEX
by A3,A4,XCMPLX_0:def 2;
f.x in Y by A1,A2,PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y;
then
A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74;
dom y = dom(f.x) by A3,A4,VALUED_1:def 7;
then y is PartFunc of DOMS(Y),COMPLEX by A6,A5,RELSET_1:4;
hence thesis by Def8;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
definition
let X;
let Y be real-functions-membered set;
let f be PartFunc of X,Y;
redefine func </>f -> PartFunc of X, R_PFuncs(DOMS(Y)); :: redefines </> (VALUED_2, definition)
coherence
proof
set h = </>f;
A1: dom h = dom f by Def35;
rng h c= R_PFuncs(DOMS(Y))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = (f.x)" by A2,Def35;
A5: rng y c= REAL
by A3,A4,XREAL_0:def 1;
f.x in Y by A1,A2,PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y;
then
A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74;
dom y = dom(f.x) by A3,A4,VALUED_1:def 7;
then y is PartFunc of DOMS(Y),REAL by A6,A5,RELSET_1:4;
hence thesis by Def12;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
definition
let X;
let Y be rational-functions-membered set;
let f be PartFunc of X,Y;
redefine func </>f -> PartFunc of X, Q_PFuncs(DOMS(Y)); :: redefines </> (VALUED_2, definition)
coherence
proof
set h = </>f;
A1: dom h = dom f by Def35;
rng h c= Q_PFuncs(DOMS(Y))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = (f.x)" by A2,Def35;
A5: rng y c= RAT
by A3,A4,RAT_1:def 2;
f.x in Y by A1,A2,PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y;
then
A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74;
dom y = dom(f.x) by A3,A4,VALUED_1:def 7;
then y is PartFunc of DOMS(Y),RAT by A6,A5,RELSET_1:4;
hence thesis by Def14;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
registration
let Y be complex-functions-membered set;
let f be FinSequence of Y;
cluster </>f -> FinSequence-like;
coherence
proof
dom </>f = dom f & ex n being Nat st dom f = Seg n by Def35,FINSEQ_1:def 2;
hence thesis by FINSEQ_1:def 2;
end;
end;
theorem
</></>f = f
proof
set f1 = </>f;
A1: dom f1 = dom f by Def35;
hence
A2: dom </>f1 = dom f by Def35;
let x be object;
assume
A3: x in dom </>f1;
hence (</>f1).x = (f1.x)" by Def35
.= (f.x)"" by A1,A2,A3,Def35
.= f.x;
end;
definition
let f be complex-functions-valued Function;
deffunc F(object) = abs(f.$1);
func abs(f) -> Function means
:Def36:
dom it = dom f & for x being object st x in dom it holds it.x = abs(f.x);
existence
proof
ex F being Function st dom F = dom f & for x being object st x in dom f
holds F.x = F(x) from FUNCT_1:sch 3;
hence thesis;
end;
uniqueness
proof
let F,G be Function such that
A1: dom F = dom f and
A2: for x being object st x in dom F holds F.x = F(x) and
A3: dom G = dom f and
A4: for x being object st x in dom G holds G.x = F(x);
thus dom F = dom G by A1,A3;
let x be object;
assume
A5: x in dom F;
hence F.x = F(x) by A2
.= G.x by A1,A3,A4,A5;
end;
end;
definition
let X;
let Y be complex-functions-membered set;
let f be PartFunc of X,Y;
redefine func abs(f) -> PartFunc of X, C_PFuncs(DOMS(Y)); :: redefines abs (VALUED_2, definition)
coherence
proof
set h = abs(f);
A1: dom h = dom f by Def36;
rng h c= C_PFuncs(DOMS(Y))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
A4: h.x = abs(f.x) by A2,Def36;
then reconsider y as Function by A3;
A5: rng y c= COMPLEX
by A3,A4,XCMPLX_0:def 2;
f.x in Y by A1,A2,PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y;
then
A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74;
dom y = dom(f.x) by A3,A4,VALUED_1:def 11;
then y is PartFunc of DOMS(Y),COMPLEX by A6,A5,RELSET_1:4;
hence thesis by Def8;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
definition
let X;
let Y be real-functions-membered set;
let f be PartFunc of X,Y;
redefine func abs(f) -> PartFunc of X, R_PFuncs(DOMS(Y)); :: redefines abs (VALUED_2, definition)
coherence
proof
set h = abs(f);
A1: dom h = dom f by Def36;
rng h c= R_PFuncs(DOMS(Y))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = abs(f.x) by A2,Def36;
A5: rng y c= REAL
by A3,A4,XREAL_0:def 1;
f.x in Y by A1,A2,PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y;
then
A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74;
dom y = dom(f.x) by A3,A4,VALUED_1:def 11;
then y is PartFunc of DOMS(Y),REAL by A6,A5,RELSET_1:4;
hence thesis by Def12;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
definition
let X;
let Y be rational-functions-membered set;
let f be PartFunc of X,Y;
redefine func abs(f) -> PartFunc of X, Q_PFuncs(DOMS(Y)); :: redefines abs (VALUED_2, definition)
coherence
proof
set h = abs(f);
A1: dom h = dom f by Def36;
rng h c= Q_PFuncs(DOMS(Y))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = abs(f.x) by A2,Def36;
A5: rng y c= RAT
by A3,A4,RAT_1:def 2;
f.x in Y by A1,A2,PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y;
then
A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74;
dom y = dom(f.x) by A3,A4,VALUED_1:def 11;
then y is PartFunc of DOMS(Y),RAT by A6,A5,RELSET_1:4;
hence thesis by Def14;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
definition
let X;
let Y be integer-functions-membered set;
let f be PartFunc of X,Y;
redefine func abs(f) -> PartFunc of X, N_PFuncs(DOMS(Y)); :: redefines abs (VALUED_2, definition)
coherence
proof
set h = abs(f);
A1: dom h = dom f by Def36;
rng h c= N_PFuncs(DOMS(Y))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = abs(f.x) by A2,Def36;
A5: rng y c= NAT
by A3,A4,ORDINAL1:def 12;
f.x in Y by A1,A2,PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y;
then
A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74;
dom y = dom(f.x) by A3,A4,VALUED_1:def 11;
then y is PartFunc of DOMS(Y),NAT by A6,A5,RELSET_1:4;
hence thesis by Def18;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
registration
let Y be complex-functions-membered set;
let f be FinSequence of Y;
cluster abs(f) -> FinSequence-like;
coherence
proof
dom abs(f) = dom f & ex n being Nat st dom f = Seg n by Def36,
FINSEQ_1:def 2;
hence thesis by FINSEQ_1:def 2;
end;
end;
theorem
abs abs f = abs f
proof
set f1 = abs f;
thus
A1: dom abs f1 = dom abs f by Def36;
let x be object;
assume
A2: x in dom abs f1;
hence (abs f1).x = abs(f1.x) by Def36
.= abs(abs(f.x)) by A1,A2,Def36
.= (abs f).x by A1,A2,Def36;
end;
definition
let Y be complex-functions-membered set;
let f be Y-valued Function;
let c be Complex;
deffunc F(object) = c+(f.$1);
func f[+]c -> Function means
:Def37:
dom it = dom f & for x being object st x in dom it holds it.x = c + f.x;
existence
proof
ex F being Function st dom F = dom f & for x being object st x in dom f
holds F.x = F(x) from FUNCT_1:sch 3;
hence thesis;
end;
uniqueness
proof
let F,G be Function such that
A1: dom F = dom f and
A2: for x being object st x in dom F holds F.x = F(x) and
A3: dom G = dom f and
A4: for x being object st x in dom G holds G.x = F(x);
thus dom F = dom G by A1,A3;
let x be object;
assume
A5: x in dom F;
hence F.x = F(x) by A2
.= G.x by A1,A3,A4,A5;
end;
end;
definition
let X;
let Y be complex-functions-membered set;
let f be PartFunc of X,Y;
let c be Complex;
redefine func f[+]c -> PartFunc of X, C_PFuncs(DOMS(Y)); :: redefines [+] (VALUED_2, definition)
coherence
proof
set h = f[+]c;
A1: dom h = dom f by Def37;
rng h c= C_PFuncs(DOMS(Y))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
A4: h.x = f.x + c by A2,Def37;
then reconsider y as Function by A3;
A5: rng y c= COMPLEX
by A3,A4,XCMPLX_0:def 2;
f.x in Y by A1,A2,PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y;
then
A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74;
dom y = dom(f.x) by A3,A4,VALUED_1:def 2;
then y is PartFunc of DOMS(Y),COMPLEX by A6,A5,RELSET_1:4;
hence thesis by Def8;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
definition
let X;
let Y be real-functions-membered set;
let f be PartFunc of X,Y;
let c be Real;
redefine func f[+]c -> PartFunc of X, R_PFuncs(DOMS(Y)); :: redefines [+] (VALUED_2, definition)
coherence
proof
set h = f[+]c;
A1: dom h = dom f by Def37;
rng h c= R_PFuncs(DOMS(Y))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = f.x + c by A2,Def37;
A5: rng y c= REAL
by A3,A4,XREAL_0:def 1;
f.x in Y by A1,A2,PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y;
then
A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74;
dom y = dom(f.x) by A3,A4,VALUED_1:def 2;
then y is PartFunc of DOMS(Y),REAL by A6,A5,RELSET_1:4;
hence thesis by Def12;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
definition
let X;
let Y be rational-functions-membered set;
let f be PartFunc of X,Y;
let c be Rational;
redefine func f[+]c -> PartFunc of X, Q_PFuncs(DOMS(Y)); :: redefines [+] (VALUED_2, definition)
coherence
proof
set h = f[+]c;
A1: dom h = dom f by Def37;
rng h c= Q_PFuncs(DOMS(Y))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = f.x + c by A2,Def37;
A5: rng y c= RAT
by A3,A4,RAT_1:def 2;
f.x in Y by A1,A2,PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y;
then
A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74;
dom y = dom(f.x) by A3,A4,VALUED_1:def 2;
then y is PartFunc of DOMS(Y),RAT by A6,A5,RELSET_1:4;
hence thesis by Def14;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
definition
let X;
let Y be integer-functions-membered set;
let f be PartFunc of X,Y;
let c be Integer;
redefine func f[+]c -> PartFunc of X, I_PFuncs(DOMS(Y)); :: redefines [+] (VALUED_2, definition)
coherence
proof
set h = f[+]c;
A1: dom h = dom f by Def37;
rng h c= I_PFuncs(DOMS(Y))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = f.x + c by A2,Def37;
A5: rng y c= INT
by A3,A4,INT_1:def 2;
f.x in Y by A1,A2,PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y;
then
A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74;
dom y = dom(f.x) by A3,A4,VALUED_1:def 2;
then y is PartFunc of DOMS(Y),INT by A6,A5,RELSET_1:4;
hence thesis by Def16;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
definition
let X;
let Y be natural-functions-membered set;
let f be PartFunc of X,Y;
let c be Nat;
redefine func f[+]c -> PartFunc of X, N_PFuncs(DOMS(Y)); :: redefines [+] (VALUED_2, definition)
coherence
proof
set h = f[+]c;
A1: dom h = dom f by Def37;
rng h c= N_PFuncs(DOMS(Y))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = f.x + c by A2,Def37;
A5: rng y c= NAT
by A3,A4,ORDINAL1:def 12;
f.x in Y by A1,A2,PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y;
then
A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74;
dom y = dom(f.x) by A3,A4,VALUED_1:def 2;
then y is PartFunc of DOMS(Y),NAT by A6,A5,RELSET_1:4;
hence thesis by Def18;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
theorem
f [+] c1 [+] c2 = f [+] (c1+c2)
proof
set f1 = f[+]c1;
A1: dom(f1[+]c2) = dom f1 by Def37;
dom f1 = dom f by Def37;
hence
A2: dom(f1[+]c2) = dom(f[+](c1+c2)) by A1,Def37;
let x be object;
assume
A3: x in dom(f1[+]c2);
hence (f1[+]c2).x = f1.x + c2 by Def37
.= f.x + c1 + c2 by A1,A3,Def37
.= f.x + (c1 + c2) by Th12
.= (f[+](c1+c2)).x by A2,A3,Def37;
end;
theorem
f <> {} & f is non-empty & f [+] c1 = f [+] c2 implies c1 = c2
proof
assume that
A1: f <> {} and
A2: f is non-empty and
A3: f[+]c1 = f[+]c2;
consider x being object such that
A4: x in dom f by A1,XBOOLE_0:def 1;
f.x in rng f by A4,FUNCT_1:def 3;
then
A5: f.x <> {} by A2,RELAT_1:def 9;
dom f = dom(f[+]c2) by Def37;
then
A6: (f[+]c2).x = f.x+c2 by A4,Def37;
dom f = dom(f[+]c1) by Def37;
then (f[+]c1).x = f.x+c1 by A4,Def37;
hence c1 = c2 by A3,A5,A6,Th7;
end;
definition
let Y be complex-functions-membered set;
let f be Y-valued Function;
let c be Complex;
func f[-]c -> Function equals
f [+] -c;
coherence;
end;
theorem
dom(f[-]c) = dom f by Def37;
theorem
x in dom(f[-]c) implies (f[-]c).x = f.x - c by Def37;
definition
let X;
let Y be complex-functions-membered set;
let f be PartFunc of X,Y;
let c be Complex;
redefine func f[-]c -> PartFunc of X, C_PFuncs(DOMS(Y)); :: redefines [-] (VALUED_2, definition)
coherence
proof
f[-]c = f [+] -c;
hence thesis;
end;
end;
definition
let X;
let Y be real-functions-membered set;
let f be PartFunc of X,Y;
let c be Real;
redefine func f[-]c -> PartFunc of X, R_PFuncs(DOMS(Y)); :: redefines [-] (VALUED_2, definition)
coherence
proof
f[-]c = f [+] -c;
hence thesis;
end;
end;
definition
let X;
let Y be rational-functions-membered set;
let f be PartFunc of X,Y;
let c be Rational;
redefine func f[-]c -> PartFunc of X, Q_PFuncs(DOMS(Y)); :: redefines [-] (VALUED_2, definition)
coherence
proof
f[-]c = f [+] -c;
hence thesis;
end;
end;
definition
let X;
let Y be integer-functions-membered set;
let f be PartFunc of X,Y;
let c be Integer;
redefine func f[-]c -> PartFunc of X, I_PFuncs(DOMS(Y)); :: redefines [-] (VALUED_2, definition)
coherence
proof
f[-]c = f [+] -c;
hence thesis;
end;
end;
theorem
f <> {} & f is non-empty & f [-] c1 = f [-] c2 implies c1 = c2
proof
assume that
A1: f <> {} and
A2: f is non-empty and
A3: f[-]c1 = f[-]c2;
consider x being object such that
A4: x in dom f by A1,XBOOLE_0:def 1;
f.x in rng f by A4,FUNCT_1:def 3;
then
A5: f.x <> {} by A2,RELAT_1:def 9;
dom f = dom(f[-]c2) by Def37;
then
A6: (f[-]c2).x = f.x-c2 by A4,Def37;
dom f = dom(f[-]c1) by Def37;
then (f[-]c1).x = f.x-c1 by A4,Def37;
hence c1 = c2 by A3,A5,A6,Th8;
end;
theorem
f [+] c1 [-] c2 = f [+] (c1-c2)
proof
set f1 = f[+]c1;
A1: dom(f1[-]c2) = dom f1 by Def37;
dom f1 = dom f by Def37;
hence
A2: dom(f1[-]c2) = dom(f[+](c1-c2)) by A1,Def37;
let x be object;
assume
A3: x in dom(f1[-]c2);
hence (f1[-]c2).x = f1.x - c2 by Def37
.= f.x + c1 - c2 by A1,A3,Def37
.= f.x + (c1 - c2) by Th12
.= (f[+](c1-c2)).x by A2,A3,Def37;
end;
theorem
f [-] c1 [+] c2 = f [-] (c1-c2)
proof
set f1 = f[-]c1;
A1: dom(f1[+]c2) = dom f1 by Def37;
dom f1 = dom f by Def37;
hence
A2: dom(f1[+]c2) = dom(f[-](c1-c2)) by A1,Def37;
let x be object;
assume
A3: x in dom(f1[+]c2);
hence (f1[+]c2).x = f1.x + c2 by Def37
.= f.x - c1 + c2 by A1,A3,Def37
.= f.x - (c1 - c2) by Th14
.= (f[-](c1-c2)).x by A2,A3,Def37;
end;
theorem
f [-] c1 [-] c2 = f [-] (c1+c2)
proof
set f1 = f[-]c1;
A1: dom(f1[-]c2) = dom f1 by Def37;
dom f1 = dom f by Def37;
hence
A2: dom(f1[-]c2) = dom(f[-](c1+c2)) by A1,Def37;
let x be object;
assume
A3: x in dom(f1[-]c2);
hence (f1[-]c2).x = f1.x - c2 by Def37
.= f.x - c1 - c2 by A1,A3,Def37
.= f.x - (c1 + c2) by Th15
.= (f[-](c1+c2)).x by A2,A3,Def37;
end;
definition
let Y be complex-functions-membered set;
let f be Y-valued Function;
let c be Complex;
deffunc F(object) = c(#)(f.$1);
func f[#]c -> Function means
:Def39:
dom it = dom f & for x being object st x in dom it holds it.x = c (#) (f.x);
existence
proof
ex F being Function st dom F = dom f & for x being object st x in dom f
holds F.x = F(x) from FUNCT_1:sch 3;
hence thesis;
end;
uniqueness
proof
let F,G be Function such that
A1: dom F = dom f and
A2: for x being object st x in dom F holds F.x = F(x) and
A3: dom G = dom f and
A4: for x being object st x in dom G holds G.x = F(x);
thus dom F = dom G by A1,A3;
let x be object;
assume
A5: x in dom F;
hence F.x = F(x) by A2
.= G.x by A1,A3,A4,A5;
end;
end;
definition
let X;
let Y be complex-functions-membered set;
let f be PartFunc of X,Y;
let c be Complex;
redefine func f[#]c -> PartFunc of X, C_PFuncs(DOMS(Y)); :: redefines [#] (VALUED_2, definition)
coherence
proof
set h = f[#]c;
A1: dom h = dom f by Def39;
rng h c= C_PFuncs(DOMS(Y))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
A4: h.x = c (#) f.x by A2,Def39;
then reconsider y as Function by A3;
A5: rng y c= COMPLEX
by A3,A4,XCMPLX_0:def 2;
f.x in Y by A1,A2,PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y;
then
A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74;
dom y = dom(f.x) by A3,A4,VALUED_1:def 5;
then y is PartFunc of DOMS(Y),COMPLEX by A6,A5,RELSET_1:4;
hence thesis by Def8;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
definition
let X;
let Y be real-functions-membered set;
let f be PartFunc of X,Y;
let c be Real;
redefine func f[#]c -> PartFunc of X, R_PFuncs(DOMS(Y)); :: redefines [#] (VALUED_2, definition)
coherence
proof
set h = f[#]c;
A1: dom h = dom f by Def39;
rng h c= R_PFuncs(DOMS(Y))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = c (#) f.x by A2,Def39;
A5: rng y c= REAL
by A3,A4,XREAL_0:def 1;
f.x in Y by A1,A2,PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y;
then
A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74;
dom y = dom(f.x) by A3,A4,VALUED_1:def 5;
then y is PartFunc of DOMS(Y),REAL by A6,A5,RELSET_1:4;
hence thesis by Def12;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
definition
let X;
let Y be rational-functions-membered set;
let f be PartFunc of X,Y;
let c be Rational;
redefine func f[#]c -> PartFunc of X, Q_PFuncs(DOMS(Y)); :: redefines [#] (VALUED_2, definition)
coherence
proof
set h = f[#]c;
A1: dom h = dom f by Def39;
rng h c= Q_PFuncs(DOMS(Y))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = c (#) f.x by A2,Def39;
A5: rng y c= RAT
by A3,A4,RAT_1:def 2;
f.x in Y by A1,A2,PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y;
then
A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74;
dom y = dom(f.x) by A3,A4,VALUED_1:def 5;
then y is PartFunc of DOMS(Y),RAT by A6,A5,RELSET_1:4;
hence thesis by Def14;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
definition
let X;
let Y be integer-functions-membered set;
let f be PartFunc of X,Y;
let c be Integer;
redefine func f[#]c -> PartFunc of X, I_PFuncs(DOMS(Y)); :: redefines [#] (VALUED_2, definition)
coherence
proof
set h = f[#]c;
A1: dom h = dom f by Def39;
rng h c= I_PFuncs(DOMS(Y))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = c (#) f.x by A2,Def39;
A5: rng y c= INT
by A3,A4,INT_1:def 2;
f.x in Y by A1,A2,PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y;
then
A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74;
dom y = dom(f.x) by A3,A4,VALUED_1:def 5;
then y is PartFunc of DOMS(Y),INT by A6,A5,RELSET_1:4;
hence thesis by Def16;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
definition
let X;
let Y be natural-functions-membered set;
let f be PartFunc of X,Y;
let c be Nat;
redefine func f[#]c -> PartFunc of X, N_PFuncs(DOMS(Y)); :: redefines [#] (VALUED_2, definition)
coherence
proof
set h = f[#]c;
A1: dom h = dom f by Def39;
rng h c= N_PFuncs(DOMS(Y))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = c (#) f.x by A2,Def39;
A5: rng y c= NAT
by A3,A4,ORDINAL1:def 12;
f.x in Y by A1,A2,PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y;
then
A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74;
dom y = dom(f.x) by A3,A4,VALUED_1:def 5;
then y is PartFunc of DOMS(Y),NAT by A6,A5,RELSET_1:4;
hence thesis by Def18;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
theorem
f [#] c1 [#] c2 = f [#] (c1*c2)
proof
set f1 = f[#]c1;
A1: dom(f1[#]c2) = dom f1 by Def39;
dom f1 = dom f by Def39;
hence
A2: dom(f1[#]c2) = dom(f[#](c1*c2)) by A1,Def39;
let x be object;
assume
A3: x in dom(f1[#]c2);
hence (f1[#]c2).x = f1.x (#) c2 by Def39
.= f.x (#) c1 (#) c2 by A1,A3,Def39
.= f.x (#) (c1 * c2) by Th16
.= (f[#](c1*c2)).x by A2,A3,Def39;
end;
theorem
f <> {} & f is non-empty & (for x st x in dom f holds f.x is non-empty
) & f [#] c1 = f [#] c2 implies c1 = c2
proof
assume that
A1: f <> {} and
A2: f is non-empty and
A3: for x st x in dom f holds f.x is non-empty and
A4: f[#]c1 = f[#]c2;
consider x being object such that
A5: x in dom f by A1,XBOOLE_0:def 1;
dom f = dom(f[#]c2) by Def39;
then
A6: (f[#]c2).x = f.x(#)c2 by A5,Def39;
dom f = dom(f[#]c1) by Def39;
then
A7: (f[#]c1).x = f.x(#)c1 by A5,Def39;
f.x in rng f by A5,FUNCT_1:def 3;
then
A8: f.x <> {} by A2,RELAT_1:def 9;
f.x is non-empty by A3,A5;
hence c1 = c2 by A4,A8,A7,A6,Th9;
end;
definition
let Y be complex-functions-membered set;
let f be Y-valued Function;
let c be Complex;
func f[/]c -> Function equals
f [#] (c");
coherence;
end;
theorem
dom(f[/]c) = dom f by Def39;
theorem
x in dom(f[/]c) implies (f[/]c).x = c" (#) f.x by Def39;
definition
let X;
let Y be complex-functions-membered set;
let f be PartFunc of X,Y;
let c be Complex;
redefine func f[/]c -> PartFunc of X, C_PFuncs(DOMS(Y)); :: redefines [/] (VALUED_2, definition)
coherence
proof
f[/]c = f [#] (c");
hence thesis;
end;
end;
definition
let X;
let Y be real-functions-membered set;
let f be PartFunc of X,Y;
let c be Real;
redefine func f[/]c -> PartFunc of X, R_PFuncs(DOMS(Y)); :: redefines [/] (VALUED_2, definition)
coherence
proof
f[/]c = f [#] (c");
hence thesis;
end;
end;
definition
let X;
let Y be rational-functions-membered set;
let f be PartFunc of X,Y;
let c be Rational;
redefine func f[/]c -> PartFunc of X, Q_PFuncs(DOMS(Y)); :: redefines [/] (VALUED_2, definition)
coherence
proof
f[/]c = f [#] (c");
hence thesis;
end;
end;
theorem
f [/] c1 [/] c2 = f [/] (c1*c2)
proof
set f1 = f[/]c1;
A1: dom(f1[/]c2) = dom f1 by Def39;
dom f1 = dom f by Def39;
hence
A2: dom(f1[/]c2) = dom(f[/](c1*c2)) by A1,Def39;
let x be object;
assume
A3: x in dom(f1[/]c2);
hence (f1[/]c2).x = f1.x (#) c2" by Def39
.= f.x (#) c1" (#) c2" by A1,A3,Def39
.= f.x (#) (c1" * c2") by Th16
.= f.x (#) (c1*c2)" by XCMPLX_1:204
.= (f[/](c1*c2)).x by A2,A3,Def39;
end;
theorem
f <> {} & f is non-empty & (for x st x in dom f holds f.x is non-empty
) & f [/] c1 = f [/] c2 implies c1 = c2
proof
assume that
A1: f <> {} and
A2: f is non-empty and
A3: for x st x in dom f holds f.x is non-empty and
A4: f[/]c1 = f[/]c2;
consider x being object such that
A5: x in dom f by A1,XBOOLE_0:def 1;
dom f = dom(f[/]c2) by Def39;
then
A6: (f[/]c2).x = f.x(/)c2 by A5,Def39;
dom f = dom(f[/]c1) by Def39;
then
A7: (f[/]c1).x = f.x(/)c1 by A5,Def39;
f.x in rng f by A5,FUNCT_1:def 3;
then
A8: f.x <> {} by A2,RELAT_1:def 9;
f.x is non-empty by A3,A5;
hence c1 = c2 by A4,A8,A7,A6,Th33;
end;
definition
let Y be complex-functions-membered set;
let f be Y-valued Function;
let g be complex-valued Function;
deffunc F(object) = f.$1+g.$1;
func f<+>g -> Function means
:Def41:
dom it = dom f /\ dom g &
for x being object st x in dom it holds it.x = f.x + g.x;
existence
proof
ex F being Function st dom F = dom f /\ dom g & for x being object st x
in dom f /\ dom g holds F.x = F(x) from FUNCT_1:sch 3;
hence thesis;
end;
uniqueness
proof
let F,G be Function such that
A1: dom F = dom f /\ dom g and
A2: for x being object st x in dom F holds F.x = F(x) and
A3: dom G = dom f /\ dom g and
A4: for x being object st x in dom G holds G.x = F(x);
thus dom F = dom G by A1,A3;
let x be object;
assume
A5: x in dom F;
hence F.x = F(x) by A2
.= G.x by A1,A3,A4,A5;
end;
end;
definition
let X;
let Y be complex-functions-membered set;
let f be PartFunc of X,Y;
let g be complex-valued Function;
redefine func f<+>g -> PartFunc of X /\ dom g, C_PFuncs(DOMS(Y)); :: redefines <+> (VALUED_2, definition)
coherence
proof
set h = f<+>g;
A1: dom h = dom f /\ dom g by Def41;
rng h c= C_PFuncs(DOMS(Y))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
A4: h.x = f.x + g.x by A2,Def41;
then reconsider y as Function by A3;
A5: rng y c= COMPLEX
by A3,A4,XCMPLX_0:def 2;
x in dom f by A1,A2,XBOOLE_0:def 4;
then f.x in Y by PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y;
then
A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74;
dom y = dom(f.x) by A3,A4,VALUED_1:def 2;
then y is PartFunc of DOMS(Y),COMPLEX by A6,A5,RELSET_1:4;
hence thesis by Def8;
end;
hence thesis by A1,RELSET_1:4,XBOOLE_1:27;
end;
end;
definition
let X;
let Y be real-functions-membered set;
let f be PartFunc of X,Y;
let g be real-valued Function;
redefine func f<+>g -> PartFunc of X /\ dom g, R_PFuncs(DOMS(Y)); :: redefines <+> (VALUED_2, definition)
coherence
proof
set h = f<+>g;
A1: dom h = dom f /\ dom g by Def41;
rng h c= R_PFuncs(DOMS(Y))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = f.x + g.x by A2,Def41;
A5: rng y c= REAL
by A3,A4,XREAL_0:def 1;
x in dom f by A1,A2,XBOOLE_0:def 4;
then f.x in Y by PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y;
then
A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74;
dom y = dom(f.x) by A3,A4,VALUED_1:def 2;
then y is PartFunc of DOMS(Y),REAL by A6,A5,RELSET_1:4;
hence thesis by Def12;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
definition
let X;
let Y be rational-functions-membered set;
let f be PartFunc of X,Y;
let g be RAT-valued Function;
redefine func f<+>g -> PartFunc of X /\ dom g, Q_PFuncs(DOMS(Y)); :: redefines <+> (VALUED_2, definition)
coherence
proof
set h = f<+>g;
A1: dom h = dom f /\ dom g by Def41;
rng h c= Q_PFuncs(DOMS(Y))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = f.x + g.x by A2,Def41;
A5: rng y c= RAT
by A3,A4,RAT_1:def 2;
x in dom f by A1,A2,XBOOLE_0:def 4;
then f.x in Y by PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y;
then
A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74;
dom y = dom(f.x) by A3,A4,VALUED_1:def 2;
then y is PartFunc of DOMS(Y),RAT by A6,A5,RELSET_1:4;
hence thesis by Def14;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
definition
let X;
let Y be integer-functions-membered set;
let f be PartFunc of X,Y;
let g be INT-valued Function;
redefine func f<+>g -> PartFunc of X /\ dom g, I_PFuncs(DOMS(Y)); :: redefines <+> (VALUED_2, definition)
coherence
proof
set h = f<+>g;
A1: dom h = dom f /\ dom g by Def41;
rng h c= I_PFuncs(DOMS(Y))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = f.x + g.x by A2,Def41;
A5: rng y c= INT
by A3,A4,INT_1:def 2;
x in dom f by A1,A2,XBOOLE_0:def 4;
then f.x in Y by PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y;
then
A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74;
dom y = dom(f.x) by A3,A4,VALUED_1:def 2;
then y is PartFunc of DOMS(Y),INT by A6,A5,RELSET_1:4;
hence thesis by Def16;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
definition
let X;
let Y be natural-functions-membered set;
let f be PartFunc of X,Y;
let g be natural-valued Function;
redefine func f<+>g -> PartFunc of X /\ dom g, N_PFuncs(DOMS(Y)); :: redefines <+> (VALUED_2, definition)
coherence
proof
set h = f<+>g;
A1: dom h = dom f /\ dom g by Def41;
rng h c= N_PFuncs(DOMS(Y))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = f.x + g.x by A2,Def41;
A5: rng y c= NAT
by A3,A4,ORDINAL1:def 12;
x in dom f by A1,A2,XBOOLE_0:def 4;
then f.x in Y by PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y;
then
A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74;
dom y = dom(f.x) by A3,A4,VALUED_1:def 2;
then y is PartFunc of DOMS(Y),NAT by A6,A5,RELSET_1:4;
hence thesis by Def18;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
theorem
f <+> g <+> h = f <+> (g+h)
proof
set f1 = f<+>g;
A1: dom(g+h) = dom g /\ dom h by VALUED_1:def 1;
A2: dom(f1<+>h) = dom f1 /\ dom h by Def41;
dom f1 = dom f /\ dom g & dom(f<+>(g+h)) = dom f /\ dom(g+h) by Def41;
hence
A3: dom(f1<+>h) = dom(f<+>(g+h)) by A2,A1,XBOOLE_1:16;
let x be object;
assume
A4: x in dom(f1<+>h);
then
A5: x in dom f1 by A2,XBOOLE_0:def 4;
A6: x in dom(g+h) by A3,A4,XBOOLE_0:def 4;
thus (f1<+>h).x = f1.x + h.x by A4,Def41
.= f.x + g.x + h.x by A5,Def41
.= f.x + (g.x + h.x) by Th12
.= f.x + ((g+h).x) by A6,VALUED_1:def 1
.= (f<+>(g+h)).x by A3,A4,Def41;
end;
theorem
<->(f<+>g) = (<->f) <+> -g
proof
set f1 = f<+>g, f2 = <->f;
A1: dom <->f1 = dom f1 by Def33;
A2: dom f1 = dom f /\ dom g & dom f2 = dom f by Def33,Def41;
dom -g = dom g by VALUED_1:8;
hence
A3: dom <->f1 = dom(f2<+>-g) by A1,A2,Def41;
let x be object;
assume
A4: x in dom <->f1;
then
A5: x in dom f2 by A1,A2,XBOOLE_0:def 4;
thus (<->f1).x = -f1.x by A4,Def33
.= -(f.x+g.x) by A1,A4,Def41
.= -f.x-g.x by Th10
.= -f.x+(-g).x by VALUED_1:8
.= f2.x+(-g).x by A5,Def33
.= (f2<+>-g).x by A3,A4,Def41;
end;
definition
let Y be complex-functions-membered set;
let f be Y-valued Function;
let g be complex-valued Function;
func f<->g -> Function equals
f <+> -g;
coherence;
end;
theorem Th61:
dom(f<->g) = dom f /\ dom g
proof
thus dom(f<->g) = dom f /\ dom -g by Def41
.= dom f /\ dom g by VALUED_1:8;
end;
theorem Th62:
x in dom(f<->g) implies (f<->g).x = f.x - g.x
proof
assume x in dom(f<->g);
hence (f<->g).x = f.x + (-g).x by Def41
.= f.x - g.x by VALUED_1:8;
end;
definition
let X;
let Y be complex-functions-membered set;
let f be PartFunc of X,Y;
let g be complex-valued Function;
redefine func f<->g -> PartFunc of X /\ dom g, C_PFuncs(DOMS(Y)); :: redefines <-> (VALUED_2, definition)
coherence
proof
set h = f<->g;
A1: dom h = dom f /\ dom g by Th61;
rng h c= C_PFuncs(DOMS(Y))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
A4: h.x = f.x - g.x by A2,Th62;
then reconsider y as Function by A3;
A5: rng y c= COMPLEX
by A3,A4,XCMPLX_0:def 2;
x in dom f by A1,A2,XBOOLE_0:def 4;
then f.x in Y by PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y;
then
A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74;
h.x = f.x - g.x by A2,Th62;
then dom y = dom(f.x) by A3,VALUED_1:def 2;
then y is PartFunc of DOMS(Y),COMPLEX by A6,A5,RELSET_1:4;
hence thesis by Def8;
end;
hence thesis by A1,RELSET_1:4,XBOOLE_1:27;
end;
end;
definition
let X;
let Y be real-functions-membered set;
let f be PartFunc of X,Y;
let g be real-valued Function;
redefine func f<->g -> PartFunc of X /\ dom g, R_PFuncs(DOMS(Y)); :: redefines <-> (VALUED_2, definition)
coherence
proof
set h = f<->g;
A1: dom h = dom f /\ dom g by Th61;
rng h c= R_PFuncs(DOMS(Y))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = f.x - g.x by A2,Th62;
A5: rng y c= REAL
by A3,A4,XREAL_0:def 1;
x in dom f by A1,A2,XBOOLE_0:def 4;
then f.x in Y by PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y;
then
A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74;
dom y = dom(f.x) by A3,A4,VALUED_1:def 2;
then y is PartFunc of DOMS(Y),REAL by A6,A5,RELSET_1:4;
hence thesis by Def12;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
definition
let X;
let Y be rational-functions-membered set;
let f be PartFunc of X,Y;
let g be RAT-valued Function;
redefine func f<->g -> PartFunc of X /\ dom g, Q_PFuncs(DOMS(Y)); :: redefines <-> (VALUED_2, definition)
coherence
proof
set h = f<->g;
A1: dom h = dom f /\ dom g by Th61;
rng h c= Q_PFuncs(DOMS(Y))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = f.x - g.x by A2,Th62;
A5: rng y c= RAT
by A3,A4,RAT_1:def 2;
x in dom f by A1,A2,XBOOLE_0:def 4;
then f.x in Y by PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y;
then
A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74;
dom y = dom(f.x) by A3,A4,VALUED_1:def 2;
then y is PartFunc of DOMS(Y),RAT by A6,A5,RELSET_1:4;
hence thesis by Def14;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
definition
let X;
let Y be integer-functions-membered set;
let f be PartFunc of X,Y;
let g be INT-valued Function;
redefine func f<->g -> PartFunc of X /\ dom g, I_PFuncs(DOMS(Y)); :: redefines <-> (VALUED_2, definition)
coherence
proof
set h = f<->g;
A1: dom h = dom f /\ dom g by Th61;
rng h c= I_PFuncs(DOMS(Y))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = f.x - g.x by A2,Th62;
A5: rng y c= INT
by A3,A4,INT_1:def 2;
x in dom f by A1,A2,XBOOLE_0:def 4;
then f.x in Y by PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y;
then
A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74;
dom y = dom(f.x) by A3,A4,VALUED_1:def 2;
then y is PartFunc of DOMS(Y),INT by A6,A5,RELSET_1:4;
hence thesis by Def16;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
theorem
f <-> -g = f <+> g;
theorem
<->(f<->g) = (<->f) <+> g
proof
set f1 = f<->g, f2 = <->f;
A1: dom <->f1 = dom f1 by Def33;
A2: dom f1 = dom f /\ dom g & dom f2 = dom f by Def33,Th61;
hence
A3: dom <->f1 = dom(f2<+>g) by A1,Def41;
let x be object;
assume
A4: x in dom <->f1;
then
A5: x in dom f2 by A1,A2,XBOOLE_0:def 4;
thus (<->f1).x = -f1.x by A4,Def33
.= -(f.x-g.x) by A1,A4,Th62
.= -f.x+g.x by Th11
.= f2.x+g.x by A5,Def33
.= (f2<+>g).x by A3,A4,Def41;
end;
theorem
f <+> g <-> h = f <+> (g-h)
proof
set f1 = f<+>g;
A1: dom(g-h) = dom g /\ dom h by VALUED_1:12;
A2: dom(f1<->h) = dom f1 /\ dom h by Th61;
dom f1 = dom f /\ dom g & dom(f<+>(g-h)) = dom f /\ dom(g-h) by Def41;
hence
A3: dom(f1<->h) = dom(f<+>(g-h)) by A2,A1,XBOOLE_1:16;
let x be object;
assume
A4: x in dom(f1<->h);
then
A5: x in dom f1 by A2,XBOOLE_0:def 4;
A6: x in dom(g-h) by A3,A4,XBOOLE_0:def 4;
thus (f1<->h).x = f1.x - h.x by A4,Th62
.= f.x + g.x - h.x by A5,Def41
.= f.x + (g.x - h.x) by Th13
.= f.x + ((g-h).x) by A6,VALUED_1:13
.= (f<+>(g-h)).x by A3,A4,Def41;
end;
theorem
f <-> g <+> h = f <-> (g-h)
proof
set f1 = f<->g;
A1: dom(g-h) = dom g /\ dom h by VALUED_1:12;
A2: dom(f1<+>h) = dom f1 /\ dom h by Def41;
dom f1 = dom f /\ dom g & dom(f<->(g-h)) = dom f /\ dom(g-h) by Th61;
hence
A3: dom(f1<+>h) = dom(f<->(g-h)) by A2,A1,XBOOLE_1:16;
let x be object;
assume
A4: x in dom(f1<+>h);
then
A5: x in dom f1 by A2,XBOOLE_0:def 4;
A6: x in dom(g-h) by A3,A4,XBOOLE_0:def 4;
thus (f1<+>h).x = f1.x + h.x by A4,Def41
.= f.x - g.x + h.x by A5,Th62
.= f.x - (g.x - h.x) by Th14
.= f.x - ((g-h).x) by A6,VALUED_1:13
.= (f<->(g-h)).x by A3,A4,Th62;
end;
theorem
f <-> g <-> h = f <-> (g+h)
proof
set f1 = f<->g;
A1: dom(g+h) = dom g /\ dom h by VALUED_1:def 1;
A2: dom(f1<->h) = dom f1 /\ dom h by Th61;
dom f1 = dom f /\ dom g & dom(f<->(g+h)) = dom f /\ dom(g+h) by Th61;
hence
A3: dom(f1<->h) = dom(f<->(g+h)) by A2,A1,XBOOLE_1:16;
let x be object;
assume
A4: x in dom(f1<->h);
then
A5: x in dom f1 by A2,XBOOLE_0:def 4;
A6: x in dom(g+h) by A3,A4,XBOOLE_0:def 4;
thus (f1<->h).x = f1.x - h.x by A4,Th62
.= f.x - g.x - h.x by A5,Th62
.= f.x - (g.x + h.x) by Th15
.= f.x - ((g+h).x) by A6,VALUED_1:def 1
.= (f<->(g+h)).x by A3,A4,Th62;
end;
definition
let Y be complex-functions-membered set;
let f be Y-valued Function;
let g be complex-valued Function;
deffunc F(object) = f.$1(#)g.$1;
func f<#>g -> Function means
:Def43:
dom it = dom f /\ dom g & for x being
object st x in dom it holds it.x = f.x (#) g.x;
existence
proof
ex F being Function st dom F = dom f /\ dom g & for x being object st x
in dom f /\ dom g holds F.x = F(x) from FUNCT_1:sch 3;
hence thesis;
end;
uniqueness
proof
let F,G be Function such that
A1: dom F = dom f /\ dom g and
A2: for x being object st x in dom F holds F.x = F(x) and
A3: dom G = dom f /\ dom g and
A4: for x being object st x in dom G holds G.x = F(x);
thus dom F = dom G by A1,A3;
let x be object;
assume
A5: x in dom F;
hence F.x = F(x) by A2
.= G.x by A1,A3,A4,A5;
end;
end;
definition
let X;
let Y be complex-functions-membered set;
let f be PartFunc of X,Y;
let g be complex-valued Function;
redefine func f<#>g -> PartFunc of X /\ dom g, C_PFuncs(DOMS(Y)); :: redefines <#> (VALUED_2, definition)
coherence
proof
set h = f<#>g;
A1: dom h = dom f /\ dom g by Def43;
rng h c= C_PFuncs(DOMS(Y))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
A4: h.x = f.x (#) g.x by A2,Def43;
then reconsider y as Function by A3;
A5: rng y c= COMPLEX
by A3,A4,XCMPLX_0:def 2;
x in dom f by A1,A2,XBOOLE_0:def 4;
then f.x in Y by PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y;
then
A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74;
dom y = dom(f.x) by A3,A4,VALUED_1:def 5;
then y is PartFunc of DOMS(Y),COMPLEX by A6,A5,RELSET_1:4;
hence thesis by Def8;
end;
hence thesis by A1,RELSET_1:4,XBOOLE_1:27;
end;
end;
definition
let X;
let Y be real-functions-membered set;
let f be PartFunc of X,Y;
let g be real-valued Function;
redefine func f<#>g -> PartFunc of X /\ dom g, R_PFuncs(DOMS(Y)); :: redefines <#> (VALUED_2, definition)
coherence
proof
set h = f<#>g;
A1: dom h = dom f /\ dom g by Def43;
rng h c= R_PFuncs(DOMS(Y))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = f.x (#) g.x by A2,Def43;
A5: rng y c= REAL
by A3,A4,XREAL_0:def 1;
x in dom f by A1,A2,XBOOLE_0:def 4;
then f.x in Y by PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y;
then
A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74;
dom y = dom(f.x) by A3,A4,VALUED_1:def 5;
then y is PartFunc of DOMS(Y),REAL by A6,A5,RELSET_1:4;
hence thesis by Def12;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
definition
let X;
let Y be rational-functions-membered set;
let f be PartFunc of X,Y;
let g be RAT-valued Function;
redefine func f<#>g -> PartFunc of X /\ dom g, Q_PFuncs(DOMS(Y)); :: redefines <#> (VALUED_2, definition)
coherence
proof
set h = f<#>g;
A1: dom h = dom f /\ dom g by Def43;
rng h c= Q_PFuncs(DOMS(Y))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = f.x (#) g.x by A2,Def43;
A5: rng y c= RAT
by A3,A4,RAT_1:def 2;
x in dom f by A1,A2,XBOOLE_0:def 4;
then f.x in Y by PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y;
then
A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74;
dom y = dom(f.x) by A3,A4,VALUED_1:def 5;
then y is PartFunc of DOMS(Y),RAT by A6,A5,RELSET_1:4;
hence thesis by Def14;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
definition
let X;
let Y be integer-functions-membered set;
let f be PartFunc of X,Y;
let g be INT-valued Function;
redefine func f<#>g -> PartFunc of X /\ dom g, I_PFuncs(DOMS(Y)); :: redefines <#> (VALUED_2, definition)
coherence
proof
set h = f<#>g;
A1: dom h = dom f /\ dom g by Def43;
rng h c= I_PFuncs(DOMS(Y))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = f.x (#) g.x by A2,Def43;
A5: rng y c= INT
by A3,A4,INT_1:def 2;
x in dom f by A1,A2,XBOOLE_0:def 4;
then f.x in Y by PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y;
then
A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74;
dom y = dom(f.x) by A3,A4,VALUED_1:def 5;
then y is PartFunc of DOMS(Y),INT by A6,A5,RELSET_1:4;
hence thesis by Def16;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
definition
let X;
let Y be natural-functions-membered set;
let f be PartFunc of X,Y;
let g be natural-valued Function;
redefine func f<#>g -> PartFunc of X /\ dom g, N_PFuncs(DOMS(Y)); :: redefines <#> (VALUED_2, definition)
coherence
proof
set h = f<#>g;
A1: dom h = dom f /\ dom g by Def43;
rng h c= N_PFuncs(DOMS(Y))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = f.x (#) g.x by A2,Def43;
A5: rng y c= NAT
by A3,A4,ORDINAL1:def 12;
x in dom f by A1,A2,XBOOLE_0:def 4;
then f.x in Y by PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y;
then
A6: dom(f.x) c= DOMS(Y) by ZFMISC_1:74;
dom y = dom(f.x) by A3,A4,VALUED_1:def 5;
then y is PartFunc of DOMS(Y),NAT by A6,A5,RELSET_1:4;
hence thesis by Def18;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
theorem
f <#> -g = (<->f) <#> g
proof
set f1 = <->f;
A1: dom f1 = dom f & dom(f<#>-g) = dom f /\ dom -g by Def33,Def43;
dom(f1<#>g) = dom f1 /\ dom g by Def43;
hence
A2: dom(f<#>-g) = dom(f1<#>g) by A1,VALUED_1:8;
let x be object;
assume
A3: x in dom(f<#>-g);
then
A4: x in dom f1 by A1,XBOOLE_0:def 4;
thus (f<#>-g).x = f.x (#) (-g).x by A3,Def43
.= f.x(#)-g.x by VALUED_1:8
.= (-f.x)(#)g.x by Th22
.= f1.x(#)g.x by A4,Def33
.= (f1<#>g).x by A2,A3,Def43;
end;
theorem
f <#> -g = <-> (f <#> g)
proof
set f1 = f<#>g;
A1: dom(<->f1) = dom f1 by Def33;
dom f1 = dom f /\ dom g & dom(f<#>-g) = dom f /\ dom -g by Def43;
hence
A2: dom(f<#>-g) = dom(<->f1) by A1,VALUED_1:8;
let x be object;
assume
A3: x in dom(f<#>-g);
hence (f<#>-g).x = f.x (#) (-g).x by Def43
.= f.x(#)-g.x by VALUED_1:8
.= -(f.x(#)g.x) by Th24
.= -f1.x by A1,A2,A3,Def43
.= (<->f1).x by A2,A3,Def33;
end;
theorem
f <#> g <#> h = f <#> (g(#)h)
proof
set f1 = f<#>g;
A1: dom(g(#)h) = dom g /\ dom h by VALUED_1:def 4;
A2: dom(f1<#>h) = dom f1 /\ dom h by Def43;
dom f1 = dom f /\ dom g & dom(f<#>(g(#)h)) = dom f /\ dom(g(#)h) by Def43;
hence
A3: dom(f1<#>h) = dom(f<#>(g(#)h)) by A2,A1,XBOOLE_1:16;
let x be object;
assume
A4: x in dom(f1<#>h);
then
A5: x in dom f1 by A2,XBOOLE_0:def 4;
A6: x in dom(g(#)h) by A3,A4,XBOOLE_0:def 4;
thus (f1<#>h).x = f1.x (#) h.x by A4,Def43
.= f.x (#) g.x (#) h.x by A5,Def43
.= f.x (#) (g.x * h.x) by Th16
.= f.x (#) ((g(#)h).x) by A6,VALUED_1:def 4
.= (f<#>(g(#)h)).x by A3,A4,Def43;
end;
definition
let Y be complex-functions-membered set;
let f be Y-valued Function;
let g be complex-valued Function;
func f</>g -> Function equals
f <#> (g");
coherence;
end;
theorem Th71:
dom(f</>g) = dom f /\ dom g
proof
thus dom(f</>g) = dom f /\ dom(g") by Def43
.= dom f /\ dom g by VALUED_1:def 7;
end;
theorem Th72:
x in dom(f</>g) implies (f</>g).x = f.x (/) g.x
proof
assume x in dom(f</>g);
hence (f</>g).x = f.x (#) (g").x by Def43
.= f.x (/) g.x by VALUED_1:10;
end;
definition
let X;
let Y be complex-functions-membered set;
let f be PartFunc of X,Y;
let g be complex-valued Function;
redefine func f</>g -> PartFunc of X /\ dom g, C_PFuncs(DOMS(Y)); :: redefines </> (VALUED_2, definition)
coherence
proof
f</>g = f <#> (g");
hence thesis by VALUED_1:def 7;
end;
end;
definition
let X;
let Y be real-functions-membered set;
let f be PartFunc of X,Y;
let g be real-valued Function;
redefine func f</>g -> PartFunc of X /\ dom g, R_PFuncs(DOMS(Y)); :: redefines </> (VALUED_2, definition)
coherence
proof
f</>g = f <#> (g");
hence thesis by VALUED_1:def 7;
end;
end;
definition
let X;
let Y be rational-functions-membered set;
let f be PartFunc of X,Y;
let g be RAT-valued Function;
redefine func f</>g -> PartFunc of X /\ dom g, Q_PFuncs(DOMS(Y)); :: redefines </> (VALUED_2, definition)
coherence
proof
f</>g = f <#> (g");
hence thesis by VALUED_1:def 7;
end;
end;
theorem
f <#> g </> h = f <#> (g/"h)
proof
set f1 = f<#>g;
A1: dom(g/"h) = dom g /\ dom h by VALUED_1:16;
A2: dom(f1</>h) = dom f1 /\ dom h by Th71;
dom f1 = dom f /\ dom g & dom(f<#>(g/"h)) = dom f /\ dom(g/"h) by Def43;
hence
A3: dom(f1</>h) = dom(f<#>(g/"h)) by A2,A1,XBOOLE_1:16;
let x be object;
assume
A4: x in dom(f1</>h);
then
A5: x in dom f1 by A2,XBOOLE_0:def 4;
thus (f1</>h).x = f1.x (/) h.x by A4,Th72
.= f.x (#) g.x (/) h.x by A5,Def43
.= f.x (#) (g.x / h.x) by Th16
.= f.x (#) ((g/"h).x) by VALUED_1:17
.= (f<#>(g/"h)).x by A3,A4,Def43;
end;
definition
let Y1, Y2 be complex-functions-membered set;
let f be Y1-valued Function;
let g be Y2-valued Function;
deffunc F(object) = f.$1+g.$1;
func f<++>g -> Function means
:Def45:
dom it = dom f /\ dom g & for x being
object st x in dom it holds it.x = f.x + g.x;
existence
proof
ex F being Function st dom F = dom f /\ dom g & for x being object st x
in dom f /\ dom g holds F.x = F(x) from FUNCT_1:sch 3;
hence thesis;
end;
uniqueness
proof
let F,G be Function such that
A1: dom F = dom f /\ dom g and
A2: for x being object st x in dom F holds F.x = F(x) and
A3: dom G = dom f /\ dom g and
A4: for x being object st x in dom G holds G.x = F(x);
thus dom F = dom G by A1,A3;
let x be object;
assume
A5: x in dom F;
hence F.x = F(x) by A2
.= G.x by A1,A3,A4,A5;
end;
end;
definition
let X1, X2 be set;
let Y1, Y2 be complex-functions-membered set;
let f be PartFunc of X1,Y1;
let g be PartFunc of X2,Y2;
redefine func f<++>g -> PartFunc of X1 /\ X2, C_PFuncs(DOMS(Y1)/\DOMS(Y2)); :: redefines <++> (VALUED_2, definition)
coherence
proof
set h = f<++>g;
A1: dom h = dom f /\ dom g by Def45;
rng h c= C_PFuncs(DOMS(Y1)/\DOMS(Y2))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
A4: h.x = f.x + g.x by A2,Def45;
then reconsider y as Function by A3;
A5: rng y c= COMPLEX
by A3,A4,XCMPLX_0:def 2;
x in dom g by A1,A2,XBOOLE_0:def 4;
then g.x in Y2 by PARTFUN1:4;
then dom(g.x) in the set of all dom m where m is Element of Y2;
then
A6: dom(g.x) c= DOMS(Y2) by ZFMISC_1:74;
x in dom f by A1,A2,XBOOLE_0:def 4;
then f.x in Y1 by PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y1;
then
A7: dom(f.x) c= DOMS(Y1) by ZFMISC_1:74;
dom y = dom(f.x) /\ dom(g.x) by A3,A4,VALUED_1:def 1;
then y is PartFunc of DOMS(Y1)/\DOMS(Y2),COMPLEX by A7,A6,A5,RELSET_1:4
,XBOOLE_1:27;
hence thesis by Def8;
end;
hence thesis by A1,RELSET_1:4,XBOOLE_1:27;
end;
end;
definition
let X1, X2 be set;
let Y1, Y2 be real-functions-membered set;
let f be PartFunc of X1,Y1;
let g be PartFunc of X2,Y2;
redefine func f<++>g -> PartFunc of X1 /\ X2, R_PFuncs(DOMS(Y1)/\DOMS(Y2)); :: redefines <++> (VALUED_2, definition)
coherence
proof
set h = f<++>g;
A1: dom h = dom f /\ dom g by Def45;
rng h c= R_PFuncs(DOMS(Y1)/\DOMS(Y2))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = f.x + g.x by A2,Def45;
A5: rng y c= REAL
by A3,A4,XREAL_0:def 1;
x in dom g by A1,A2,XBOOLE_0:def 4;
then g.x in Y2 by PARTFUN1:4;
then dom(g.x) in the set of all dom m where m is Element of Y2;
then
A6: dom(g.x) c= DOMS(Y2) by ZFMISC_1:74;
x in dom f by A1,A2,XBOOLE_0:def 4;
then f.x in Y1 by PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y1;
then
A7: dom(f.x) c= DOMS(Y1) by ZFMISC_1:74;
dom y = dom(f.x) /\ dom(g.x) by A3,A4,VALUED_1:def 1;
then y is PartFunc of DOMS(Y1)/\DOMS(Y2),REAL by A7,A6,A5,RELSET_1:4
,XBOOLE_1:27;
hence thesis by Def12;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
definition
let X1, X2 be set;
let Y1, Y2 be rational-functions-membered set;
let f be PartFunc of X1,Y1;
let g be PartFunc of X2,Y2;
redefine func f<++>g -> PartFunc of X1 /\ X2, Q_PFuncs(DOMS(Y1)/\DOMS(Y2)); :: redefines <++> (VALUED_2, definition)
coherence
proof
set h = f<++>g;
A1: dom h = dom f /\ dom g by Def45;
rng h c= Q_PFuncs(DOMS(Y1)/\DOMS(Y2))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = f.x + g.x by A2,Def45;
A5: rng y c= RAT
by A3,A4,RAT_1:def 2;
x in dom g by A1,A2,XBOOLE_0:def 4;
then g.x in Y2 by PARTFUN1:4;
then dom(g.x) in the set of all dom m where m is Element of Y2;
then
A6: dom(g.x) c= DOMS(Y2) by ZFMISC_1:74;
x in dom f by A1,A2,XBOOLE_0:def 4;
then f.x in Y1 by PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y1;
then
A7: dom(f.x) c= DOMS(Y1) by ZFMISC_1:74;
dom y = dom(f.x) /\ dom(g.x) by A3,A4,VALUED_1:def 1;
then y is PartFunc of DOMS(Y1)/\DOMS(Y2),RAT by A7,A6,A5,RELSET_1:4
,XBOOLE_1:27;
hence thesis by Def14;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
definition
let X1, X2 be set;
let Y1, Y2 be integer-functions-membered set;
let f be PartFunc of X1,Y1;
let g be PartFunc of X2,Y2;
redefine func f<++>g -> PartFunc of X1 /\ X2, I_PFuncs(DOMS(Y1)/\DOMS(Y2)); :: redefines <++> (VALUED_2, definition)
coherence
proof
set h = f<++>g;
A1: dom h = dom f /\ dom g by Def45;
rng h c= I_PFuncs(DOMS(Y1)/\DOMS(Y2))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = f.x + g.x by A2,Def45;
A5: rng y c= INT
by A3,A4,INT_1:def 2;
x in dom g by A1,A2,XBOOLE_0:def 4;
then g.x in Y2 by PARTFUN1:4;
then dom(g.x) in the set of all dom m where m is Element of Y2;
then
A6: dom(g.x) c= DOMS(Y2) by ZFMISC_1:74;
x in dom f by A1,A2,XBOOLE_0:def 4;
then f.x in Y1 by PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y1;
then
A7: dom(f.x) c= DOMS(Y1) by ZFMISC_1:74;
dom y = dom(f.x) /\ dom(g.x) by A3,A4,VALUED_1:def 1;
then y is PartFunc of DOMS(Y1)/\DOMS(Y2),INT by A7,A6,A5,RELSET_1:4
,XBOOLE_1:27;
hence thesis by Def16;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
definition
let X1, X2 be set;
let Y1, Y2 be natural-functions-membered set;
let f be PartFunc of X1,Y1;
let g be PartFunc of X2,Y2;
redefine func f<++>g -> PartFunc of X1 /\ X2, N_PFuncs(DOMS(Y1)/\DOMS(Y2)); :: redefines <++> (VALUED_2, definition)
coherence
proof
set h = f<++>g;
A1: dom h = dom f /\ dom g by Def45;
rng h c= N_PFuncs(DOMS(Y1)/\DOMS(Y2))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = f.x + g.x by A2,Def45;
A5: rng y c= NAT
by A3,A4,ORDINAL1:def 12;
x in dom g by A1,A2,XBOOLE_0:def 4;
then g.x in Y2 by PARTFUN1:4;
then dom(g.x) in the set of all dom m where m is Element of Y2;
then
A6: dom(g.x) c= DOMS(Y2) by ZFMISC_1:74;
x in dom f by A1,A2,XBOOLE_0:def 4;
then f.x in Y1 by PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y1;
then
A7: dom(f.x) c= DOMS(Y1) by ZFMISC_1:74;
dom y = dom(f.x) /\ dom(g.x) by A3,A4,VALUED_1:def 1;
then y is PartFunc of DOMS(Y1)/\DOMS(Y2),NAT by A7,A6,A5,RELSET_1:4
,XBOOLE_1:27;
hence thesis by Def18;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
theorem
f1 <++> f2 = f2 <++> f1
proof
dom(f1<++>f2) = dom f1 /\ dom f2 by Def45;
hence
A1: dom(f1<++>f2) = dom(f2<++>f1) by Def45;
let x be object;
assume
A2: x in dom(f1<++>f2);
hence (f1<++>f2).x = f1.x + f2.x by Def45
.= (f2<++>f1).x by A1,A2,Def45;
end;
theorem
f <++> f1 <++> f2 = f <++> (f1 <++> f2)
proof
set f3 = f<++>f1, f4 = f1<++>f2;
A1: dom(f3<++>f2) = dom f3 /\ dom f2 by Def45;
A2: dom(f<++>f4) = dom f /\ dom f4 by Def45;
dom f3 = dom f /\ dom f1 & dom f4 = dom f1 /\ dom f2 by Def45;
hence
A3: dom(f3<++>f2) = dom(f<++>f4) by A1,A2,XBOOLE_1:16;
let x be object;
assume
A4: x in dom(f3<++>f2);
then
A5: x in dom f4 by A2,A3,XBOOLE_0:def 4;
A6: x in dom f3 by A1,A4,XBOOLE_0:def 4;
thus (f3<++>f2).x = f3.x + f2.x by A4,Def45
.= f.x + f1.x + f2.x by A6,Def45
.= f.x + (f1.x + f2.x) by RFUNCT_1:8
.= f.x + f4.x by A5,Def45
.= (f<++>f4).x by A3,A4,Def45;
end;
theorem
<-> (f1 <++> f2) = (<->f1) <++> (<->f2)
proof
set f3 = f1 <++> f2, f4 = <->f1, f5 = <->f2;
A1: dom(f1 <++> f2) = dom f1 /\ dom f2 by Def45;
A2: dom <->f2 = dom f2 by Def33;
A3: dom <->f3 = dom f3 by Def33;
A4: dom <->f1 = dom f1 by Def33;
hence
A5: dom(<->f3) = dom(f4<++>f5) by A1,A2,A3,Def45;
let x be object;
assume
A6: x in dom(<->f3);
then
A7: x in dom f4 by A1,A4,A3,XBOOLE_0:def 4;
A8: x in dom f5 by A1,A2,A3,A6,XBOOLE_0:def 4;
thus (<->f3).x = -f3.x by A6,Def33
.= -(f1.x+f2.x) by A3,A6,Def45
.= -f1.x-f2.x by Th17
.= f4.x + -f2.x by A7,Def33
.= f4.x + f5.x by A8,Def33
.= (f4<++>f5).x by A5,A6,Def45;
end;
definition
let Y1, Y2 be complex-functions-membered set;
let f be Y1-valued Function;
let g be Y2-valued Function;
deffunc F(object) = f.$1-g.$1;
func f<-->g -> Function means
:Def46:
dom it = dom f /\ dom g & for x being
object st x in dom it holds it.x = f.x - g.x;
existence
proof
ex F being Function st dom F = dom f /\ dom g & for x being object st x
in dom f /\ dom g holds F.x = F(x) from FUNCT_1:sch 3;
hence thesis;
end;
uniqueness
proof
let F,G be Function such that
A1: dom F = dom f /\ dom g and
A2: for x being object st x in dom F holds F.x = F(x) and
A3: dom G = dom f /\ dom g and
A4: for x being object st x in dom G holds G.x = F(x);
thus dom F = dom G by A1,A3;
let x be object;
assume
A5: x in dom F;
hence F.x = F(x) by A2
.= G.x by A1,A3,A4,A5;
end;
end;
definition
let X1, X2 be set;
let Y1, Y2 be complex-functions-membered set;
let f be PartFunc of X1,Y1;
let g be PartFunc of X2,Y2;
redefine func f<-->g -> PartFunc of X1 /\ X2, C_PFuncs(DOMS(Y1)/\DOMS(Y2)); :: redefines <--> (VALUED_2, definition)
coherence
proof
set h = f<-->g;
A1: dom h = dom f /\ dom g by Def46;
rng h c= C_PFuncs(DOMS(Y1)/\DOMS(Y2))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
A4: h.x = f.x - g.x by A2,Def46;
then reconsider y as Function by A3;
A5: rng y c= COMPLEX
by A3,A4,XCMPLX_0:def 2;
x in dom g by A1,A2,XBOOLE_0:def 4;
then g.x in Y2 by PARTFUN1:4;
then dom(g.x) in the set of all dom m where m is Element of Y2;
then
A6: dom(g.x) c= DOMS(Y2) by ZFMISC_1:74;
x in dom f by A1,A2,XBOOLE_0:def 4;
then f.x in Y1 by PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y1;
then
A7: dom(f.x) c= DOMS(Y1) by ZFMISC_1:74;
dom y = dom(f.x) /\ dom(g.x) by A3,A4,VALUED_1:12;
then y is PartFunc of DOMS(Y1)/\DOMS(Y2),COMPLEX by A7,A6,A5,RELSET_1:4
,XBOOLE_1:27;
hence thesis by Def8;
end;
hence thesis by A1,RELSET_1:4,XBOOLE_1:27;
end;
end;
definition
let X1, X2 be set;
let Y1, Y2 be real-functions-membered set;
let f be PartFunc of X1,Y1;
let g be PartFunc of X2,Y2;
redefine func f<-->g -> PartFunc of X1 /\ X2, R_PFuncs(DOMS(Y1)/\DOMS(Y2)); :: redefines <--> (VALUED_2, definition)
coherence
proof
set h = f<-->g;
A1: dom h = dom f /\ dom g by Def46;
rng h c= R_PFuncs(DOMS(Y1)/\DOMS(Y2))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = f.x - g.x by A2,Def46;
A5: rng y c= REAL
by A3,A4,XREAL_0:def 1;
x in dom g by A1,A2,XBOOLE_0:def 4;
then g.x in Y2 by PARTFUN1:4;
then dom(g.x) in the set of all dom m where m is Element of Y2;
then
A6: dom(g.x) c= DOMS(Y2) by ZFMISC_1:74;
x in dom f by A1,A2,XBOOLE_0:def 4;
then f.x in Y1 by PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y1;
then
A7: dom(f.x) c= DOMS(Y1) by ZFMISC_1:74;
dom y = dom(f.x) /\ dom(g.x) by A3,A4,VALUED_1:12;
then y is PartFunc of DOMS(Y1)/\DOMS(Y2),REAL by A7,A6,A5,RELSET_1:4
,XBOOLE_1:27;
hence thesis by Def12;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
definition
let X1, X2 be set;
let Y1, Y2 be rational-functions-membered set;
let f be PartFunc of X1,Y1;
let g be PartFunc of X2,Y2;
redefine func f<-->g -> PartFunc of X1 /\ X2, Q_PFuncs(DOMS(Y1)/\DOMS(Y2)); :: redefines <--> (VALUED_2, definition)
coherence
proof
set h = f<-->g;
A1: dom h = dom f /\ dom g by Def46;
rng h c= Q_PFuncs(DOMS(Y1)/\DOMS(Y2))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = f.x - g.x by A2,Def46;
A5: rng y c= RAT
by A3,A4,RAT_1:def 2;
x in dom g by A1,A2,XBOOLE_0:def 4;
then g.x in Y2 by PARTFUN1:4;
then dom(g.x) in the set of all dom m where m is Element of Y2;
then
A6: dom(g.x) c= DOMS(Y2) by ZFMISC_1:74;
x in dom f by A1,A2,XBOOLE_0:def 4;
then f.x in Y1 by PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y1;
then
A7: dom(f.x) c= DOMS(Y1) by ZFMISC_1:74;
dom y = dom(f.x) /\ dom(g.x) by A3,A4,VALUED_1:12;
then y is PartFunc of DOMS(Y1)/\DOMS(Y2),RAT by A7,A6,A5,RELSET_1:4
,XBOOLE_1:27;
hence thesis by Def14;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
definition
let X1, X2 be set;
let Y1, Y2 be integer-functions-membered set;
let f be PartFunc of X1,Y1;
let g be PartFunc of X2,Y2;
redefine func f<-->g -> PartFunc of X1 /\ X2, I_PFuncs(DOMS(Y1)/\DOMS(Y2)); :: redefines <--> (VALUED_2, definition)
coherence
proof
set h = f<-->g;
A1: dom h = dom f /\ dom g by Def46;
rng h c= I_PFuncs(DOMS(Y1)/\DOMS(Y2))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = f.x - g.x by A2,Def46;
A5: rng y c= INT
by A3,A4,INT_1:def 2;
x in dom g by A1,A2,XBOOLE_0:def 4;
then g.x in Y2 by PARTFUN1:4;
then dom(g.x) in the set of all dom m where m is Element of Y2;
then
A6: dom(g.x) c= DOMS(Y2) by ZFMISC_1:74;
x in dom f by A1,A2,XBOOLE_0:def 4;
then f.x in Y1 by PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y1;
then
A7: dom(f.x) c= DOMS(Y1) by ZFMISC_1:74;
dom y = dom(f.x) /\ dom(g.x) by A3,A4,VALUED_1:12;
then y is PartFunc of DOMS(Y1)/\DOMS(Y2),INT by A7,A6,A5,RELSET_1:4
,XBOOLE_1:27;
hence thesis by Def16;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
theorem
f1 <--> f2 = <-> (f2 <--> f1)
proof
set f = f2<-->f1;
A1: dom(f1<-->f2) = dom f1 /\ dom f2 & dom(f2<-->f1) = dom f2 /\ dom f1 by
Def46;
hence
A2: dom(f1<-->f2) = dom<->f by Def33;
let x be object;
assume
A3: x in dom(f1<-->f2);
hence (f1<-->f2).x = f1.x-f2.x by Def46
.= -(f2.x-f1.x) by Th18
.= -f.x by A1,A3,Def46
.= (<->f).x by A2,A3,Def33;
end;
theorem
<-> (f1 <--> f2) = (<->f1) <++> f2
proof
set f3 = f1 <--> f2, f4 = <->f1;
A1: dom <->f3 = dom f3 by Def33;
A2: dom(f1 <--> f2) = dom f1 /\ dom f2 & dom <->f1 = dom f1 by Def33,Def46;
hence
A3: dom(<->f3) = dom(f4<++>f2) by A1,Def45;
let x be object;
assume
A4: x in dom(<->f3);
then
A5: x in dom f4 by A2,A1,XBOOLE_0:def 4;
thus (<->f3).x = -f3.x by A4,Def33
.= -(f1.x-f2.x) by A1,A4,Def46
.= -f1.x--f2.x by Th17
.= f4.x + f2.x by A5,Def33
.= (f4<++>f2).x by A3,A4,Def45;
end;
theorem
f <++> f1 <--> f2 = f <++> (f1<-->f2)
proof
set f3 = f<++>f1, f4 = f1<-->f2;
A1: dom(f3<-->f2) = dom f3 /\ dom f2 by Def46;
A2: dom(f<++>f4) = dom f /\ dom f4 by Def45;
dom f3 = dom f /\ dom f1 & dom f4 = dom f1 /\ dom f2 by Def45,Def46;
hence
A3: dom(f3<-->f2) = dom(f<++>f4) by A1,A2,XBOOLE_1:16;
let x be object;
assume
A4: x in dom(f3<-->f2);
then
A5: x in dom f4 by A2,A3,XBOOLE_0:def 4;
A6: x in dom f3 by A1,A4,XBOOLE_0:def 4;
thus (f3<-->f2).x = f3.x - f2.x by A4,Def46
.= f.x + f1.x - f2.x by A6,Def45
.= f.x + (f1.x - f2.x) by RFUNCT_1:8
.= f.x + f4.x by A5,Def46
.= (f<++>f4).x by A3,A4,Def45;
end;
theorem
f <--> f1 <++> f2 = f <--> (f1 <--> f2)
proof
set f3 = f<-->f1, f4 = f1<-->f2;
A1: dom(f3<++>f2) = dom f3 /\ dom f2 by Def45;
A2: dom(f<-->f4) = dom f /\ dom f4 by Def46;
dom f3 = dom f /\ dom f1 & dom f4 = dom f1 /\ dom f2 by Def46;
hence
A3: dom(f3<++>f2) = dom(f<-->f4) by A1,A2,XBOOLE_1:16;
let x be object;
assume
A4: x in dom(f3<++>f2);
then
A5: x in dom f4 by A2,A3,XBOOLE_0:def 4;
A6: x in dom f3 by A1,A4,XBOOLE_0:def 4;
thus (f3<++>f2).x = f3.x + f2.x by A4,Def45
.= f.x - f1.x + f2.x by A6,Def46
.= f.x - (f1.x - f2.x) by RFUNCT_1:22
.= f.x - f4.x by A5,Def46
.= (f<-->f4).x by A3,A4,Def46;
end;
theorem
f <--> f1 <--> f2 = f <--> (f1 <++> f2)
proof
set f3 = f<-->f1, f4 = f1<++>f2;
A1: dom(f3<-->f2) = dom f3 /\ dom f2 by Def46;
A2: dom(f<-->f4) = dom f /\ dom f4 by Def46;
dom f3 = dom f /\ dom f1 & dom f4 = dom f1 /\ dom f2 by Def45,Def46;
hence
A3: dom(f3<-->f2) = dom(f<-->f4) by A1,A2,XBOOLE_1:16;
let x be object;
assume
A4: x in dom(f3<-->f2);
then
A5: x in dom f4 by A2,A3,XBOOLE_0:def 4;
A6: x in dom f3 by A1,A4,XBOOLE_0:def 4;
thus (f3<-->f2).x = f3.x - f2.x by A4,Def46
.= f.x - f1.x - f2.x by A6,Def46
.= f.x - (f1.x + f2.x) by RFUNCT_1:20
.= f.x - f4.x by A5,Def45
.= (f<-->f4).x by A3,A4,Def46;
end;
theorem
f <--> f1 <--> f2 = f <--> f2 <--> f1
proof
set f3 = f<-->f1, f4 = f<-->f2;
A1: dom(f3<-->f2) = dom f3 /\ dom f2 by Def46;
A2: dom(f4<-->f1) = dom f4 /\ dom f1 by Def46;
dom f3 = dom f /\ dom f1 & dom f4 = dom f /\ dom f2 by Def46;
hence
A3: dom(f3<-->f2) = dom(f4<-->f1) by A1,A2,XBOOLE_1:16;
let x be object;
assume
A4: x in dom(f3<-->f2);
then
A5: x in dom f4 by A2,A3,XBOOLE_0:def 4;
A6: x in dom f3 by A1,A4,XBOOLE_0:def 4;
thus (f3<-->f2).x = f3.x - f2.x by A4,Def46
.= f.x - f1.x - f2.x by A6,Def46
.= f.x - f2.x - f1.x by RFUNCT_1:23
.= f4.x - f1.x by A5,Def46
.= (f4<-->f1).x by A3,A4,Def46;
end;
definition
let Y1, Y2 be complex-functions-membered set;
let f be Y1-valued Function;
let g be Y2-valued Function;
deffunc F(object) = f.$1(#)g.$1;
func f<##>g -> Function means
:Def47:
dom it = dom f /\ dom g & for x being
object st x in dom it holds it.x = f.x (#) g.x;
existence
proof
ex F being Function st dom F = dom f /\ dom g & for x being object st x
in dom f /\ dom g holds F.x = F(x) from FUNCT_1:sch 3;
hence thesis;
end;
uniqueness
proof
let F,G be Function such that
A1: dom F = dom f /\ dom g and
A2: for x being object st x in dom F holds F.x = F(x) and
A3: dom G = dom f /\ dom g and
A4: for x being object st x in dom G holds G.x = F(x);
thus dom F = dom G by A1,A3;
let x be object;
assume
A5: x in dom F;
hence F.x = F(x) by A2
.= G.x by A1,A3,A4,A5;
end;
end;
definition
let X1, X2 be set;
let Y1, Y2 be complex-functions-membered set;
let f be PartFunc of X1,Y1;
let g be PartFunc of X2,Y2;
redefine func f<##>g -> PartFunc of X1 /\ X2, C_PFuncs(DOMS(Y1)/\DOMS(Y2)); :: redefines <##> (VALUED_2, definition)
coherence
proof
set h = f<##>g;
A1: dom h = dom f /\ dom g by Def47;
rng h c= C_PFuncs(DOMS(Y1)/\DOMS(Y2))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
A4: h.x = f.x (#) g.x by A2,Def47;
then reconsider y as Function by A3;
A5: rng y c= COMPLEX
by A3,A4,XCMPLX_0:def 2;
x in dom g by A1,A2,XBOOLE_0:def 4;
then g.x in Y2 by PARTFUN1:4;
then dom(g.x) in the set of all dom m where m is Element of Y2;
then
A6: dom(g.x) c= DOMS(Y2) by ZFMISC_1:74;
x in dom f by A1,A2,XBOOLE_0:def 4;
then f.x in Y1 by PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y1;
then
A7: dom(f.x) c= DOMS(Y1) by ZFMISC_1:74;
dom y = dom(f.x) /\ dom(g.x) by A3,A4,VALUED_1:def 4;
then y is PartFunc of DOMS(Y1)/\DOMS(Y2),COMPLEX by A7,A6,A5,RELSET_1:4
,XBOOLE_1:27;
hence thesis by Def8;
end;
hence thesis by A1,RELSET_1:4,XBOOLE_1:27;
end;
end;
definition
let X1, X2 be set;
let Y1, Y2 be real-functions-membered set;
let f be PartFunc of X1,Y1;
let g be PartFunc of X2,Y2;
redefine func f<##>g -> PartFunc of X1 /\ X2, R_PFuncs(DOMS(Y1)/\DOMS(Y2)); :: redefines <##> (VALUED_2, definition)
coherence
proof
set h = f<##>g;
A1: dom h = dom f /\ dom g by Def47;
rng h c= R_PFuncs(DOMS(Y1)/\DOMS(Y2))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = f.x (#) g.x by A2,Def47;
A5: rng y c= REAL
by A3,A4,XREAL_0:def 1;
x in dom g by A1,A2,XBOOLE_0:def 4;
then g.x in Y2 by PARTFUN1:4;
then dom(g.x) in the set of all dom m where m is Element of Y2;
then
A6: dom(g.x) c= DOMS(Y2) by ZFMISC_1:74;
x in dom f by A1,A2,XBOOLE_0:def 4;
then f.x in Y1 by PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y1;
then
A7: dom(f.x) c= DOMS(Y1) by ZFMISC_1:74;
dom y = dom(f.x) /\ dom(g.x) by A3,A4,VALUED_1:def 4;
then y is PartFunc of DOMS(Y1)/\DOMS(Y2),REAL by A7,A6,A5,RELSET_1:4
,XBOOLE_1:27;
hence thesis by Def12;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
definition
let X1, X2 be set;
let Y1, Y2 be rational-functions-membered set;
let f be PartFunc of X1,Y1;
let g be PartFunc of X2,Y2;
redefine func f<##>g -> PartFunc of X1 /\ X2, Q_PFuncs(DOMS(Y1)/\DOMS(Y2)); :: redefines <##> (VALUED_2, definition)
coherence
proof
set h = f<##>g;
A1: dom h = dom f /\ dom g by Def47;
rng h c= Q_PFuncs(DOMS(Y1)/\DOMS(Y2))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = f.x (#) g.x by A2,Def47;
A5: rng y c= RAT
by A3,A4,RAT_1:def 2;
x in dom g by A1,A2,XBOOLE_0:def 4;
then g.x in Y2 by PARTFUN1:4;
then dom(g.x) in the set of all dom m where m is Element of Y2;
then
A6: dom(g.x) c= DOMS(Y2) by ZFMISC_1:74;
x in dom f by A1,A2,XBOOLE_0:def 4;
then f.x in Y1 by PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y1;
then
A7: dom(f.x) c= DOMS(Y1) by ZFMISC_1:74;
dom y = dom(f.x) /\ dom(g.x) by A3,A4,VALUED_1:def 4;
then y is PartFunc of DOMS(Y1)/\DOMS(Y2),RAT by A7,A6,A5,RELSET_1:4
,XBOOLE_1:27;
hence thesis by Def14;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
definition
let X1, X2 be set;
let Y1, Y2 be integer-functions-membered set;
let f be PartFunc of X1,Y1;
let g be PartFunc of X2,Y2;
redefine func f<##>g -> PartFunc of X1 /\ X2, I_PFuncs(DOMS(Y1)/\DOMS(Y2)); :: redefines <##> (VALUED_2, definition)
coherence
proof
set h = f<##>g;
A1: dom h = dom f /\ dom g by Def47;
rng h c= I_PFuncs(DOMS(Y1)/\DOMS(Y2))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = f.x (#) g.x by A2,Def47;
A5: rng y c= INT
by A3,A4,INT_1:def 2;
x in dom g by A1,A2,XBOOLE_0:def 4;
then g.x in Y2 by PARTFUN1:4;
then dom(g.x) in the set of all dom m where m is Element of Y2;
then
A6: dom(g.x) c= DOMS(Y2) by ZFMISC_1:74;
x in dom f by A1,A2,XBOOLE_0:def 4;
then f.x in Y1 by PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y1;
then
A7: dom(f.x) c= DOMS(Y1) by ZFMISC_1:74;
dom y = dom(f.x) /\ dom(g.x) by A3,A4,VALUED_1:def 4;
then y is PartFunc of DOMS(Y1)/\DOMS(Y2),INT by A7,A6,A5,RELSET_1:4
,XBOOLE_1:27;
hence thesis by Def16;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
definition
let X1, X2 be set;
let Y1, Y2 be natural-functions-membered set;
let f be PartFunc of X1,Y1;
let g be PartFunc of X2,Y2;
redefine func f<##>g -> PartFunc of X1 /\ X2, N_PFuncs(DOMS(Y1)/\DOMS(Y2)); :: redefines <##> (VALUED_2, definition)
coherence
proof
set h = f<##>g;
A1: dom h = dom f /\ dom g by Def47;
rng h c= N_PFuncs(DOMS(Y1)/\DOMS(Y2))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = f.x (#) g.x by A2,Def47;
A5: rng y c= NAT
by A3,A4,ORDINAL1:def 12;
x in dom g by A1,A2,XBOOLE_0:def 4;
then g.x in Y2 by PARTFUN1:4;
then dom(g.x) in the set of all dom m where m is Element of Y2;
then
A6: dom(g.x) c= DOMS(Y2) by ZFMISC_1:74;
x in dom f by A1,A2,XBOOLE_0:def 4;
then f.x in Y1 by PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y1;
then
A7: dom(f.x) c= DOMS(Y1) by ZFMISC_1:74;
dom y = dom(f.x) /\ dom(g.x) by A3,A4,VALUED_1:def 4;
then y is PartFunc of DOMS(Y1)/\DOMS(Y2),NAT by A7,A6,A5,RELSET_1:4
,XBOOLE_1:27;
hence thesis by Def18;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
theorem Th83:
f1 <##> f2 = f2 <##> f1
proof
dom(f1<##>f2) = dom f1 /\ dom f2 by Def47;
hence
A1: dom(f1<##>f2) = dom(f2<##>f1) by Def47;
let x be object;
assume
A2: x in dom(f1<##>f2);
hence (f1<##>f2).x = f1.x (#) f2.x by Def47
.= (f2<##>f1).x by A1,A2,Def47;
end;
theorem
(f <##> f1) <##> f2 = f <##> (f1 <##> f2)
proof
set f3 = f<##>f1, f4 = f1<##>f2;
A1: dom(f3<##>f2) = dom f3 /\ dom f2 by Def47;
A2: dom(f<##>f4) = dom f /\ dom f4 by Def47;
dom f3 = dom f /\ dom f1 & dom f4 = dom f1 /\ dom f2 by Def47;
hence
A3: dom(f3<##>f2) = dom(f<##>f4) by A1,A2,XBOOLE_1:16;
let x be object;
assume
A4: x in dom(f3<##>f2);
then
A5: x in dom f4 by A2,A3,XBOOLE_0:def 4;
A6: x in dom f3 by A1,A4,XBOOLE_0:def 4;
thus (f3<##>f2).x = f3.x (#) f2.x by A4,Def47
.= f.x (#) f1.x (#) f2.x by A6,Def47
.= f.x (#) (f1.x (#) f2.x) by RFUNCT_1:9
.= f.x (#) f4.x by A5,Def47
.= (f<##>f4).x by A3,A4,Def47;
end;
theorem
(<->f1) <##> f2 = <-> (f1<##>f2)
proof
set f3 = f1<##>f2, f4 = <->f1;
A1: dom f3 = dom f1 /\ dom f2 & dom f4 = dom f1 by Def33,Def47;
dom(f4<##>f2) = dom f4 /\ dom f2 by Def47;
hence
A2: dom(f4<##>f2) = dom(<->f3) by A1,Def33;
let x be object;
assume
A3: x in dom(f4<##>f2);
then
A4: x in dom f3 by A1,Def47;
then
A5: x in dom <->f1 by A1,XBOOLE_0:def 4;
thus (f4<##>f2).x = f4.x (#) f2.x by A3,Def47
.= (-(f1.x)) (#) f2.x by A5,Def33
.= -(f1.x) (#) f2.x by Th25
.= -f3.x by A4,Def47
.= (<->f3).x by A2,A3,Def33;
end;
theorem
f1 <##> <->f2 = <-> (f1<##>f2)
proof
set f3 = f1<##>f2, f4 = <->f2;
A1: dom f3 = dom f1 /\ dom f2 & dom f4 = dom f2 by Def33,Def47;
dom(f1<##>f4) = dom f1 /\ dom f4 by Def47;
hence
A2: dom(f1<##>f4) = dom(<->f3) by A1,Def33;
let x be object;
assume
A3: x in dom(f1<##>f4);
then
A4: x in dom f3 by A1,Def47;
then
A5: x in dom <->f2 by A1,XBOOLE_0:def 4;
thus (f1<##>f4).x = f1.x (#) f4.x by A3,Def47
.= f1.x (#) -f2.x by A5,Def33
.= -(f1.x) (#) f2.x by Th25
.= -f3.x by A4,Def47
.= (<->f3).x by A2,A3,Def33;
end;
theorem Th87:
f <##> (f1<++>f2) = (f<##>f1) <++> (f<##>f2)
proof
set f3 = f<##>f1, f4 = f<##>f2, f5 = f1<++>f2;
A1: dom(f<##>f5) = dom f /\ dom f5 by Def47;
A2: dom f5 = dom f1 /\ dom f2 by Def45;
A3: dom(f3<++>f4) = dom f3 /\ dom f4 by Def45;
dom f3 = dom f /\ dom f1 & dom f4 = dom f /\ dom f2 by Def47;
hence
A4: dom(f<##>f5) = dom(f3<++>f4) by A1,A3,A2,Lm1;
let x be object;
assume
A5: x in dom(f<##>f5);
then
A6: x in dom f3 by A3,A4,XBOOLE_0:def 4;
A7: x in dom f5 by A1,A5,XBOOLE_0:def 4;
A8: x in dom f4 by A3,A4,A5,XBOOLE_0:def 4;
thus (f<##>f5).x = f.x (#) f5.x by A5,Def47
.= f.x (#) (f1.x + f2.x) by A7,Def45
.= f.x (#) f1.x + f.x (#) f2.x by RFUNCT_1:10
.= f3.x + f.x (#) f2.x by A6,Def47
.= f3.x + f4.x by A8,Def47
.= (f3<++>f4).x by A4,A5,Def45;
end;
theorem
(f1<++>f2) <##> f = (f1<##>f) <++> (f2<##>f)
proof
set f3 = f1<##>f, f4 = f2<##>f, f5 = f1<++>f2;
A1: f1<##>f = f<##>f1 & f2<##>f = f<##>f2 by Th83;
thus f5 <##> f = f <##> f5 by Th83
.= f3 <++> f4 by A1,Th87;
end;
theorem Th89:
f <##> (f1<-->f2) = (f<##>f1) <--> (f<##>f2)
proof
set f3 = f<##>f1, f4 = f<##>f2, f5 = f1<-->f2;
A1: dom(f<##>f5) = dom f /\ dom f5 by Def47;
A2: dom f5 = dom f1 /\ dom f2 by Def46;
A3: dom(f3<-->f4) = dom f3 /\ dom f4 by Def46;
dom f3 = dom f /\ dom f1 & dom f4 = dom f /\ dom f2 by Def47;
hence
A4: dom(f<##>f5) = dom(f3<-->f4) by A1,A3,A2,Lm1;
let x be object;
assume
A5: x in dom(f<##>f5);
then
A6: x in dom f3 by A3,A4,XBOOLE_0:def 4;
A7: x in dom f5 by A1,A5,XBOOLE_0:def 4;
A8: x in dom f4 by A3,A4,A5,XBOOLE_0:def 4;
thus (f<##>f5).x = f.x (#) f5.x by A5,Def47
.= f.x (#) (f1.x - f2.x) by A7,Def46
.= f.x (#) f1.x - f.x (#) f2.x by RFUNCT_1:15
.= f3.x - f.x (#) f2.x by A6,Def47
.= f3.x - f4.x by A8,Def47
.= (f3<-->f4).x by A4,A5,Def46;
end;
theorem
(f1<-->f2) <##> f = (f1<##>f) <--> (f2<##>f)
proof
set f3 = f1<##>f, f4 = f2<##>f, f5 = f1<-->f2;
A1: f1<##>f = f<##>f1 & f2<##>f = f<##>f2 by Th83;
thus f5 <##> f = f <##> f5 by Th83
.= f3 <--> f4 by A1,Th89;
end;
definition
let Y1, Y2 be complex-functions-membered set;
let f be Y1-valued Function;
let g be Y2-valued Function;
deffunc F(object) = f.$1/"g.$1;
func f<//>g -> Function means
:Def48:
dom it = dom f /\ dom g & for x being
object st x in dom it holds it.x = f.x /" g.x;
existence
proof
ex F being Function st dom F = dom f /\ dom g & for x being object st x
in dom f /\ dom g holds F.x = F(x) from FUNCT_1:sch 3;
hence thesis;
end;
uniqueness
proof
let F,G be Function such that
A1: dom F = dom f /\ dom g and
A2: for x being object st x in dom F holds F.x = F(x) and
A3: dom G = dom f /\ dom g and
A4: for x being object st x in dom G holds G.x = F(x);
thus dom F = dom G by A1,A3;
let x be object;
assume
A5: x in dom F;
hence F.x = F(x) by A2
.= G.x by A1,A3,A4,A5;
end;
end;
definition
let X1, X2 be set;
let Y1, Y2 be complex-functions-membered set;
let f be PartFunc of X1,Y1;
let g be PartFunc of X2,Y2;
redefine func f<//>g -> PartFunc of X1 /\ X2, C_PFuncs(DOMS(Y1)/\DOMS(Y2)); :: redefines <//> (VALUED_2, definition)
coherence
proof
set h = f<//>g;
A1: dom h = dom f /\ dom g by Def48;
rng h c= C_PFuncs(DOMS(Y1)/\DOMS(Y2))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
A4: h.x = f.x /" g.x by A2,Def48;
then reconsider y as Function by A3;
A5: rng y c= COMPLEX
by A3,A4,XCMPLX_0:def 2;
x in dom g by A1,A2,XBOOLE_0:def 4;
then g.x in Y2 by PARTFUN1:4;
then dom(g.x) in the set of all dom m where m is Element of Y2;
then
A6: dom(g.x) c= DOMS(Y2) by ZFMISC_1:74;
x in dom f by A1,A2,XBOOLE_0:def 4;
then f.x in Y1 by PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y1;
then
A7: dom(f.x) c= DOMS(Y1) by ZFMISC_1:74;
dom y = dom(f.x) /\ dom(g.x) by A3,A4,VALUED_1:16;
then y is PartFunc of DOMS(Y1)/\DOMS(Y2),COMPLEX by A7,A6,A5,RELSET_1:4
,XBOOLE_1:27;
hence thesis by Def8;
end;
hence thesis by A1,RELSET_1:4,XBOOLE_1:27;
end;
end;
definition
let X1, X2 be set;
let Y1, Y2 be real-functions-membered set;
let f be PartFunc of X1,Y1;
let g be PartFunc of X2,Y2;
redefine func f<//>g -> PartFunc of X1 /\ X2, R_PFuncs(DOMS(Y1)/\DOMS(Y2)); :: redefines <//> (VALUED_2, definition)
coherence
proof
set h = f<//>g;
A1: dom h = dom f /\ dom g by Def48;
rng h c= R_PFuncs(DOMS(Y1)/\DOMS(Y2))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = f.x /" g.x by A2,Def48;
A5: rng y c= REAL
by A3,A4,XREAL_0:def 1;
x in dom g by A1,A2,XBOOLE_0:def 4;
then g.x in Y2 by PARTFUN1:4;
then dom(g.x) in the set of all dom m where m is Element of Y2;
then
A6: dom(g.x) c= DOMS(Y2) by ZFMISC_1:74;
x in dom f by A1,A2,XBOOLE_0:def 4;
then f.x in Y1 by PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y1;
then
A7: dom(f.x) c= DOMS(Y1) by ZFMISC_1:74;
dom y = dom(f.x) /\ dom(g.x) by A3,A4,VALUED_1:16;
then y is PartFunc of DOMS(Y1)/\DOMS(Y2),REAL by A7,A6,A5,RELSET_1:4
,XBOOLE_1:27;
hence thesis by Def12;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
definition
let X1, X2 be set;
let Y1, Y2 be rational-functions-membered set;
let f be PartFunc of X1,Y1;
let g be PartFunc of X2,Y2;
redefine func f<//>g -> PartFunc of X1 /\ X2, Q_PFuncs(DOMS(Y1)/\DOMS(Y2)); :: redefines <//> (VALUED_2, definition)
coherence
proof
set h = f<//>g;
A1: dom h = dom f /\ dom g by Def48;
rng h c= Q_PFuncs(DOMS(Y1)/\DOMS(Y2))
proof
let y be object;
assume y in rng h;
then consider x being object such that
A2: x in dom h and
A3: h.x = y by FUNCT_1:def 3;
reconsider y as Function by A3;
A4: h.x = f.x /" g.x by A2,Def48;
A5: rng y c= RAT
by A3,A4,RAT_1:def 2;
x in dom g by A1,A2,XBOOLE_0:def 4;
then g.x in Y2 by PARTFUN1:4;
then dom(g.x) in the set of all dom m where m is Element of Y2;
then
A6: dom(g.x) c= DOMS(Y2) by ZFMISC_1:74;
x in dom f by A1,A2,XBOOLE_0:def 4;
then f.x in Y1 by PARTFUN1:4;
then dom(f.x) in the set of all dom m where m is Element of Y1;
then
A7: dom(f.x) c= DOMS(Y1) by ZFMISC_1:74;
dom y = dom(f.x) /\ dom(g.x) by A3,A4,VALUED_1:16;
then y is PartFunc of DOMS(Y1)/\DOMS(Y2),RAT by A7,A6,A5,RELSET_1:4
,XBOOLE_1:27;
hence thesis by Def14;
end;
hence thesis by A1,RELSET_1:4;
end;
end;
theorem
(<->f1) <//> f2 = <-> (f1<//>f2)
proof
set f3 = f1<//>f2, f4 = <->f1;
A1: dom f3 = dom f1 /\ dom f2 & dom f4 = dom f1 by Def33,Def48;
dom(f4<//>f2) = dom f4 /\ dom f2 by Def48;
hence
A2: dom(f4<//>f2) = dom(<->f3) by A1,Def33;
let x be object;
assume
A3: x in dom(f4<//>f2);
then
A4: x in dom f3 by A1,Def48;
then
A5: x in dom <->f1 by A1,XBOOLE_0:def 4;
thus (f4<//>f2).x = f4.x /" f2.x by A3,Def48
.= (-(f1.x)) /" f2.x by A5,Def33
.= -(f1.x) /" f2.x by Th25
.= -f3.x by A4,Def48
.= (<->f3).x by A2,A3,Def33;
end;
theorem
f1 <//> <->f2 = <-> (f1<//>f2)
proof
set f3 = f1<//>f2, f4 = <->f2;
A1: dom f3 = dom f1 /\ dom f2 & dom f4 = dom f2 by Def33,Def48;
dom(f1<//>f4) = dom f1 /\ dom f4 by Def48;
hence
A2: dom(f1<//>f4) = dom(<->f3) by A1,Def33;
let x be object;
assume
A3: x in dom(f1<//>f4);
then
A4: x in dom f3 by A1,Def48;
then
A5: x in dom <->f2 by A1,XBOOLE_0:def 4;
thus (f1<//>f4).x = f1.x /" f4.x by A3,Def48
.= f1.x /" -f2.x by A5,Def33
.= -(f1.x) /" f2.x by Th27
.= -f3.x by A4,Def48
.= (<->f3).x by A2,A3,Def33;
end;
theorem
f <##> f1 <//> f2 = f <##> (f1<//>f2)
proof
set f3 = f<##>f1, f4 = f1<//>f2;
A1: dom(f3<//>f2) = dom f3 /\ dom f2 by Def48;
A2: dom(f<##>f4) = dom f /\ dom f4 by Def47;
dom f3 = dom f /\ dom f1 & dom f4 = dom f1 /\ dom f2 by Def47,Def48;
hence
A3: dom(f3<//>f2) = dom(f<##>f4) by A1,A2,XBOOLE_1:16;
let x be object;
assume
A4: x in dom(f3<//>f2);
then
A5: x in dom f4 by A2,A3,XBOOLE_0:def 4;
A6: x in dom f3 by A1,A4,XBOOLE_0:def 4;
thus (f3<//>f2).x = f3.x /" f2.x by A4,Def48
.= f.x (#) f1.x /" f2.x by A6,Def47
.= f.x (#) (f1.x /" f2.x) by Th19
.= f.x (#) f4.x by A5,Def48
.= (f<##>f4).x by A3,A4,Def47;
end;
theorem
f <//> f1 <##> f2 = f <##> f2 <//> f1
proof
set f3 = f<//>f1, f4 = f<##>f2;
A1: dom(f3<##>f2) = dom f3 /\ dom f2 by Def47;
A2: dom(f4<//>f1) = dom f4 /\ dom f1 by Def48;
dom f3 = dom f /\ dom f1 & dom f4 = dom f /\ dom f2 by Def47,Def48;
hence
A3: dom(f3<##>f2) = dom(f4<//>f1) by A1,A2,XBOOLE_1:16;
let x be object;
assume
A4: x in dom(f3<##>f2);
then
A5: x in dom f4 by A2,A3,XBOOLE_0:def 4;
A6: x in dom f3 by A1,A4,XBOOLE_0:def 4;
thus (f3<##>f2).x = f3.x (#) f2.x by A4,Def47
.= f.x /" f1.x (#) f2.x by A6,Def48
.= f.x (#) f2.x /" f1.x by Th20
.= f4.x /" f1.x by A5,Def47
.= (f4<//>f1).x by A3,A4,Def48;
end;
theorem
f <//> f1 <//> f2 = f <//> (f1 <##> f2)
proof
set f3 = f<//>f1, f4 = f1<##>f2;
A1: dom(f3<//>f2) = dom f3 /\ dom f2 by Def48;
A2: dom(f<//>f4) = dom f /\ dom f4 by Def48;
dom f3 = dom f /\ dom f1 & dom f4 = dom f1 /\ dom f2 by Def47,Def48;
hence
A3: dom(f3<//>f2) = dom(f<//>f4) by A1,A2,XBOOLE_1:16;
let x be object;
assume
A4: x in dom(f3<//>f2);
then
A5: x in dom f4 by A2,A3,XBOOLE_0:def 4;
A6: x in dom f3 by A1,A4,XBOOLE_0:def 4;
thus (f3<//>f2).x = f3.x /" f2.x by A4,Def48
.= f.x /" f1.x /" f2.x by A6,Def48
.= f.x /" (f1.x (#) f2.x) by Th21
.= f.x /" f4.x by A5,Def47
.= (f<//>f4).x by A3,A4,Def48;
end;
theorem
(f1<++>f2) <//> f = (f1<//>f) <++> (f2<//>f)
proof
set f3 = f1<//>f, f4 = f2<//>f, f5 = f1<++>f2;
A1: dom(f5<//>f) = dom f /\ dom f5 by Def48;
A2: dom f5 = dom f1 /\ dom f2 by Def45;
A3: dom(f3<++>f4) = dom f3 /\ dom f4 by Def45;
dom f3 = dom f1 /\ dom f & dom f4 = dom f2 /\ dom f by Def48;
hence
A4: dom(f5<//>f) = dom(f3<++>f4) by A1,A3,A2,Lm1;
let x be object;
assume
A5: x in dom(f5<//>f);
then
A6: x in dom f3 by A3,A4,XBOOLE_0:def 4;
A7: x in dom f5 by A1,A5,XBOOLE_0:def 4;
A8: x in dom f4 by A3,A4,A5,XBOOLE_0:def 4;
thus (f5<//>f).x = f5.x /" f.x by A5,Def48
.= (f1.x+f2.x) /" f.x by A7,Def45
.= f1.x /" f.x + f2.x /" f.x by RFUNCT_1:10
.= f3.x + f2.x /" f.x by A6,Def48
.= f3.x + f4.x by A8,Def48
.= (f3<++>f4).x by A4,A5,Def45;
end;
theorem
(f1<-->f2) <//> f = (f1<//>f) <--> (f2<//>f)
proof
set f3 = f1<//>f, f4 = f2<//>f, f5 = f1<-->f2;
A1: dom(f5<//>f) = dom f /\ dom f5 by Def48;
A2: dom f5 = dom f1 /\ dom f2 by Def46;
A3: dom(f3<-->f4) = dom f3 /\ dom f4 by Def46;
dom f3 = dom f1 /\ dom f & dom f4 = dom f2 /\ dom f by Def48;
hence
A4: dom(f5<//>f) = dom(f3<-->f4) by A1,A3,A2,Lm1;
let x be object;
assume
A5: x in dom(f5<//>f);
then
A6: x in dom f3 by A3,A4,XBOOLE_0:def 4;
A7: x in dom f5 by A1,A5,XBOOLE_0:def 4;
A8: x in dom f4 by A3,A4,A5,XBOOLE_0:def 4;
thus (f5<//>f).x = f5.x /" f.x by A5,Def48
.= (f1.x-f2.x) /" f.x by A7,Def46
.= f1.x /" f.x - f2.x /" f.x by RFUNCT_1:14
.= f3.x - f2.x /" f.x by A6,Def48
.= f3.x - f4.x by A8,Def48
.= (f3<-->f4).x by A4,A5,Def46;
end;