:: Basic Functions and Operations on Functions
:: by Czes{\l}aw Byli\'nski
::
:: Received May 9, 1989
:: Copyright (c) 1990-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 XBOOLE_0, TARSKI, RELAT_1, FUNCT_1, ZFMISC_1, SUBSET_1, MCART_1,
PARTFUN1, FUNCT_2, FUNCT_3, BINOP_1, CARD_1, ORDINAL1;
notations TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, ORDINAL1, SUBSET_1, MCART_1,
RELSET_1, FUNCT_1, FUNCT_2, BINOP_1;
constructors BINOP_1, RELSET_1, ORDINAL1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1;
requirements SUBSET, BOOLE, NUMERALS;
definitions TARSKI, FUNCT_1, BINOP_1, FUNCT_2;
equalities BINOP_1, ORDINAL1;
expansions TARSKI, FUNCT_1, FUNCT_2;
theorems TARSKI, ZFMISC_1, FUNCT_1, FUNCT_2, RELAT_1, RELSET_1, XBOOLE_0,
XBOOLE_1, DOMAIN_1, XTUPLE_0, SUBSET_1, BINOP_1;
schemes FUNCT_1;
begin
reserve p,q,x,x1,x2,y,y1,y2,z,z1,z2 for set;
reserve A,B,V,X,X1,X2,Y,Y1,Y2,Z for set;
reserve C,C1,C2,D,D1,D2 for non empty set;
:: Additional propositions about functions
theorem Th1:
A c= Y implies id A = (id Y)|A
proof
assume A c= Y;
hence id A = id(Y /\ A) by XBOOLE_1:28
.= (id Y)*(id A) by FUNCT_1:22
.= (id Y)|A by RELAT_1:65;
end;
theorem Th2:
for f,g being Function st X c= dom(g*f) holds f.:X c= dom g
proof
let f,g be Function such that
A1: X c= dom(g*f);
let y be object;
assume y in f.:X;
then ex x being object st x in dom f & x in X & y = f.x by FUNCT_1:def 6;
hence thesis by A1,FUNCT_1:11;
end;
theorem Th3:
for f,g being Function st X c= dom f & f.:X c= dom g holds X c= dom(g*f)
proof
let f,g be Function such that
A1: X c= dom f and
A2: f.:X c= dom g;
let x be object;
assume
A3: x in X;
then f.x in f.:X by A1,FUNCT_1:def 6;
hence thesis by A1,A2,A3,FUNCT_1:11;
end;
theorem Th4:
for f,g being Function st Y c= rng(g*f) & g is one-to-one holds g "Y c= rng f
proof
let f,g be Function such that
A1: Y c= rng(g*f) and
A2: g is one-to-one;
let y be object;
assume
A3: y in g"Y;
then
A4: y in dom g by FUNCT_1:def 7;
g.y in Y by A3,FUNCT_1:def 7;
then consider x being object such that
A5: x in dom(g*f) and
A6: g.y = (g*f).x by A1,FUNCT_1:def 3;
A7: x in dom f by A5,FUNCT_1:11;
g.y = g.(f.x) & f.x in dom g by A5,A6,FUNCT_1:11,12;
then y = f.x by A2,A4;
hence thesis by A7,FUNCT_1:def 3;
end;
theorem Th5:
for f,g being Function st Y c= rng g & g"Y c= rng f holds Y c= rng(g*f)
proof
let f,g be Function such that
A1: Y c= rng g and
A2: g"Y c= rng f;
let y be object;
assume
A3: y in Y;
then consider z being object such that
A4: z in dom g & y = g.z by A1,FUNCT_1:def 3;
z in g"Y by A3,A4,FUNCT_1:def 7;
then consider x being object such that
A5: x in dom f & z = f.x by A2,FUNCT_1:def 3;
x in dom(g*f) & (g*f).x = y by A4,A5,FUNCT_1:11,13;
hence thesis by FUNCT_1:def 3;
end;
scheme
FuncEx3{A()->set,B()-> set,P[object,object,object]}:
ex f being Function st dom f = [:A(),B():] &
for x,y being object st x in A() & y in B() holds P[x,y,f.(x,y)]
provided
A1: for x,y,z1,z2 being object
st x in A() & y in B() & P[x,y,z1] & P[x,y,z2] holds z1 = z2 and
A2: for x,y being object st x in A() & y in B()
ex z being object st P[x,y,z];
defpred R[object,object] means
for x,y being object st $1=[x,y] holds P[x,y,$2];
set D = [:A(), B():];
A3: for p being object st p in D ex z being object st R[p,z]
proof
let p be object;
assume p in D;
then consider x1,y1 being object such that
A4: x1 in A() & y1 in B() and
A5: p = [x1,y1] by ZFMISC_1:def 2;
consider z being object such that
A6: P[x1,y1,z] by A2,A4;
take z;
let x,y be object;
assume
A7: p=[x,y];
then x=x1 by A5,XTUPLE_0:1;
hence thesis by A5,A6,A7,XTUPLE_0:1;
end;
A8: for p,y1,y2 being object st p in D & R[p,y1] & R[p,y2] holds y1 = y2
proof
let p,y1,y2 be object;
assume p in D;
then consider x1,x2 being object such that
A9: x1 in A() & x2 in B() and
A10: p = [x1,x2] by ZFMISC_1:def 2;
assume
( for x,y being object st p=[x,y] holds P[x,y,y1])&
for x,y being object st p=[x,y] holds P[ x,y,y2];
then ( P[x1,x2,y1])& P[x1,x2,y2] by A10;
hence thesis by A1,A9;
end;
consider f being Function such that
A11: dom f = D and
A12: for p being object st p in D holds R[p,f.p] from FUNCT_1:sch 2(A8,A3);
take f;
thus dom f = [:A(),B():] by A11;
let x,y be object;
assume x in A() & y in B();
then [x,y] in [:A(),B():] by ZFMISC_1:def 2;
hence thesis by A12;
end;
scheme
Lambda3{A()->set,B()->set,F(object,object)->object}:
ex f being Function st dom f = [:A(),B():] &
for x,y being object st x in A() & y in B() holds f.(x,y) = F(x,y);
defpred P[object,object,object] means $3 = F($1,$2);
A1: for x,y being object st x in A() & y in B()
ex z being object st P[x,y,z];
A2: for x,y,z1,z2 being object st x in A() & y in B() & P[x,y,z1] & P[x,y,z2]
holds z1=z2;
ex f being Function st dom f = [:A(),B():] &
for x,y being object st x in A() & y in B()
holds P[x,y,f.(x,y)] from FuncEx3(A2,A1);
hence thesis;
end;
theorem Th6:
for f,g being Function st dom f = [:X,Y:] & dom g = [:X,Y:] &
for x,y being object st x in X & y in Y holds f.(x,y) = g.(x,y)
holds f = g
proof
let f,g be Function such that
A1: dom f = [:X,Y:] & dom g = [:X,Y:] and
A2: for x,y being object st x in X & y in Y holds f.(x,y) = g.(x,y);
for p being object holds p in [:X,Y:] implies f.p = g.p
proof let p be object;
assume p in [:X,Y:];
then consider x,y being object such that
A3: x in X & y in Y and
A4: p = [x,y] by ZFMISC_1:def 2;
f.(x,y) = g.(x,y) by A2,A3;
hence thesis by A4;
end;
hence thesis by A1;
end;
:: Function indicated by the image under a function
definition
let f be Function;
func .:f -> Function means
:Def1:
dom it = bool dom f & for X st X c= dom f holds it.X = f.:X;
existence
proof
defpred P[object,object] means for X st $1=X holds $2 = f.:X;
A1: for x being object st x in bool dom f ex y being object st P[x,y]
proof
let x being object such that
x in bool dom f;
reconsider x as set by TARSKI:1;
take f.:x;
thus thesis;
end;
A2: for x,y1,y2 being object st x in bool dom f & P[x,y1] & P[x,y2]
holds y1=y2
proof
let x,y1,y2 be object such that
x in bool dom f and
A3: for X st x=X holds y1 = f.:X and
A4: for X st x=X holds y2 = f.:X;
reconsider x as set by TARSKI:1;
thus y1 = f.:x by A3
.= y2 by A4;
end;
consider g being Function such that
A5: dom g = bool dom f &
for x being object st x in bool dom f holds P[x,g.x] from
FUNCT_1:sch 2(A2,A1);
take g;
thus thesis by A5;
end;
uniqueness
proof
let f1,f2 be Function such that
A6: dom f1 = bool dom f and
A7: for X st X c= dom f holds f1.X = f.:X and
A8: dom f2 = bool dom f and
A9: for X st X c= dom f holds f2.X = f.:X;
for x being object st x in bool dom f holds f1.x = f2.x
proof
let x be object;
assume
A10: x in bool dom f;
reconsider x as set by TARSKI:1;
f1.x = f.:x by A7,A10;
hence thesis by A9,A10;
end;
hence thesis by A6,A8;
end;
end;
theorem Th7:
for f being Function st X in dom(.:f) holds (.:f).X = f.:X
proof
let f be Function;
assume X in dom(.:f);
then X in bool dom f by Def1;
hence thesis by Def1;
end;
theorem
for f being Function holds (.:f).{} = {}
proof
let f be Function;
{} c= dom f;
then (.:f).{} = f.:{} by Def1;
hence thesis;
end;
theorem Th9:
for f being Function holds rng(.:f) c= bool rng f
proof
let f be Function;
let y be object;
reconsider yy=y as set by TARSKI:1;
assume y in rng(.:f);
then consider x being object such that
A1: x in dom(.:f) & y = (.:f).x by FUNCT_1:def 3;
reconsider x as set by TARSKI:1;
y = f.:x by A1,Th7;
then yy c= rng f by RELAT_1:111;
hence thesis;
end;
theorem
for f being Function holds (.:f).:A c= bool rng f
proof
let f be Function;
(.:f).:A c= rng(.:f) & rng(.:f) c= bool rng f by Th9,RELAT_1:111;
hence thesis;
end;
theorem Th11:
for f being Function holds (.:f)"B c= bool dom f
proof
let f be Function;
dom(.:f) = bool dom f by Def1;
hence thesis by RELAT_1:132;
end;
theorem
for f being Function of X,D holds (.:f)"B c= bool X
proof
let f be Function of X,D;
dom f = X by FUNCT_2:def 1;
hence thesis by Th11;
end;
theorem Th13:
for f being Function holds union((.:f).:A) c= f.:(union A)
proof
let f be Function;
let y be object;
assume y in union((.:f).:A);
then consider Z such that
A1: y in Z and
A2: Z in (.:f).:A by TARSKI:def 4;
consider X being object such that
A3: X in dom(.:f) and
A4: X in A and
A5: Z = (.:f).X by A2,FUNCT_1:def 6;
reconsider X as set by TARSKI:1;
y in f.:X by A1,A3,A5,Th7;
then consider x being object such that
A6: x in dom f and
A7: x in X and
A8: y = f.x by FUNCT_1:def 6;
x in union A by A4,A7,TARSKI:def 4;
hence thesis by A6,A8,FUNCT_1:def 6;
end;
theorem Th14:
for f being Function st A c= bool dom f holds f.:(union A) = union((.:f).:A)
proof
let f be Function such that
A1: A c= bool dom f;
A2: f.:(union A) c= union((.:f).:A)
proof
let y be object;
assume y in f.:(union A);
then consider x being object such that
x in dom f and
A3: x in union A and
A4: y = f.x by FUNCT_1:def 6;
consider X such that
A5: x in X and
A6: X in A by A3,TARSKI:def 4;
X in bool dom f by A1,A6;
then X in dom(.:f) by Def1;
then
A7: (.:f).X in (.:f).:A by A6,FUNCT_1:def 6;
y in f.:X by A1,A4,A5,A6,FUNCT_1:def 6;
then y in (.:f).X by A1,A6,Def1;
hence thesis by A7,TARSKI:def 4;
end;
union((.:f).:A) c= f.:(union A) by Th13;
hence thesis by A2,XBOOLE_0:def 10;
end;
theorem
for f being Function of X,D st A c= bool X holds f.:(union A) = union(
(.:f).:A)
proof
let f be Function of X,D;
dom f = X by FUNCT_2:def 1;
hence thesis by Th14;
end;
theorem Th16:
for f being Function holds union((.:f)"B) c= f"(union B)
proof
let f be Function;
let x be object;
assume x in union((.:f)"B);
then consider X such that
A1: x in X and
A2: X in (.:f)"B by TARSKI:def 4;
dom(.:f) = bool dom f by Def1;
then
A3: X in bool dom f by A2,FUNCT_1:def 7;
then
A4: f.x in f.:X by A1,FUNCT_1:def 6;
(.:f).X in B by A2,FUNCT_1:def 7;
then f.:X in B by A3,Def1;
then f.x in union B by A4,TARSKI:def 4;
hence thesis by A1,A3,FUNCT_1:def 7;
end;
theorem
for f being Function st B c= bool rng f holds f"(union B) = union((.:f
) " B )
proof
let f be Function such that
A1: B c= bool rng f;
A2: f"(union B) c= union((.:f)"B)
proof
let x be object;
assume
A3: x in f"(union B);
then f.x in union B by FUNCT_1:def 7;
then consider Y such that
A4: f.x in Y and
A5: Y in B by TARSKI:def 4;
A6: f"Y c= dom f by RELAT_1:132;
then f"Y in bool dom f;
then
A7: f"Y in dom(.:f) by Def1;
f.:(f"Y) = Y by A1,A5,FUNCT_1:77;
then (.:f).(f"Y) in B by A5,A6,Def1;
then
A8: f"Y in (.:f)"B by A7,FUNCT_1:def 7;
x in dom f by A3,FUNCT_1:def 7;
then x in f"Y by A4,FUNCT_1:def 7;
hence thesis by A8,TARSKI:def 4;
end;
union((.:f)"B) c= f"(union B) by Th16;
hence thesis by A2,XBOOLE_0:def 10;
end;
theorem
for f,g being Function holds .:(g*f) = .:g*.:f
proof
let f,g be Function;
for x being object holds x in dom .:(g*f) iff x in dom(.:g*.:f)
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
thus x in dom .:(g*f) implies x in dom(.:g*.:f)
proof
assume x in dom .:(g*f);
then
A1: x in bool dom(g*f) by Def1;
dom(g*f) c= dom f by RELAT_1:25;
then
A2: xx c= dom f by A1;
then x in bool dom f;
then
A3: x in dom .:f by Def1;
f.:xx c= dom g by A1,Th2;
then f.:xx in bool dom g;
then f.:xx in dom .:g by Def1;
then .:f.x in dom .:g by A2,Def1;
hence thesis by A3,FUNCT_1:11;
end;
assume
A4: x in dom(.:g*.:f);
then
A5: x in dom .:f by FUNCT_1:11;
.:f.x in dom .:g by A4,FUNCT_1:11;
then f.:xx in dom .:g by A5,Th7;
then
A6: f.:xx in bool dom g by Def1;
x in bool dom f by A5,Def1;
then xx c= dom(g*f) by A6,Th3;
then x in bool dom(g*f);
hence thesis by Def1;
end;
then
A7: dom .:(g*f) = dom(.:g*.:f) by TARSKI:2;
for x being object st x in dom .:(g*f) holds (.:(g*f)).x = (.:g*.:f).x
proof
let x be object;
assume
A8: x in dom .:(g*f);
then
A9: x in bool dom(g*f) by Def1;
reconsider xx=x as set by TARSKI:1;
A10: f.:xx c= dom g by Th2,A9;
dom(g*f) c= dom f by RELAT_1:25;
then
A11: xx c= dom f by A9;
then x in bool dom f;
then
A12: x in dom .:f by Def1;
thus (.:(g*f)).x = (g*f).:xx by A8,Th7
.= g.:(f.:xx) by RELAT_1:126
.= .:g.(f.:xx) by A10,Def1
.= .:g.(.:f.x) by A11,Def1
.= (.:g*.:f).x by A12,FUNCT_1:13;
end;
hence thesis by A7;
end;
theorem Th19:
for f being Function holds .:f is Function of bool dom f, bool rng f
proof
let f be Function;
dom .:f = bool dom f & rng.:f c= bool rng f by Def1,Th9;
hence thesis by FUNCT_2:def 1,RELSET_1:4;
end;
theorem Th20:
for f being Function of X,Y st Y = {} implies X = {} holds .:f
is Function of bool X, bool Y
proof
let f be Function of X,Y;
assume Y = {} implies X = {};
then
A1: dom f = X by FUNCT_2:def 1;
rng f c= Y by RELAT_1:def 19;
then
A2: bool rng f c= bool Y by ZFMISC_1:67;
A3: .:f is Function of bool dom f, bool rng f by Th19;
then rng.:f c= bool rng f by RELAT_1:def 19;
then
A4: rng.:f c= bool Y by A2;
dom.:f = bool dom f by A3,FUNCT_2:def 1;
hence thesis by A1,A4,FUNCT_2:def 1,RELSET_1:4;
end;
definition
let X,D;
let f be Function of X,D;
redefine func .:f -> Function of bool X, bool D; :: redefines .: (FUNCT_3, definition)
coherence by Th20;
end;
:: Function indicated by the inverse image under a function
definition
let f be Function;
func "f -> Function means
:Def2:
dom it = bool rng f & for Y st Y c= rng f holds it.Y = f"Y;
existence
proof
defpred P[object,object] means for Y st $1=Y holds $2 = f"Y;
A1: for y being object st y in bool rng f ex x being object st P[y,x]
proof
let y being object such that
y in bool rng f;
reconsider y as set by TARSKI:1;
take f"y;
thus thesis;
end;
A2: for y,x1,x2 being object
st y in bool rng f & P[y,x1] & P[y,x2] holds x1=x2
proof
let y,x1,x2 being object such that
y in bool rng f and
A3: for Y st y=Y holds x1 = f"Y and
A4: for Y st y=Y holds x2 = f"Y;
reconsider y as set by TARSKI:1;
thus x1 = f"y by A3
.= x2 by A4;
end;
consider g being Function such that
A5: dom g = bool rng f &
for y being object st y in bool rng f holds P[y,g.y] from
FUNCT_1:sch 2(A2,A1);
take g;
thus thesis by A5;
end;
uniqueness
proof
let f1,f2 be Function such that
A6: dom f1 = bool rng f and
A7: for Y st Y c= rng f holds f1.Y = f"Y and
A8: dom f2 = bool rng f and
A9: for Y st Y c= rng f holds f2.Y = f"Y;
for y being object st y in bool rng f holds f1.y = f2.y
proof
let y be object;
assume
A10: y in bool rng f;
reconsider y as set by TARSKI:1;
f1.y = f"y by A7,A10;
hence thesis by A9,A10;
end;
hence thesis by A6,A8;
end;
end;
theorem Th21:
for f being Function st Y in dom("f) holds ("f).Y = f"Y
proof
let f be Function;
dom("f) = bool rng f by Def2;
hence thesis by Def2;
end;
theorem Th22:
for f being Function holds rng("f) c= bool dom f
proof
let f be Function;
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in rng("f);
then consider y being object such that
A1: y in dom("f) & x = "f.y by FUNCT_1:def 3;
reconsider y as set by TARSKI:1;
x = f"y by A1,Th21;
then xx c= dom f by RELAT_1:132;
hence thesis;
end;
theorem
for f being Function holds ("f).:B c= bool dom f
proof
let f be Function;
rng("f) c= bool dom f & ("f).:B c= rng("f) by Th22,RELAT_1:111;
hence thesis;
end;
theorem
for f being Function holds ("f)"A c= bool rng f
proof
let f be Function;
dom("f) = bool rng f by Def2;
hence thesis by RELAT_1:132;
end;
theorem Th25:
for f being Function holds union(("f).:B) c= f"(union B)
proof
let f be Function;
let x be object;
assume x in union(("f).:B);
then consider X such that
A1: x in X and
A2: X in ("f).:B by TARSKI:def 4;
consider Y being object such that
A3: Y in dom("f) and
A4: Y in B and
A5: X = "f.Y by A2,FUNCT_1:def 6;
reconsider Y as set by TARSKI:1;
A6: ("f).Y = f"Y by A3,Th21;
Y in bool rng f by A3,Def2;
then
A7: f.:X in B by A4,A5,A6,FUNCT_1:77;
A8: f"Y c= dom f by RELAT_1:132;
then f.x in f.:X by A1,A5,A6,FUNCT_1:def 6;
then f.x in union B by A7,TARSKI:def 4;
hence thesis by A1,A5,A6,A8,FUNCT_1:def 7;
end;
theorem
for f being Function st B c= bool rng f holds union(("f).:B) = f"( union B )
proof
let f be Function such that
A1: B c= bool rng f;
A2: f"(union B) c= union(("f).:B)
proof
let x be object;
assume
A3: x in f"(union B);
then f.x in union B by FUNCT_1:def 7;
then consider Y such that
A4: f.x in Y and
A5: Y in B by TARSKI:def 4;
x in dom f by A3,FUNCT_1:def 7;
then
A6: x in f"Y by A4,FUNCT_1:def 7;
Y in bool rng f by A1,A5;
then
A7: Y in dom("f) by Def2;
("f).Y = f"Y by A1,A5,Def2;
then f"Y in ("f).:B by A5,A7,FUNCT_1:def 6;
hence thesis by A6,TARSKI:def 4;
end;
union(("f).:B) c= f"(union B) by Th25;
hence thesis by A2,XBOOLE_0:def 10;
end;
theorem Th27:
for f being Function holds union(("f)"A) c= f.:(union A)
proof
let f be Function;
let y be object;
assume y in union(("f)"A);
then consider Y such that
A1: y in Y and
A2: Y in ("f)"A by TARSKI:def 4;
dom("f) = bool rng f by Def2;
then
A3: Y in bool rng f by A2,FUNCT_1:def 7;
then consider x being object such that
A4: x in dom f & y = f.x by A1,FUNCT_1:def 3;
"f.Y in A by A2,FUNCT_1:def 7;
then
A5: f"Y in A by A3,Def2;
x in f"Y by A1,A4,FUNCT_1:def 7;
then x in union A by A5,TARSKI:def 4;
hence thesis by A4,FUNCT_1:def 6;
end;
theorem
for f being Function st A c= bool dom f & f is one-to-one holds union(
("f)"A) = f.:(union A)
proof
let f be Function such that
A1: A c= bool dom f and
A2: f is one-to-one;
A3: f.:(union A) c= union(("f)"A)
proof
let y be object;
assume y in f.:(union A);
then consider x being object such that
A4: x in dom f and
A5: x in union A and
A6: y = f.x by FUNCT_1:def 6;
consider X such that
A7: x in X and
A8: X in A by A5,TARSKI:def 4;
A9: f"(f.:X) c= X by A2,FUNCT_1:82;
A10: f.:X c= rng f by RELAT_1:111;
then f.:X in bool rng f;
then
A11: (f.:X) in dom("f) by Def2;
X c= f"(f.:X) by A1,A8,FUNCT_1:76;
then f"(f.:X) = X by A9,XBOOLE_0:def 10;
then ("f).(f.:X) in A by A8,A10,Def2;
then
A12: (f.:X) in ("f)"A by A11,FUNCT_1:def 7;
y in (f.:X) by A4,A6,A7,FUNCT_1:def 6;
hence thesis by A12,TARSKI:def 4;
end;
union(("f)"A) c= f.:(union A) by Th27;
hence thesis by A3,XBOOLE_0:def 10;
end;
theorem Th29:
for f being Function holds ("f).:B c= (.:f)"B
proof
let f be Function;
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in ("f).:B;
then consider Y being object such that
A1: Y in dom ("f) and
A2: Y in B and
A3: x = "f.Y by FUNCT_1:def 6;
reconsider Y as set by TARSKI:1;
A4: "f.Y = f"Y by A1,Th21;
then
A5: xx c= dom f by A3,RELAT_1:132;
then x in bool dom f;
then
A6: x in dom(.:f) by Def1;
Y in bool rng f by A1,Def2;
then f.:xx in B by A2,A3,A4,FUNCT_1:77;
then (.:f).x in B by A5,Def1;
hence thesis by A6,FUNCT_1:def 7;
end;
theorem
for f being Function st f is one-to-one holds ("f).:B = (.:f)"B
proof
let f be Function such that
A1: f is one-to-one;
A2: (.:f)"B c= ("f).:B
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
A3: f.:xx c= rng f by RELAT_1:111;
then f.:xx in bool rng f;
then
A4: f.:xx in dom("f) by Def2;
assume
A5: x in (.:f)"B;
then
A6: x in dom(.:f) by FUNCT_1:def 7;
then x in bool dom f by Def1;
then
A7: xx c= f"(f.:xx) by FUNCT_1:76;
f"(f.:xx) c= xx by A1,FUNCT_1:82;
then x = f"(f.:xx) by A7,XBOOLE_0:def 10;
then
A8: x =("f).(f.:xx) by A3,Def2;
(.:f).x in B by A5,FUNCT_1:def 7;
then f.:xx in B by A6,Th7;
hence thesis by A8,A4,FUNCT_1:def 6;
end;
("f).:B c= (.:f)"B by Th29;
hence thesis by A2,XBOOLE_0:def 10;
end;
theorem Th31:
for f being Function,A be set st A c= bool dom f holds ("f)"A c= (.:f).:A
proof
let f be Function,A be set such that
A1: A c= bool dom f;
let y be object;
reconsider yy=y as set by TARSKI:1;
assume
A2: y in ("f)"A;
then
A3: "f.y in A by FUNCT_1:def 7;
y in dom("f) by A2,FUNCT_1:def 7;
then
A4: y in bool rng f by Def2;
then
A5: f"yy in A by A3,Def2;
then f"yy in bool dom f by A1;
then
A6: f"yy in dom .:f by Def1;
f.:(f"yy) = y by A4,FUNCT_1:77;
then
A7: .:f.(f"yy) = y by A1,A5,Def1;
f"yy in A by A3,A4,Def2;
hence thesis by A7,A6,FUNCT_1:def 6;
end;
theorem Th32:
for f being Function,A be set st f is one-to-one holds (.:f).:A c= ("f)"A
proof
let f be Function,A be set such that
A1: f is one-to-one;
let y be object;
reconsider yy=y as set by TARSKI:1;
assume y in (.:f).:A;
then consider x being object such that
A2: x in dom(.:f) and
A3: x in A and
A4: y = .:f.x by FUNCT_1:def 6;
reconsider x as set by TARSKI:1;
A5: x in bool dom f by A2,Def1;
then
A6: y = f.:x by A4,Def1;
then
A7: x c= f"yy by A5,FUNCT_1:76;
A8: yy c= rng f by A6,RELAT_1:111;
then y in bool rng f;
then
A9: y in dom("f) by Def2;
f"yy c= x by A1,A6,FUNCT_1:82;
then f"yy in A by A3,A7,XBOOLE_0:def 10;
then "f.y in A by A8,Def2;
hence thesis by A9,FUNCT_1:def 7;
end;
theorem
for f being Function,A be set st f is one-to-one & A c= bool dom f
holds ("f)"A = (.:f).:A
proof
let f be Function,A be set;
assume f is one-to-one & A c= bool dom f;
then ("f)"A c= (.:f).:A & (.:f).:A c= ("f)"A by Th31,Th32;
hence thesis by XBOOLE_0:def 10;
end;
theorem
for f,g being Function st g is one-to-one holds "(g*f) = "f*"g
proof
let f,g be Function such that
A1: g is one-to-one;
for y being object holds y in dom "(g*f) iff y in dom("f*"g)
proof
let y be object;
reconsider yy=y as set by TARSKI:1;
thus y in dom "(g*f) implies y in dom("f*"g)
proof
assume y in dom "(g*f);
then
A2: y in bool rng(g*f) by Def2;
rng(g*f) c= rng g by RELAT_1:26;
then
A3: yy c= rng g by A2;
then y in bool rng g;
then
A4: y in dom "g by Def2;
g"yy c= rng f by A1,A2,Th4;
then g"yy in bool rng f;
then g"yy in dom "f by Def2;
then "g.y in dom "f by A3,Def2;
hence thesis by A4,FUNCT_1:11;
end;
assume
A5: y in dom("f*"g);
then
A6: y in dom "g by FUNCT_1:11;
"g.y in dom "f by A5,FUNCT_1:11;
then g"yy in dom "f by A6,Th21;
then
A7: g"yy in bool rng f by Def2;
y in bool rng g by A6,Def2;
then yy c= rng(g*f) by A7,Th5;
then y in bool rng(g*f);
hence thesis by Def2;
end;
then
A8: dom "(g*f) = dom("f*"g) by TARSKI:2;
for y being object st y in dom "(g*f) holds "(g*f).y = ("f*"g).y
proof
let y be object;
assume
A9: y in dom "(g*f);
then
A10: y in bool rng(g*f) by Def2;
reconsider yy=y as set by TARSKI:1;
A11: g"yy c= rng f by A1,Th4,A10;
rng(g*f) c= rng g by RELAT_1:26;
then
A12: yy c= rng g by A10;
then y in bool rng g;
then
A13: y in dom "g by Def2;
thus "(g*f).y = (g*f)"yy by A9,Th21
.= f"(g"yy) by RELAT_1:146
.= "f.(g"yy) by A11,Def2
.= "f.("g.y) by A12,Def2
.= ("f*"g).y by A13,FUNCT_1:13;
end;
hence thesis by A8;
end;
theorem
for f being Function holds "f is Function of bool rng f, bool dom f
proof
let f be Function;
dom"f = bool rng f & rng"f c= bool dom f by Def2,Th22;
hence thesis by FUNCT_2:def 1,RELSET_1:4;
end;
:: Characteristic function
definition
let A,X;
func chi(A,X) -> Function means
:Def3:
dom it = X & for x being object st x in X holds
(x in A implies it.x = 1) & (not x in A implies it.x = 0);
existence
proof
defpred P[object,object] means ($1 in A implies $2 = 1) &
(not $1 in A implies $2 = 0);
A1: for x being object st x in X ex y being object st P[x,y]
proof
let x be object;
assume x in X;
not x in A implies ex y st y = {} & (x in A implies y = 1) & (not x
in A implies y = {});
hence thesis;
end;
A2: for x,y1,y2 being object st x in X & P[x,y1] & P[x,y2] holds y1 = y2;
ex f being Function st dom f = X &
for x being object st x in X holds P[x,f.x] from
FUNCT_1:sch 2(A2,A1);
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function such that
A3: dom f1 = X and
A4: for x being object st x in X holds (x in A implies f1.x = 1) &
(not x in A
implies f1.x = 0) and
A5: dom f2 = X and
A6: for x being object st x in X holds (x in A implies f2.x = 1) &
(not x in A
implies f2.x = 0);
for x being object st x in X holds f1.x=f2.x
proof
let x be object;
assume
A7: x in X;
then
A8: not x in A implies f1.x = 0 & f2.x = 0 by A4,A6;
x in A implies f1.x = 1 & f2.x = 1 by A4,A6,A7;
hence thesis by A8;
end;
hence thesis by A3,A5;
end;
end;
theorem Th36:
for x being object holds chi(A,X).x = 1 implies x in A
proof let x be object;
assume
A1: chi(A,X).x = 1;
A2: 1 = succ 0 .= {0};
per cases;
suppose
x in X;
hence thesis by A1,Def3;
end;
suppose
not x in X;
then not x in dom chi(A,X) by Def3;
hence thesis by A1,FUNCT_1:def 2,A2;
end;
end;
theorem
x in X \ A implies chi(A,X).x = 0
proof
assume
A1: x in X\A;
then not x in A by XBOOLE_0:def 5;
hence thesis by A1,Def3;
end;
theorem
A c= X & B c= X & chi(A,X) = chi(B,X) implies A = B
proof
assume that
A1: A c= X and
A2: B c= X and
A3: chi(A,X) = chi(B,X);
for x being object holds x in A iff x in B
proof let x be object;
thus x in A implies x in B
proof
assume x in A;
then chi(A,X).x = 1 by A1,Def3;
hence thesis by A3,Th36;
end;
assume x in B;
then chi(B,X).x = 1 by A2,Def3;
hence thesis by A3,Th36;
end;
hence thesis by TARSKI:2;
end;
theorem Th39:
rng chi(A,X) c= {0,1}
proof
let y be object;
assume y in rng chi(A,X);
then consider x being object such that
A1: x in dom chi(A,X) and
A2: y = chi(A,X).x by FUNCT_1:def 3;
A3: x in A or not x in A;
x in X by A1,Def3;
then y = {} or y = 1 by A2,A3,Def3;
hence thesis by TARSKI:def 2;
end;
theorem
for f being Function of X,{0,1} holds f = chi(f"{1},X)
proof
let f be Function of X,{0,1};
now
thus
A1: dom f = X by FUNCT_2:def 1;
let x be object such that
A2: x in X;
thus x in f"{1} implies f.x = 1
proof
assume x in f"{1};
then f.x in {1} by FUNCT_1:def 7;
hence thesis by TARSKI:def 1;
end;
assume not x in f"{1};
then not f.x in {1} by A1,A2,FUNCT_1:def 7;
then
A3: rng f c= {{},1} & f.x <> 1 by RELAT_1:def 19,TARSKI:def 1;
f.x in rng f by A1,A2,FUNCT_1:def 3;
hence f.x = {} by A3,TARSKI:def 2;
end;
hence thesis by Def3;
end;
definition
let A,X;
redefine func chi(A,X) -> Function of X,{0,1}; :: redefines chi (FUNCT_3, definition)
coherence
proof
dom chi(A,X) = X & rng chi(A,X) c= {0,1} by Def3,Th39;
hence thesis by FUNCT_2:def 1,RELSET_1:4;
end;
end;
notation
let Y;
let A be Subset of Y;
synonym incl A for id A;
end;
definition
let Y;
let A be Subset of Y;
redefine func incl A -> Function of A,Y; :: redefines incl (FUNCT_3, synonym) → id (RELAT_1, definition)
coherence
proof
A1: rng id A = A & dom id A = A;
thus thesis by A1,FUNCT_2:2;
end;
end;
theorem
for A being Subset of Y holds incl A = (id Y)|A by Th1;
theorem
for A being Subset of Y st x in A holds incl(A).x in Y
proof
let A be Subset of Y such that
A1: x in A;
dom incl A = A & rng incl A = A;
then incl(A).x in A by A1,FUNCT_1:def 3;
hence thesis;
end;
:: Projections
definition
let X,Y;
func pr1(X,Y) -> Function means
:Def4: dom it = [:X,Y:] &
for x,y being object st x in X & y in Y holds it.(x,y) = x;
existence
proof
deffunc F(object,object) = $1;
ex f being Function st dom f = [:X,Y:] &
for x,y being object st x in X & y in Y
holds f.(x,y) = F(x,y) from Lambda3;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function such that
A1: dom f1 = [:X,Y:] and
A2: for x,y being object st x in X & y in Y holds f1.(x,y) = x and
A3: dom f2 = [:X,Y:] and
A4: for x,y being object st x in X & y in Y holds f2.(x,y) = x;
for x,y being object st x in X & y in Y holds f1.(x,y) = f2.(x,y)
proof
let x,y be object;
assume
A5: x in X & y in Y;
then f1.(x,y) = x by A2;
hence thesis by A4,A5;
end;
hence thesis by A1,A3,Th6;
end;
func pr2(X,Y) -> Function means
:Def5: dom it = [:X,Y:] &
for x,y being object st x in X & y in Y holds it.(x,y) = y;
existence
proof
deffunc F(object,object) = $2;
ex f being Function st dom f = [:X,Y:] &
for x,y being object st x in X & y in Y holds f.(x,y) = F(x,y)
from Lambda3;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function such that
A6: dom f1 = [:X,Y:] and
A7: for x,y being object st x in X & y in Y holds f1.(x,y) = y and
A8: dom f2 = [:X,Y:] and
A9: for x,y being object st x in X & y in Y holds f2.(x,y) = y;
for x,y being object st x in X & y in Y holds f1.(x,y) = f2.(x,y)
proof
let x,y be object;
assume
A10: x in X & y in Y;
then f1.(x,y) = y by A7;
hence thesis by A9,A10;
end;
hence thesis by A6,A8,Th6;
end;
end;
theorem Th43:
rng pr1(X,Y) c= X
proof
let x be object;
assume x in rng pr1(X,Y);
then consider p being object such that
A1: p in dom pr1(X,Y) and
A2: x = pr1(X,Y).p by FUNCT_1:def 3;
p in [:X,Y:] by A1,Def4;
then consider x1,y1 being object such that
A3: x1 in X & y1 in Y and
A4: p = [x1,y1] by ZFMISC_1:def 2;
x =pr1(X,Y).(x1,y1) by A2,A4;
hence thesis by A3,Def4;
end;
theorem
Y <> {} implies rng pr1(X,Y) = X
proof
set y = the Element of Y;
assume
A1: Y <> {};
A2: X c= rng pr1(X,Y)
proof
let x be object;
assume
A3: x in X;
then [x,y] in [:X,Y:] by A1,ZFMISC_1:87;
then
A4: [x,y] in dom pr1(X,Y) by Def4;
pr1(X,Y).(x,y) = x by A1,A3,Def4;
hence thesis by A4,FUNCT_1:def 3;
end;
rng pr1(X,Y) c= X by Th43;
hence thesis by A2,XBOOLE_0:def 10;
end;
theorem Th45:
rng pr2(X,Y) c= Y
proof
let y be object;
assume y in rng pr2(X,Y);
then consider p being object such that
A1: p in dom pr2(X,Y) and
A2: y = pr2(X,Y).p by FUNCT_1:def 3;
p in [:X,Y:] by A1,Def5;
then consider x1,y1 being object such that
A3: x1 in X & y1 in Y and
A4: p = [x1,y1] by ZFMISC_1:def 2;
y = pr2(X,Y).(x1,y1) by A2,A4;
hence thesis by A3,Def5;
end;
theorem
X <> {} implies rng pr2(X,Y) = Y
proof
set x = the Element of X;
assume
A1: X <> {};
A2: Y c= rng pr2(X,Y)
proof
let y be object;
assume
A3: y in Y;
then [x,y] in [:X,Y:] by A1,ZFMISC_1:87;
then
A4: [x,y] in dom pr2(X,Y) by Def5;
pr2(X,Y).(x,y) = y by A1,A3,Def5;
hence thesis by A4,FUNCT_1:def 3;
end;
rng pr2(X,Y) c= Y by Th45;
hence thesis by A2,XBOOLE_0:def 10;
end;
definition
let X,Y;
redefine func pr1(X,Y) -> Function of [:X,Y:],X; :: redefines pr1 (FUNCT_3, definition)
coherence
proof
per cases;
suppose
X = {} implies [:X,Y:] = {};
dom pr1(X,Y) = [:X,Y:] & rng pr1(X,Y) c= X by Def4,Th43;
hence thesis by FUNCT_2:2;
end;
suppose
X = {} & [:X,Y:] <> {};
hence thesis by ZFMISC_1:90;
end;
end;
redefine func pr2(X,Y) -> Function of [:X,Y:],Y; :: redefines pr2 (FUNCT_3, definition)
coherence
proof
per cases;
suppose
Y = {} implies [:X,Y:] = {};
dom pr2(X,Y) = [:X,Y:] & rng pr2(X,Y) c= Y by Def5,Th45;
hence thesis by FUNCT_2:2;
end;
suppose
Y = {} & [:X,Y:] <> {};
hence thesis by ZFMISC_1:90;
end;
end;
end;
definition
let X;
func delta(X) -> Function means
:Def6:
dom it = X & for x being object st x in X holds it .x = [x,x];
existence
proof
deffunc F(object) = [$1,$1];
ex f being Function st dom f = X &
for x being object st x in X holds f.x = F(x)
from FUNCT_1:sch 3;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function such that
A1: dom f1 = X and
A2: for x being object st x in X holds f1.x = [x,x] and
A3: dom f2 = X and
A4: for x being object st x in X holds f2.x = [x,x];
for x being object st x in X holds f1.x = f2.x
proof
let x be object;
assume
A5: x in X;
then f1.x = [x,x] by A2;
hence thesis by A4,A5;
end;
hence thesis by A1,A3;
end;
end;
theorem Th47:
rng delta X c= [:X,X:]
proof
let y be object;
assume y in rng delta X;
then consider x being object such that
A1: x in dom delta X and
A2: y = (delta X).x by FUNCT_1:def 3;
A3: x in X by A1,Def6;
then y = [x,x] by A2,Def6;
hence thesis by A3,ZFMISC_1:87;
end;
definition
let X;
redefine func delta(X) -> Function of X,[:X,X:]; :: redefines delta (FUNCT_3, definition)
coherence
proof
dom delta X = X & rng delta X c= [:X,X:] by Def6,Th47;
hence thesis by FUNCT_2:2;
end;
end;
:: Complex functions
definition
let f,g be Function;
func <:f,g:> -> Function means
:Def7:
dom it = dom f /\ dom g &
for x being object st x in dom it holds it.x = [f.x,g.x];
existence
proof
deffunc F(object) = [f.$1,g.$1];
ex fg being Function st dom fg = dom f /\ dom g &
for x being object st x in dom f
/\ dom g holds fg.x = F(x) from FUNCT_1:sch 3;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function such that
A1: dom f1 = dom f /\ dom g and
A2: for x being object st x in dom f1 holds f1.x = [f.x,g.x] and
A3: dom f2 = dom f /\ dom g and
A4: for x being object st x in dom f2 holds f2.x = [f.x,g.x];
for x being object st x in dom f /\ dom g holds f1.x=f2.x
proof
let x be object;
assume
A5: x in dom f /\ dom g;
then f1.x=[f.x,g.x] by A1,A2;
hence thesis by A3,A4,A5;
end;
hence thesis by A1,A3;
end;
end;
registration
let f be empty Function, g be Function;
cluster <:f,g:> -> empty;
coherence
proof
dom f = {};
then dom<:f,g:> = {} /\ dom g by Def7;
hence thesis;
end;
cluster <:g,f:> -> empty;
coherence
proof
dom f = {};
then dom<:g,f:> = {} /\ dom g by Def7;
hence thesis;
end;
end;
theorem Th48:
for f,g being Function st x in dom f /\ dom g holds <:f,g:>.x = [f.x,g.x]
proof
let f,g be Function;
assume x in dom f /\ dom g;
then x in dom <:f,g:> by Def7;
hence thesis by Def7;
end;
theorem Th49:
for f,g being Function st dom f = X & dom g = X & x in X holds
<:f,g:>.x = [f.x,g.x]
proof
let f,g be Function;
assume dom f = X & dom g = X & x in X;
then x in dom f /\ dom g;
then x in dom <:f,g:> by Def7;
hence thesis by Def7;
end;
theorem Th50:
for f,g being Function st dom f = X & dom g = X holds dom <:f,g :> = X
proof
let f,g be Function;
dom <:f,g:> = dom f /\ dom g by Def7;
hence thesis;
end;
theorem Th51:
for f,g being Function holds rng <:f,g:> c= [:rng f,rng g:]
proof
let f,g be Function;
let q be object;
assume q in rng <:f,g:>;
then consider x being object such that
A1: x in dom <:f,g:> and
A2: q = <:f,g:>.x by FUNCT_1:def 3;
A3: x in dom f /\ dom g by A1,Def7;
then x in dom f by XBOOLE_0:def 4;
then
A4: f.x in rng f by FUNCT_1:def 3;
x in dom g by A3,XBOOLE_0:def 4;
then
A5: g.x in rng g by FUNCT_1:def 3;
q = [f.x,g.x] by A1,A2,Def7;
hence thesis by A4,A5,ZFMISC_1:87;
end;
theorem Th52:
for f,g being Function st dom f = dom g & rng f c= Y & rng g c=
Z holds pr1(Y,Z)*<:f,g:> = f & pr2(Y,Z)*<:f,g:> = g
proof
let f,g be Function such that
A1: dom f = dom g and
A2: rng f c= Y & rng g c= Z;
A3: [:rng f, rng g:] c= [:Y,Z:] by A2,ZFMISC_1:96;
A4: rng <:f,g:> c= [:rng f, rng g:] by Th51;
dom pr1(Y,Z) = [:Y, Z:] by Def4;
then
A5: dom(pr1(Y,Z)*<:f,g:>) = dom <:f,g:> by A3,A4,RELAT_1:27,XBOOLE_1:1;
then
A6: dom(pr1(Y,Z)*<:f,g:>) = dom f by A1,Th50;
for x being object holds x in dom f implies (pr1(Y,Z)*<:f,g:>).x = f.x
proof let x be object;
assume
A7: x in dom f;
then
A8: f.x in rng f & g.x in rng g by A1,FUNCT_1:def 3;
thus (pr1(Y,Z)*<:f,g:>).x = pr1(Y,Z).(<:f,g:>.x) by A6,A7,FUNCT_1:12
.= pr1(Y,Z).(f.x,g.x) by A5,A6,A7,Def7
.= f.x by A2,A8,Def4;
end;
hence pr1(Y,Z)*<:f,g:> = f by A6;
dom pr2(Y,Z) = [:Y, Z:] by Def5;
then
A9: dom(pr2(Y,Z)*<:f,g:>) = dom <:f,g:> by A3,A4,RELAT_1:27,XBOOLE_1:1;
then
A10: dom(pr2(Y,Z)*<:f,g:>) = dom g by A1,Th50;
for x being object holds x in dom g implies (pr2(Y,Z)*<:f,g:>).x = g.x
proof let x be object;
assume
A11: x in dom g;
then
A12: f.x in rng f & g.x in rng g by A1,FUNCT_1:def 3;
thus (pr2(Y,Z)*<:f,g:>).x = pr2(Y,Z).(<:f,g:>.x) by A10,A11,FUNCT_1:12
.= pr2(Y,Z).(f.x,g.x) by A9,A10,A11,Def7
.= g.x by A2,A12,Def5;
end;
hence thesis by A10;
end;
theorem Th53:
<:pr1(X,Y),pr2(X,Y):> = id [:X,Y:]
proof
dom pr1(X,Y) = [:X,Y:] & dom pr2(X,Y) = [:X,Y:] by Def4,Def5;
then
A1: dom <:pr1(X,Y),pr2(X,Y):> = [:X,Y:] by Th50;
A2: for x,y being object st x in X & y in Y
holds <:pr1(X,Y),pr2(X,Y):>.(x,y) = (id [:X,Y:]).(x,y)
proof
let x,y be object;
assume
A3: x in X & y in Y;
then
A4: [x,y] in [:X,Y:] by ZFMISC_1:87;
hence <:pr1(X,Y),pr2(X,Y):>.(x,y) = [pr1(X,Y).(x,y),pr2(X,Y).(x,y)] by A1
,Def7
.= [x,pr2(X,Y).(x,y)] by A3,Def4
.= [x,y] by A3,Def5
.= (id [:X,Y:]).(x,y) by A4,FUNCT_1:18;
end;
dom id [:X,Y:] = [:X,Y:];
hence thesis by A1,A2,Th6;
end;
theorem Th54:
for f,g,h,k being Function st dom f = dom g & dom k = dom h & <:
f,g:> = <:k,h:> holds f = k & g = h
proof
let f,g,h,k be Function such that
A1: dom f = dom g and
A2: dom k = dom h and
A3: <:f,g:> = <:k,h:>;
A4: dom <:f,g:> = dom f by A1,Th50;
for x being object holds x in dom f implies f.x = k.x
proof let x be object;
assume x in dom f;
then <:f,g:>.x = [f.x,g.x] & <:k,h:>.x = [k.x,h.x] by A3,A4,Def7;
hence thesis by A3,XTUPLE_0:1;
end;
hence f = k by A2,A3,A4,Th50;
A5: dom <:f,g:> = dom g by A1,Th50;
for x being object holds x in dom g implies g.x = h.x
proof let x be object;
assume x in dom g;
then <:f,g:>.x = [f.x,g.x] & <:k,h:>.x = [k.x,h.x] by A3,A5,Def7;
hence thesis by A3,XTUPLE_0:1;
end;
hence thesis by A2,A3,A5,Th50;
end;
theorem
for f,g,h being Function holds <:f*h,g*h:> = <:f,g:>*h
proof
let f,g,h be Function;
for x being object holds x in dom <:f*h,g*h:> iff x in dom(<:f,g:>*h)
proof let x be object;
thus x in dom <:f*h,g*h:> implies x in dom(<:f,g:>*h)
proof
assume x in dom <:f*h,g*h:>;
then
A1: x in dom(f*h) /\ dom(g*h) by Def7;
then
A2: x in dom(f*h) by XBOOLE_0:def 4;
x in dom(g*h) by A1,XBOOLE_0:def 4;
then
A3: h.x in dom g by FUNCT_1:11;
h.x in dom f by A2,FUNCT_1:11;
then h.x in dom f /\ dom g by A3,XBOOLE_0:def 4;
then
A4: h.x in dom <:f,g:> by Def7;
x in dom h by A2,FUNCT_1:11;
hence thesis by A4,FUNCT_1:11;
end;
assume
A5: x in dom(<:f,g:>*h);
then
A6: x in dom h by FUNCT_1:11;
h.x in dom <:f,g:> by A5,FUNCT_1:11;
then
A7: h.x in dom f /\ dom g by Def7;
then h.x in dom g by XBOOLE_0:def 4;
then
A8: x in dom(g*h) by A6,FUNCT_1:11;
h.x in dom f by A7,XBOOLE_0:def 4;
then x in dom(f*h) by A6,FUNCT_1:11;
then x in dom(f*h) /\ dom(g*h) by A8,XBOOLE_0:def 4;
hence thesis by Def7;
end;
then
A9: dom <:f*h,g*h:> = dom(<:f,g:>*h) by TARSKI:2;
for x being object st x in dom <:f*h,g*h:>
holds <:f*h,g*h:>.x = (<:f,g:>*h).x
proof
let x be object;
assume
A10: x in dom <:f*h,g*h:>;
then
A11: x in dom(f*h) /\ dom(g*h) by Def7;
then
A12: x in dom(f*h) by XBOOLE_0:def 4;
then
A13: x in dom h by FUNCT_1:11;
A14: x in dom(g*h) by A11,XBOOLE_0:def 4;
then
A15: h.x in dom g by FUNCT_1:11;
h.x in dom f by A12,FUNCT_1:11;
then
A16: h.x in dom f /\ dom g by A15,XBOOLE_0:def 4;
thus <:f*h,g*h:>.x = [(f*h).x,(g*h).x] by A10,Def7
.= [f.(h.x),(g*h).x] by A12,FUNCT_1:12
.= [f.(h.x),g.(h.x)] by A14,FUNCT_1:12
.= <:f,g:>.(h.x) by A16,Th48
.= (<:f,g:>*h).x by A13,FUNCT_1:13;
end;
hence thesis by A9;
end;
theorem
for f,g being Function holds <:f,g:>.:A c= [:f.:A,g.:A:]
proof
let f,g be Function;
let y be object;
assume y in <:f,g:>.:A;
then consider x being object such that
A1: x in dom <:f,g:> and
A2: x in A and
A3: y = <:f,g:>.x by FUNCT_1:def 6;
A4: x in dom f /\ dom g by A1,Def7;
then x in dom f by XBOOLE_0:def 4;
then
A5: f.x in f.:A by A2,FUNCT_1:def 6;
x in dom g by A4,XBOOLE_0:def 4;
then
A6: g.x in g.: A by A2,FUNCT_1:def 6;
y = [f.x,g.x] by A1,A3,Def7;
hence thesis by A5,A6,ZFMISC_1:def 2;
end;
theorem
for f,g being Function holds <:f,g:>"[:B,C:] = f"B /\ g"C
proof
let f,g be Function;
for x being object holds x in <:f,g:>"[:B,C:] iff x in f"B /\ g"C
proof let x be object;
thus x in <:f,g:>"[:B,C:] implies x in f"B /\ g"C
proof
assume
A1: x in <:f,g:>"[:B,C:];
then <:f,g:>.x in [:B,C:] by FUNCT_1:def 7;
then consider y1,y2 being object such that
A2: y1 in B and
A3: y2 in C and
A4: <:f,g:>.x = [y1,y2] by ZFMISC_1:def 2;
A5: x in dom <:f,g:> by A1,FUNCT_1:def 7;
then
A6: x in dom f /\ dom g by Def7;
then
A7: x in dom g by XBOOLE_0:def 4;
A8: [y1,y2] = [f.x,g.x] by A4,A5,Def7;
then y2 = g.x by XTUPLE_0:1;
then
A9: x in g"C by A3,A7,FUNCT_1:def 7;
A10: x in dom f by A6,XBOOLE_0:def 4;
y1 =f.x by A8,XTUPLE_0:1;
then x in f"B by A2,A10,FUNCT_1:def 7;
hence thesis by A9,XBOOLE_0:def 4;
end;
assume
A11: x in f"B /\ g"C;
then
A12: x in g"C by XBOOLE_0:def 4;
then
A13: x in dom g by FUNCT_1:def 7;
A14: x in f"B by A11,XBOOLE_0:def 4;
then x in dom f by FUNCT_1:def 7;
then
A15: x in dom f /\ dom g by A13,XBOOLE_0:def 4;
then
A16: x in dom <:f,g:> by Def7;
A17: g.x in C by A12,FUNCT_1:def 7;
f.x in B by A14,FUNCT_1:def 7;
then [f.x,g.x] in [:B,C:] by A17,ZFMISC_1:def 2;
then <:f,g:>.x in [:B,C:] by A15,Th48;
hence thesis by A16,FUNCT_1:def 7;
end;
hence thesis by TARSKI:2;
end;
theorem Th58:
for f being Function of X,Y for g being Function of X,Z st (Y =
{} implies X = {}) & (Z = {} implies X = {}) holds <:f,g:> is Function of X,[:Y
,Z:]
proof
let f be Function of X,Y;
let g be Function of X,Z;
assume
A1: ( Y = {} implies X = {})&( Z = {} implies X = {});
per cases;
suppose
[:Y,Z:] = {} implies X = {};
rng f c= Y & rng g c= Z by RELAT_1:def 19;
then
A2: [:rng f,rng g:] c= [:Y,Z:] by ZFMISC_1:96;
dom f = X & dom g = X by A1,FUNCT_2:def 1;
then
A3: dom<:f,g:> = X by Th50;
rng <:f,g:> c= [:rng f,rng g:] by Th51;
then rng<:f,g:> c= [:Y,Z:] by A2;
hence thesis by A3,FUNCT_2:2;
end;
suppose
[:Y,Z:] = {} & X <> {};
hence thesis by A1;
end;
end;
definition
let X,D1,D2;
let f1 be Function of X,D1;
let f2 be Function of X,D2;
redefine func <:f1,f2:> -> Function of X,[:D1,D2:]; :: redefines <: (FUNCT_3, definition)
coherence by Th58;
end;
theorem
for f1 being Function of C,D1 for f2 being Function of C,D2 for c
being Element of C holds <:f1,f2:>.c = [f1.c,f2.c]
proof
let f1 be Function of C,D1;
let f2 be Function of C,D2;
let c be Element of C;
dom f1 = C & dom f2 = C by FUNCT_2:def 1;
hence thesis by Th49;
end;
theorem
for f being Function of X,Y for g being Function of X,Z holds rng <:f,
g:> c= [:Y,Z:]
proof
let f be Function of X,Y;
let g be Function of X,Z;
rng f c= Y & rng g c= Z by RELAT_1:def 19;
then
A1: [:rng f,rng g:] c= [:Y,Z:] by ZFMISC_1:96;
rng <:f,g:> c= [:rng f,rng g:] by Th51;
hence thesis by A1;
end;
theorem Th61:
for f being Function of X,Y for g being Function of X,Z st (Y =
{} implies X = {}) & (Z = {} implies X = {}) holds pr1(Y,Z)*<:f,g:> = f & pr2(Y
,Z)*<:f,g:> = g
proof
let f be Function of X,Y;
let g be Function of X,Z;
assume ( Y = {} implies X = {})&( Z = {} implies X = {});
then
A1: dom f = X & dom g = X by FUNCT_2:def 1;
rng f c= Y & rng g c= Z by RELAT_1:def 19;
hence thesis by A1,Th52;
end;
theorem
for f being Function of X,D1 for g being Function of X,D2 holds pr1(D1
,D2)*<:f,g:> = f & pr2(D1,D2)*<:f,g:> = g by Th61;
theorem
for f1,f2 being Function of X,Y for g1,g2 being Function of X,Z st (Y
= {} implies X = {}) & (Z = {} implies X = {}) & <:f1,g1:> = <:f2,g2:> holds f1
= f2 & g1 = g2
proof
let f1,f2 be Function of X,Y;
let g1,g2 be Function of X,Z;
assume that
A1: Y = {} implies X = {} and
A2: Z = {} implies X = {};
A3: dom g1 = X & dom g2 = X by A2,FUNCT_2:def 1;
dom f1 = X & dom f2 = X by A1,FUNCT_2:def 1;
hence thesis by A3,Th54;
end;
theorem
for f1,f2 being Function of X,D1 for g1,g2 being Function of X,D2 st
<:f1,g1:> = <:f2,g2:> holds f1 = f2 & g1 = g2
proof
let f1,f2 be Function of X,D1;
let g1,g2 be Function of X,D2;
A1: dom g1 = X & dom g2 = X by FUNCT_2:def 1;
dom f1 = X & dom f2 = X by FUNCT_2:def 1;
hence thesis by A1,Th54;
end;
:: Product-functions
definition
let f,g be Function;
func [:f,g:] -> Function means
:Def8:
dom it = [:dom f, dom g:] & for x,y being object st
x in dom f & y in dom g holds it.(x,y) = [f.x,g.y];
existence
proof
deffunc F(object,object) = [f.$1,g.$2];
ex F being Function st dom F = [:dom f,dom g:] &
for x,y being object st x in dom f
& y in dom g holds F.(x,y) = F(x,y) from Lambda3;
hence thesis;
end;
uniqueness
proof
let fg1, fg2 be Function such that
A1: dom fg1 = [:dom f, dom g:] and
A2: for x,y being object st x in dom f & y in dom g
holds fg1.(x,y) = [f.x,g.y] and
A3: dom fg2 = [:dom f, dom g:] and
A4: for x,y being object st x in dom f & y in dom g
holds fg2.(x,y) = [f.x,g.y];
for p being object st p in [:dom f,dom g:] holds fg1.p=fg2.p
proof
let p be object;
assume p in [:dom f,dom g:];
then consider x,y being object such that
A5: x in dom f & y in dom g and
A6: p = [x,y] by ZFMISC_1:def 2;
fg1.(x,y) = [f.x,g.y] & fg2.(x,y) = [f.x,g.y] by A2,A4,A5;
hence thesis by A6;
end;
hence thesis by A1,A3;
end;
end;
theorem Th65:
for f,g being Function, x,y being object st [x,y] in [:dom f,dom g:]
holds [:f,g:].(x,y) = [f.x,g.y]
proof
let f,g be Function, x,y be object;
assume [x,y] in [:dom f,dom g:];
then x in dom f & y in dom g by ZFMISC_1:87;
hence thesis by Def8;
end;
theorem Th66:
for f,g being Function holds [:f,g:] = <:f*pr1(dom f,dom g),g*
pr2(dom f,dom g):>
proof
let f,g be Function;
A1: dom pr1(dom f,dom g) = [:dom f,dom g:] by Def4;
A2: dom pr2(dom f,dom g) = [:dom f,dom g:] by Def5;
rng pr2(dom f,dom g) c= dom g by Th45;
then
A3: dom(g*pr2(dom f,dom g)) = [:dom f,dom g:] by A2,RELAT_1:27;
rng pr1(dom f,dom g) c= dom f by Th43;
then dom(f*pr1(dom f,dom g)) = [:dom f,dom g:] by A1,RELAT_1:27;
then
A4: dom <:f*pr1(dom f,dom g),g*pr2(dom f,dom g):> = [:dom f,dom g:] by A3,Th50;
A5: for x,y being object st x in dom f & y in dom g
holds [:f,g:].(x,y) = <:f*pr1(dom f,dom g),g*pr2(dom f,dom g):>.(x,y)
proof
let x,y be object;
assume
A6: x in dom f & y in dom g;
then
A7: [x,y] in [:dom f,dom g:] by ZFMISC_1:87;
thus [:f,g:].(x,y) = [f.x,g.y] by A6,Def8
.= [f.(pr1(dom f,dom g).(x,y)),g.y] by A6,Def4
.= [f.(pr1(dom f,dom g).(x,y)),g.(pr2(dom f,dom g).(x,y))] by A6,Def5
.= [(f*pr1(dom f,dom g)).(x,y),g.(pr2(dom f,dom g).(x,y))] by A1,A7,
FUNCT_1:13
.= [(f*pr1(dom f,dom g)).(x,y),(g*pr2(dom f,dom g)).(x,y)] by A2,A7,
FUNCT_1:13
.= <:f*pr1(dom f,dom g),g*pr2(dom f,dom g):>.(x,y) by A4,A7,Def7;
end;
dom [:f,g:] = [:dom f,dom g:] by Def8;
hence thesis by A4,A5,Th6;
end;
theorem Th67:
for f,g being Function holds rng [:f,g:] = [:rng f,rng g:]
proof
let f,g be Function;
for q being object holds q in rng [:f,g:] iff q in [:rng f,rng g:]
proof let q be object;
A1: dom [:f,g:]=[:dom f,dom g:] by Def8;
thus q in rng [:f,g:] implies q in [:rng f,rng g:]
proof
assume q in rng [:f,g:];
then consider p being object such that
A2: p in dom [:f,g:] and
A3: q = [:f,g:].p by FUNCT_1:def 3;
p in [:dom f, dom g:] by A2,Def8;
then consider x,y being object such that
A4: x in dom f & y in dom g and
A5: p = [x,y] by ZFMISC_1:def 2;
A6: f.x in rng f & g.y in rng g by A4,FUNCT_1:def 3;
q = [:f,g:].(x,y) by A3,A5
.= [f.x,g.y] by A4,Def8;
hence thesis by A6,ZFMISC_1:87;
end;
assume q in [:rng f,rng g:];
then consider y1,y2 being object such that
A7: y1 in rng f and
A8: y2 in rng g and
A9: q = [y1,y2] by ZFMISC_1:def 2;
consider x2 being object such that
A10: x2 in dom g and
A11: y2 = g.x2 by A8,FUNCT_1:def 3;
consider x1 being object such that
A12: x1 in dom f and
A13: y1 = f.x1 by A7,FUNCT_1:def 3;
A14: [x1,x2] in [:dom f,dom g:] by A12,A10,ZFMISC_1:87;
[:f,g:].(x1,x2)=q by A9,A12,A13,A10,A11,Def8;
hence thesis by A14,A1,FUNCT_1:def 3;
end;
hence thesis by TARSKI:2;
end;
theorem Th68:
for f,g being Function st dom f = X & dom g = X holds <:f,g:> =
[:f,g:]*(delta X)
proof
let f,g be Function such that
A1: dom f = X & dom g = X;
A2: dom delta X = X by Def6;
rng delta X c= [:X,X:] by Th47;
then rng delta X c= dom [:f,g:] by A1,Def8;
then
A3: dom([:f,g:]*(delta X)) = X by A2,RELAT_1:27;
dom f /\ dom g = X by A1;
then
A4: dom <:f,g:> = X by Def7;
for x being object st x in X holds <:f,g:>.x = ([:f,g:]*(delta X)).x
proof
let x be object;
assume
A5: x in X;
hence <:f,g:>.x = [f.x,g.x] by A4,Def7
.= [:f,g:].(x,x) by A1,A5,Def8
.= [:f,g:].((delta X).x) by A5,Def6
.= ([:f,g:]*(delta X)).x by A3,A5,FUNCT_1:12;
end;
hence thesis by A4,A3;
end;
theorem
[:id X, id Y:] = id [:X,Y:]
proof
rng pr1(X,Y) c= X by Th43;
then
A1: (id X)*pr1(X,Y) = pr1(X,Y) by RELAT_1:53;
rng pr2(X,Y) c= Y by Th45;
then
A2: (id Y)*pr2(X,Y) = pr2(X,Y) by RELAT_1:53;
dom id X = X & dom id Y = Y;
hence [:id X, id Y:] = <:pr1(X,Y),pr2(X,Y):> by A1,A2,Th66
.= id [:X,Y:] by Th53;
end;
theorem
for f,g,h,k being Function holds [:f,h:]*<:g,k:> = <:f*g,h*k:>
proof
let f,g,h,k be Function;
for x being object holds x in dom([:f,h:]*<:g,k:>) iff x in dom <:f*g,h*k:>
proof let x be object;
thus x in dom([:f,h:]*<:g,k:>) implies x in dom <:f*g,h*k:>
proof
assume
A1: x in dom([:f,h:]*<:g,k:>);
then
A2: x in dom <:g,k:> by FUNCT_1:11;
then
A3: x in dom g /\ dom k by Def7;
then
A4: x in dom g by XBOOLE_0:def 4;
A5: x in dom k by A3,XBOOLE_0:def 4;
<:g,k:>.x in dom [:f,h:] by A1,FUNCT_1:11;
then [g.x,k.x] in dom [:f,h:] by A2,Def7;
then
A6: [g.x,k.x] in [:dom f,dom h:] by Def8;
then k.x in dom h by ZFMISC_1:87;
then
A7: x in dom(h*k) by A5,FUNCT_1:11;
g.x in dom f by A6,ZFMISC_1:87;
then x in dom(f*g) by A4,FUNCT_1:11;
then x in dom(f*g) /\ dom(h*k) by A7,XBOOLE_0:def 4;
hence thesis by Def7;
end;
assume x in dom <:f*g,h*k:>;
then
A8: x in dom(f*g) /\ dom(h*k) by Def7;
then
A9: x in dom(f*g) by XBOOLE_0:def 4;
A10: x in dom(h*k) by A8,XBOOLE_0:def 4;
then
A11: x in dom k by FUNCT_1:11;
x in dom g by A9,FUNCT_1:11;
then x in dom g /\ dom k by A11,XBOOLE_0:def 4;
then
A12: x in dom <:g,k:> by Def7;
A13: k.x in dom h by A10,FUNCT_1:11;
g.x in dom f by A9,FUNCT_1:11;
then [g.x,k.x] in [:dom f,dom h:] by A13,ZFMISC_1:87;
then [g.x,k.x] in dom [:f,h:] by Def8;
then <:g,k:>.x in dom [:f,h:] by A12,Def7;
hence thesis by A12,FUNCT_1:11;
end;
then
A14: dom([:f,h:]*<:g,k:>) = dom <:f*g,h*k:> by TARSKI:2;
for x being object st x in dom([:f,h:]*<:g,k:>)
holds ([:f,h:]*<:g,k:>).x = <:f*g,h*k :> . x
proof
let x be object;
assume
A15: x in dom([:f,h:]*<:g,k:>);
then
A16: x in dom <:g,k:> by FUNCT_1:11;
then
A17: x in dom g /\ dom k by Def7;
then
A18: x in dom g by XBOOLE_0:def 4;
<:g,k:>.x in dom [:f,h:] by A15,FUNCT_1:11;
then [g.x,k.x] in dom [:f,h:] by A16,Def7;
then
A19: [g.x,k.x] in [:dom f,dom h:] by Def8;
then
A20: g.x in dom f by ZFMISC_1:87;
A21: x in dom k by A17,XBOOLE_0:def 4;
A22: k.x in dom h by A19,ZFMISC_1:87;
then
A23: x in dom(h*k) by A21,FUNCT_1:11;
x in dom(f*g) by A20,A18,FUNCT_1:11;
then
A24: x in dom(f*g) /\ dom(h*k) by A23,XBOOLE_0:def 4;
thus ([:f,h:]*<:g,k:>).x = [:f,h:].(<:g,k:>.x) by A15,FUNCT_1:12
.= [:f,h:].(g.x,k.x) by A16,Def7
.= [f.(g.x),h.(k.x)] by A20,A22,Def8
.= [(f*g).x,h.(k.x)] by A18,FUNCT_1:13
.= [(f*g).x,(h*k).x] by A21,FUNCT_1:13
.= <:f*g,h*k:>.x by A24,Th48;
end;
hence thesis by A14;
end;
theorem
for f,g,h,k being Function holds [:f,h:]*[:g,k:] = [:f*g,h*k:]
proof
let f,g,h,k be Function;
A1: for x,y being object st x in dom(f*g) & y in dom(h*k)
holds ([:f,h:]*[:g,k:]).(x,y) = [:f*g,h*k:].(x,y)
proof
let x,y be object such that
A2: x in dom(f*g) and
A3: y in dom(h*k);
A4: g.x in dom f & k.y in dom h by A2,A3,FUNCT_1:11;
A5: x in dom g & y in dom k by A2,A3,FUNCT_1:11;
then [x,y] in [:dom g, dom k:] by ZFMISC_1:87;
then [x,y] in dom [:g,k:] by Def8;
hence ([:f,h:]*[:g,k:]).(x,y) = [:f,h:].([:g,k:].(x,y)) by FUNCT_1:13
.= [:f,h:].(g.x,k.y) by A5,Def8
.= [f.(g.x),h.(k.y)] by A4,Def8
.= [(f*g).x,h.(k.y)] by A2,FUNCT_1:12
.= [(f*g).x,(h*k).y] by A3,FUNCT_1:12
.= [:f*g,h*k:].(x,y) by A2,A3,Def8;
end;
for p being object
holds p in dom([:f,h:]*[:g,k:]) iff p in [:dom(f*g),dom(h*k):]
proof let p be object;
A6: dom [:g,k:] = [:dom g, dom k:] by Def8;
A7: dom [:f,h:] = [:dom f, dom h:] by Def8;
thus p in dom([:f,h:]*[:g,k:]) implies p in [:dom(f*g),dom(h*k):]
proof
assume
A8: p in dom([:f,h:]*[:g,k:]);
then
A9: [:g,k:].p in dom [:f,h:] by FUNCT_1:11;
A10: p in dom [:g,k:] by A8,FUNCT_1:11;
then consider x1,x2 being object such that
A11: x1 in dom g and
A12: x2 in dom k and
A13: p = [x1,x2] by A6,ZFMISC_1:def 2;
[:g,k:].(x1,x2) =[:g,k:].p by A13;
then
A14: [g.x1,k.x2] in dom [:f,h:] by A6,A10,A9,A13,Th65;
then k.x2 in dom h by A7,ZFMISC_1:87;
then
A15: x2 in dom(h*k) by A12,FUNCT_1:11;
g.x1 in dom f by A7,A14,ZFMISC_1:87;
then x1 in dom(f*g) by A11,FUNCT_1:11;
hence thesis by A13,A15,ZFMISC_1:87;
end;
assume p in [:dom(f*g),dom(h*k):];
then consider x1,x2 being object such that
A16: x1 in dom(f*g) & x2 in dom(h*k) and
A17: p = [x1,x2] by ZFMISC_1:def 2;
x1 in dom g & x2 in dom k by A16,FUNCT_1:11;
then
A18: [x1,x2] in dom [:g,k:] by A6,ZFMISC_1:87;
g.x1 in dom f & k.x2 in dom h by A16,FUNCT_1:11;
then [g.x1,k.x2] in dom [:f,h:] by A7,ZFMISC_1:87;
then [:g,k:].(x1,x2) in dom [:f,h:] by A6,A18,Th65;
hence thesis by A17,A18,FUNCT_1:11;
end;
then
A19: dom([:f,h:]*[:g,k:]) = [:dom(f*g),dom(h*k):] by TARSKI:2;
[:dom(f*g),dom(h*k):] = dom [:f*g,h*k:] by Def8;
hence thesis by A19,A1,Th6;
end;
theorem
for f,g being Function holds [:f,g:].:[:B,A:] = [:f.:B,g.:A:]
proof
let f,g be Function;
for q being object holds q in [:f,g:].:[:B,A:] iff q in [:f.:B,g.:A:]
proof let q be object;
A1: [:dom f,dom g:] = dom [:f,g:] by Def8;
thus q in [:f,g:].:[:B,A:] implies q in [:f.:B,g.:A:]
proof
assume q in [:f,g:].:[:B,A:];
then consider p being object such that
A2: p in dom [:f,g:] and
A3: p in [:B,A:] and
A4: q = [:f,g:].p by FUNCT_1:def 6;
dom [:f,g:] = [:dom f,dom g:] by Def8;
then consider x,y being object such that
A5: x in dom f and
A6: y in dom g and
A7: p =[x,y] by A2,ZFMISC_1:def 2;
x in B by A3,A7,ZFMISC_1:87;
then
A8: f.x in f.:B by A5,FUNCT_1:def 6;
y in A by A3,A7,ZFMISC_1:87;
then
A9: g.y in g.:A by A6,FUNCT_1:def 6;
q = [:f,g:].(x,y) by A4,A7;
then q=[f.x,g.y] by A5,A6,Def8;
hence thesis by A8,A9,ZFMISC_1:87;
end;
assume q in [:f.:B,g.:A:];
then consider y1,y2 being object such that
A10: y1 in f.:B and
A11: y2 in g.:A and
A12: q = [y1,y2] by ZFMISC_1:def 2;
consider x1 being object such that
A13: x1 in dom f and
A14: x1 in B and
A15: y1 = f.x1 by A10,FUNCT_1:def 6;
consider x2 being object such that
A16: x2 in dom g and
A17: x2 in A and
A18: y2 = g.x2 by A11,FUNCT_1:def 6;
A19: [:f,g:].(x1,x2) = [f.x1,g.x2] by A13,A16,Def8;
[x1,x2] in [:dom f,dom g:] & [x1,x2] in [:B,A:] by A13,A14,A16,A17,
ZFMISC_1:87;
hence thesis by A12,A15,A18,A1,A19,FUNCT_1:def 6;
end;
hence thesis by TARSKI:2;
end;
theorem
for f,g being Function holds [:f,g:]"[:B,A:] = [:f"B,g"A:]
proof
let f,g be Function;
for q being object holds q in [:f,g:]"[:B,A:] iff q in [:f"B,g"A:]
proof let q be object;
thus q in [:f,g:]"[:B,A:] implies q in [:f"B,g"A:]
proof
assume
A1: q in [:f,g:]"[:B,A:];
then
A2: [:f,g:].q in [:B,A:] by FUNCT_1:def 7;
q in dom [:f,g:] by A1,FUNCT_1:def 7;
then q in [:dom f,dom g:] by Def8;
then consider x1,x2 being object such that
A3: x1 in dom f and
A4: x2 in dom g and
A5: q = [x1,x2] by ZFMISC_1:def 2;
[:f,g:].q = [:f,g:].(x1,x2) by A5;
then
A6: [f.x1,g.x2] in [:B,A:] by A3,A4,A2,Def8;
then g.x2 in A by ZFMISC_1:87;
then
A7: x2 in g"A by A4,FUNCT_1:def 7;
f.x1 in B by A6,ZFMISC_1:87;
then x1 in f"B by A3,FUNCT_1:def 7;
hence thesis by A5,A7,ZFMISC_1:87;
end;
assume q in [:f"B,g"A:];
then consider x1,x2 being object such that
A8: x1 in f"B & x2 in g"A and
A9: q = [x1,x2] by ZFMISC_1:def 2;
f.x1 in B & g.x2 in A by A8,FUNCT_1:def 7;
then
A10: [f.x1,g.x2] in [:B,A:] by ZFMISC_1:87;
x1 in dom f & x2 in dom g by A8,FUNCT_1:def 7;
then
A11: [x1,x2] in [:dom f,dom g:] & [:f,g:].(x1,x2) = [f.x1,g.x2] by Def8,
ZFMISC_1:87;
[:dom f,dom g:] = dom [:f,g:] by Def8;
hence thesis by A9,A11,A10,FUNCT_1:def 7;
end;
hence thesis by TARSKI:2;
end;
theorem Th74:
for f being Function of X,Y for g being Function of V,Z holds [:
f,g:] is Function of [:X,V:],[:Y,Z:]
proof
let f be Function of X,Y;
let g be Function of V,Z;
per cases;
suppose
A1: [:Y,Z:] = {} implies [:X,V:] = {};
now
per cases by A1;
suppose
A2: [:Y,Z:] <> {};
rng f c= Y & rng g c= Z by RELAT_1:def 19;
then [:rng f,rng g:] c= [:Y,Z:] by ZFMISC_1:96;
then
A3: rng [:f,g:] c= [:Y,Z:] by Th67;
Z = {} implies V = {} by A2,ZFMISC_1:90;
then
A4: dom g = V by FUNCT_2:def 1;
Y = {} implies X = {} by A2,ZFMISC_1:90;
then dom f = X by FUNCT_2:def 1;
then dom[:f,g:] = [:X,V:] by A4,Def8;
hence thesis by A3,FUNCT_2:2;
end;
suppose
A5: [:X,V:] = {};
then X = {} or V = {};
then dom f = {} or dom g = {};
then [:dom f,dom g:] = {} by ZFMISC_1:90;
then
A6: dom[:f,g:] = [:X,V:] by A5,Def8;
rng f c= Y & rng g c= Z by RELAT_1:def 19;
then [:rng f,rng g:] c= [:Y,Z:] by ZFMISC_1:96;
then rng[:f,g:] c= [:Y,Z:] by Th67;
hence thesis by A6,FUNCT_2:2;
end;
end;
hence thesis;
end;
suppose
A7: [:Y,Z:] = {} & [:X,V:] <> {};
then Y = {} or Z = {};
then f = {} or g = {};
then [:dom f,dom g:] = {} by ZFMISC_1:90;
then
A8: dom [:f,g:] = {} by Def8;
then rng[:f,g:] = {} & dom [:f,g:] c= [:X,V:] by RELAT_1:42;
then reconsider R = [:f,g:] as Relation of [:X,V:],[:Y,Z:] by RELSET_1:4
,XBOOLE_1:2;
[:f,g:] = {} by A8;
then R is quasi_total by A7,FUNCT_2:def 1;
hence thesis;
end;
end;
definition
let X1,X2,Y1,Y2;
let f1 be Function of X1,Y1;
let f2 be Function of X2,Y2;
redefine func [:f1,f2:] -> Function of [:X1,X2:],[:Y1,Y2:]; :: redefines [: (FUNCT_3, definition)
coherence by Th74;
end;
theorem Th75:
for f1 being Function of C1,D1 for f2 being Function of C2,D2 for c1
being Element of C1 for c2 being Element of C2 holds [:f1,f2:].(c1,c2) = [f1.c1
,f2.c2]
proof
let f1 be Function of C1,D1;
let f2 be Function of C2,D2;
let c1 be Element of C1;
let c2 be Element of C2;
dom f1 = C1 & dom f2 = C2 by FUNCT_2:def 1;
hence thesis by Def8;
end;
theorem
for f1 being Function of X1,Y1 for f2 being Function of X2,Y2 st (Y1 =
{} implies X1 = {}) & (Y2 = {} implies X2 = {}) holds [:f1,f2:] = <:f1*pr1(X1,
X2),f2*pr2(X1,X2):>
proof
let f1 be Function of X1,Y1;
let f2 be Function of X2,Y2;
assume ( Y1 = {} implies X1 = {})&( Y2 = {} implies X2 = {});
then dom f1 = X1 & dom f2 = X2 by FUNCT_2:def 1;
hence thesis by Th66;
end;
theorem
for f1 being Function of X1,D1 for f2 being Function of X2,D2 holds [:
f1,f2:] = <:f1*pr1(X1,X2),f2*pr2(X1,X2):>
proof
let f1 be Function of X1,D1;
let f2 be Function of X2,D2;
dom f1 = X1 & dom f2 = X2 by FUNCT_2:def 1;
hence thesis by Th66;
end;
theorem
for f1 being Function of X,Y1 for f2 being Function of X,Y2 holds <:f1
,f2:> = [:f1,f2:]*(delta X)
proof
let f1 be Function of X,Y1;
let f2 be Function of X,Y2;
per cases;
suppose
Y1 = {} or Y2 = {};
then
A1: dom f1 = {} or dom f2 = {};
A2: dom[:f1,f2:] = [:dom f1, dom f2:] by Def8
.= {} by A1,ZFMISC_1:90;
dom<:f1,f2:> = dom f1 /\ dom f2 by Def7
.= {} by A1;
hence <:f1,f2:> = {}*delta X .= [:f1,f2:]*delta X by A2,RELAT_1:41;
end;
suppose
Y1 <> {} & Y2 <> {};
then dom f1 = X & dom f2 = X by FUNCT_2:def 1;
hence thesis by Th68;
end;
end;
begin :: Addenda
:: from AMI_1
theorem
for f being Function holds pr1(dom f,rng f).:f = dom f
proof
let f be Function;
now
let y be object;
thus y in dom f implies
ex x being object st x in dom pr1(dom f,rng f) & x in
f & y = pr1(dom f,rng f).x
proof
assume
A1: y in dom f;
take [y,f.y];
A2: f.y in rng f by A1,FUNCT_1:def 3;
then [y,f.y] in [:dom f,rng f:] by A1,ZFMISC_1:87;
hence [y,f.y] in dom pr1(dom f,rng f) by Def4;
thus [y,f.y] in f by A1,FUNCT_1:def 2;
thus y = pr1(dom f,rng f).(y,f.y) by A1,A2,Def4
.= pr1(dom f,rng f).[y,f.y];
end;
given x being object such that
A3: x in dom pr1(dom f,rng f) and
x in f and
A4: y = pr1(dom f,rng f).x;
consider x1,x2 being object such that
A5: x1 in dom f & x2 in rng f and
A6: x = [x1,x2] by A3,ZFMISC_1:84;
y = pr1(dom f,rng f).(x1,x2) by A4,A6;
hence y in dom f by A5,Def4;
end;
hence thesis by FUNCT_1:def 6;
end;
theorem
for A,B,C being non empty set, f,g being Function of A,[:B,C:] st
pr1(B,C)*f = pr1(B,C)*g & pr2(B,C)*f = pr2(B,C)*g holds f = g
proof
let A,B,C be non empty set, f,g be Function of A,[:B,C:] such that
A1: pr1(B,C)*f = pr1(B,C)*g & pr2(B,C)*f = pr2(B,C)*g;
now
let a be Element of A;
consider b1 being Element of B, c1 being Element of C such that
A2: f.a = [b1,c1] by DOMAIN_1:1;
consider b2 being Element of B, c2 being Element of C such that
A3: g.a = [b2,c2] by DOMAIN_1:1;
A4: pr1(B,C).(g.a) = (pr1(B,C)*g).a by FUNCT_2:15;
A5: pr1(B,C).(f.a) = (pr1(B,C)*f).a & pr2(B,C).(f.a) = (pr2(B,C)*f).a by
FUNCT_2:15;
A6: pr2(B,C).(b1,c1) = c1 & pr2(B,C).(b2,c2) = c2 by Def5;
pr1(B,C).(b1,c1) = b1 & pr1(B,C).(b2,c2) = b2 by Def4;
hence f.a = g.a by A1,A2,A3,A6,A5,A4,FUNCT_2:15;
end;
hence thesis;
end;
registration
let F,G be one-to-one Function;
cluster [:F,G:] -> one-to-one;
coherence
proof
let z1,z2 be object such that
A1: z1 in dom [:F,G:] and
A2: z2 in dom [:F,G:] and
A3: [:F,G:].z1 = [:F,G:].z2;
A4: dom[:F,G:] = [:dom F, dom G:] by Def8;
then consider x1,y1 being object such that
A5: x1 in dom F and
A6: y1 in dom G and
A7: z1 = [x1,y1] by A1,ZFMISC_1:84;
A8: [:F,G:].(x1,y1) = [F.x1,G.y1] by A5,A6,Def8;
consider x2,y2 being object such that
A9: x2 in dom F and
A10: y2 in dom G and
A11: z2 = [x2,y2] by A2,A4,ZFMISC_1:84;
A12: [:F,G:].(x2,y2) = [F.x2,G.y2] by A9,A10,Def8;
then F.x1 = F.x2 by A3,A7,A11,A8,XTUPLE_0:1;
then
A13: x1 = x2 by A5,A9,FUNCT_1:def 4;
G.y1 = G.y2 by A3,A7,A11,A8,A12,XTUPLE_0:1;
hence thesis by A6,A7,A10,A11,A13,FUNCT_1:def 4;
end;
end;
registration let A be set;
cluster idempotent for BinOp of A;
existence
proof
take pr1(A,A);
per cases;
suppose
A1: A <> {};
let a be Element of A;
a in A by A1;
hence pr1(A,A).(a,a) = a by Def4;
end;
suppose
A2: A = {};
let a be Element of A;
not [a,a] in dom pr1(A,A) by A2;
hence pr1(A,A).(a,a) = {} by FUNCT_1:def 2
.= a by A2,SUBSET_1:def 1;
end;
end;
end;
registration let A be set, b be idempotent BinOp of A;
let a be Element of A;
reduce b.(a,a) to a;
reducibility by BINOP_1:def 4;
end;
reserve A1,A2,B1,B2 for non empty set,
f for Function of A1,B1,
g for Function of A2,B2,
Y1 for non empty Subset of A1,
Y2 for non empty Subset of A2;
definition
let A1 be set, B1 be non empty set, f be Function of A1, B1, Y1 be Subset of
A1;
redefine func f|Y1 -> Function of Y1,B1; :: redefines | (RELAT_1, definition)
coherence by FUNCT_2:32;
end;
theorem
[:f,g:]|([:Y1,Y2:] qua Subset of [:A1,A2:])
qua Function of [:Y1,Y2:],[:B1,B2:]
= [:f|Y1,g|Y2:] qua Function of [:Y1,Y2:],[:B1,B2:]
proof
let a be Element of [:Y1,Y2:];
consider a1 being Element of Y1, a2 being Element of Y2 such that
A1: a = [a1,a2] by DOMAIN_1:1;
A2: (g|Y2).a2 = g.a2 by FUNCT_1:49;
A3: (f|Y1).a1 = f.a1 by FUNCT_1:49;
thus [:f|Y1,g|Y2:].a = [:f|Y1,g|Y2:].(a1,a2) by A1
.= [f.a1,g.a2] by A3,A2,Th75
.= [:f,g:].(a1,a2) by Th75
.= ([:f,g:]|[:Y1,Y2:]).a by A1,FUNCT_1:49;
end;