:: Functions and Their Basic Properties
:: by Czes{\l}aw Byli\'nski
::
:: Received March 3, 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 RELAT_1, XBOOLE_0, ZFMISC_1, SUBSET_1, TARSKI, SETFAM_1, FUNCT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, SETFAM_1;
constructors SETFAM_1, RELAT_1, XTUPLE_0;
registrations XBOOLE_0, RELAT_1, ZFMISC_1;
requirements SUBSET, BOOLE;
definitions TARSKI, XBOOLE_0, RELAT_1, SETFAM_1, ZFMISC_1;
equalities RELAT_1;
expansions TARSKI, XBOOLE_0, RELAT_1, ZFMISC_1;
theorems TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, XBOOLE_1, SUBSET_1, XTUPLE_0;
schemes TARSKI, XBOOLE_0;
begin
reserve X,X1,X2,Y,Y1,Y2 for set, p,x,x1,x2,y,y1,y2,z,z1,z2 for object;
definition
let X be set;
attr X is Function-like means
:Def1:
for x,y1,y2 st [x,y1] in X & [x,y2] in X holds y1 = y2;
end;
registration
cluster empty -> Function-like for set;
coherence;
end;
registration
cluster Function-like for Relation;
existence
proof
take {};
thus thesis;
end;
end;
definition
mode Function is Function-like Relation;
end;
registration
let a, b be object;
cluster {[a,b]} -> Function-like;
coherence
proof
set X = {[a, b]};
A1: [:{a},{b}:] = X by ZFMISC_1:29;
for x,y1,y2 be object st [x,y1] in X & [x,y2] in X holds y1 = y2
proof
let x,y1,y2 be object such that
A2: [x,y1] in X and
A3: [x,y2] in X;
y1 = b by A1,A2,ZFMISC_1:28;
hence thesis by A1,A3,ZFMISC_1:28;
end;
hence thesis;
end;
end;
reserve f,g,g1,g2,h for Function,
R,S for Relation;
scheme
GraphFunc { A()->set,P[object,object] } :
ex f st for x,y being object holds [x,y] in f iff x in A() & P[x,y]
provided
A1: for x,y1,y2 being object st P[x,y1] & P[x,y2] holds y1 = y2
proof
consider Y such that
A2: for y being object holds y in Y iff
ex x being object st x in A() & P[x,y]
from TARSKI:sch 1(A1);
defpred R[object] means ex x,y st [x,y] = $1 & P[x,y];
consider F being set such that
A3: for p being object holds
p in F iff p in [:A(),Y:] & R[p] from XBOOLE_0:sch 1;
now
thus for p being object holds p in F implies
ex x,y being object st [x,y] = p
proof let p be object;
p in F implies ex x,y st [x,y] = p & P[x,y] by A3;
hence thesis;
end;
let x,y1,y2;
assume [x,y1] in F;
then consider x1,z1 such that
A4: [x1,z1] = [x,y1] and
A5: P[x1,z1] by A3;
A6: x = x1 & z1 = y1 by A4,XTUPLE_0:1;
assume [x,y2] in F;
then consider x2,z2 such that
A7: [x2,z2] = [x,y2] and
A8: P[x2,z2] by A3;
x = x2 & z2 = y2 by A7,XTUPLE_0:1;
hence y1 = y2 by A1,A5,A8,A6;
end;
then reconsider f = F as Function by Def1,RELAT_1:def 1;
take f;
let x,y be object;
thus [x,y] in f implies x in A() & P[x,y]
proof
assume
A9: [x,y] in f;
then consider x1,y1 such that
A10: [x1,y1] = [x,y] and
A11: P[x1,y1] by A3;
[x,y] in [:A(),Y:] by A3,A9;
hence x in A() by ZFMISC_1:87;
x1 = x by A10,XTUPLE_0:1;
hence thesis by A10,A11,XTUPLE_0:1;
end;
assume that
A12: x in A() and
A13: P[x,y];
y in Y by A2,A12,A13;
then [x,y] in [:A(),Y:] by A12,ZFMISC_1:87;
hence thesis by A3,A13;
end;
definition
let f; let x be object;
func f.x -> set means
:Def2:
[x,it] in f if x in dom f otherwise it = {};
existence
proof
hereby assume x in dom f;
then consider y being object such that
A1: [x,y] in f by XTUPLE_0:def 12;
reconsider y as set by TARSKI:1;
take y;
thus [x,y] in f by A1;
end;
thus thesis;
end;
uniqueness by Def1;
consistency;
end;
theorem Th1:
[x,y] in f iff x in dom f & y = f.x
proof
thus [x,y] in f implies x in dom f & y = f.x
proof
assume
A1: [x,y] in f;
hence
A2: x in dom f by XTUPLE_0:def 12;
reconsider y as set by TARSKI:1;
y = f.x by A1,Def2,A2;
hence thesis;
end;
thus thesis by Def2;
end;
theorem Th2:
dom f = dom g & (for x st x in dom f holds f.x = g.x) implies f = g
proof
assume that
A1: dom f = dom g and
A2: for x st x in dom f holds f.x = g.x;
let x,y be object;
thus [x,y] in f implies [x,y] in g
proof
assume
A3: [x,y] in f;
then
A4: x in dom f by XTUPLE_0:def 12;
reconsider y as set by TARSKI:1;
f.x = y by A3,Def2,A4;
then g.x = y by A2,A4;
hence thesis by A1,A4,Def2;
end;
assume
A5: [x,y] in g;
then
A6: x in dom g by XTUPLE_0:def 12;
reconsider y as set by TARSKI:1;
g.x = y by A5,Def2,A6;
then f.x = y by A1,A2,A6;
hence thesis by A1,A6,Def2;
end;
definition
let f;
redefine func rng f means :: redefines rng (RELAT_1, synonym) → proj2 (XTUPLE_0, definition)
:Def3:
for y being object holds y in it iff
ex x being object st x in dom f & y = f.x;
compatibility
proof
let Y;
hereby
assume
A1: Y = rng f;
let y be object;
hereby
assume y in Y;
then consider x being object such that
A2: [x,y] in f by A1,XTUPLE_0:def 13;
take x;
thus x in dom f & y = f.x by A2,Th1;
end;
given x being object such that
A3: x in dom f & y = f.x;
[x,y] in f by A3,Def2;
hence y in Y by A1,XTUPLE_0:def 13;
end;
assume
A4: for y being object
holds y in Y iff ex x being object st x in dom f & y = f.x;
hereby
let y be object;
assume y in Y;
then consider x being object such that
A5: x in dom f & y = f.x by A4;
[x,y] in f by A5,Def2;
hence y in rng f by XTUPLE_0:def 13;
end;
let y be object;
assume y in rng f;
then consider x being object such that
A6: [x,y] in f by XTUPLE_0:def 13;
x in dom f & y = f.x by A6,Th1;
hence thesis by A4;
end;
end;
theorem
x in dom f implies f.x in rng f by Def3;
theorem Th4:
dom f = {x} implies rng f = {f.x}
proof
assume
A1: dom f = {x};
for y being object holds y in rng f iff y in {f.x}
proof let y be object;
thus y in rng f implies y in {f.x}
proof
assume y in rng f;
then consider z being object such that
A2: z in dom f and
A3: y = f.z by Def3;
z = x by A1,A2,TARSKI:def 1;
hence thesis by A3,TARSKI:def 1;
end;
assume y in {f.x};
then
A4: y = f.x by TARSKI:def 1;
x in dom f by A1,TARSKI:def 1;
hence thesis by A4,Def3;
end;
hence thesis by TARSKI:2;
end;
scheme
FuncEx { A()->set,P[object,object] } :
ex f st dom f = A() & for x st x in A() holds P[x,f.x]
provided
A1: for x,y1,y2 st x in A() & P[x,y1] & P[x,y2] holds y1 = y2 and
A2: for x st x in A() ex y st P[x,y]
proof
defpred R[object,object] means $1 in A() & P[$1,$2];
A3: for x,y1,y2 being object st R[x,y1] & R[x,y2] holds y1 = y2 by A1;
consider f being Function such that
A4: for x,y being object holds [x,y] in f iff x in A() & R[x,y]
from GraphFunc(A3);
take f;
for x being object holds x in dom f iff x in A()
proof let x be object;
thus x in dom f implies x in A()
proof
assume x in dom f;
then ex y being object st [x,y] in f by XTUPLE_0:def 12;
hence thesis by A4;
end;
assume
A5: x in A();
then consider y such that
A6: P[x,y] by A2;
[x,y] in f by A4,A5,A6;
hence thesis by XTUPLE_0:def 12;
end;
hence
A7: dom f = A() by TARSKI:2;
let x;
assume
A8: x in A();
then consider y such that
A9: P[x,y] by A2;
reconsider y as set by TARSKI:1;
[x,y] in f by A4,A8,A9;
hence thesis by A7,A8,A9,Def2;
end;
scheme
Lambda { A() -> set,F(object) -> object } :
ex f being Function st dom f = A() & for x st x in A() holds f.x = F(x)
proof
defpred P[object,object] means $2 = F($1);
A1: for x st x in A() ex y st P[x,y];
A2: for x,y1,y2 st x in A() & P[x,y1] & P[x,y2] holds y1 = y2;
thus ex f being Function st dom f = A() & for x st x in A() holds P[x,f.x]
from FuncEx(A2,A1);
end;
theorem Th5:
X <> {} implies for y ex f st dom f = X & rng f = {y}
proof
assume
A1: X <> {};
let y;
deffunc F(object) = y;
consider f such that
A2: dom f = X and
A3: for x st x in X holds f.x = F(x) from Lambda;
take f;
thus dom f = X by A2;
for y1 be object holds y1 in rng f iff y1 = y
proof
let y1 be object;
A4: now
set x = the Element of X;
assume
A5: y1 = y;
f.x = y by A1,A3;
hence y1 in rng f by A1,A2,A5,Def3;
end;
now
assume y1 in rng f;
then ex x being object st x in dom f & y1 = f.x by Def3;
hence y1 = y by A2,A3;
end;
hence thesis by A4;
end;
hence thesis by TARSKI:def 1;
end;
theorem
(for f,g st dom f = X & dom g = X holds f = g) implies X = {}
proof
deffunc F(object) = {};
assume
A1: for f,g st dom f = X & dom g = X holds f = g;
set x = the Element of X;
consider f being Function such that
A2: dom f = X and
A3: for x st x in X holds f.x = F(x) from Lambda;
assume
A4: not thesis;
then
A5: f.x = {} by A3;
deffunc F(object) = {{}};
consider g being Function such that
A6: dom g = X and
A7: for x st x in X holds g.x = F(x) from Lambda;
g.x = {{}} by A4,A7;
hence contradiction by A1,A2,A6,A5;
end;
theorem
dom f = dom g & rng f = {y} & rng g = {y} implies f = g
proof
assume that
A1: dom f = dom g and
A2: rng f = {y} and
A3: rng g = {y};
x in dom f implies f.x = g.x
proof
assume
A4: x in dom f;
then f.x in rng f by Def3;
then
A5: f.x = y by A2,TARSKI:def 1;
g.x in rng g by A1,A4,Def3;
hence thesis by A3,A5,TARSKI:def 1;
end;
hence thesis by A1,Th2;
end;
theorem
Y <> {} or X = {} implies ex f st X = dom f & rng f c= Y
proof
assume
A1: Y <> {} or X = {};
A2: now
set y = the Element of Y;
deffunc F(object) = y;
consider f such that
A3: dom f = X and
A4: for x st x in X holds f.x = F(x) from Lambda;
assume X <> {};
then
A5: y in Y by A1;
take f;
thus dom f = X by A3;
for z being object holds z in rng f implies z in Y
proof let z be object;
assume z in rng f;
then ex x being object st x in dom f & z = f.x by Def3;
hence thesis by A5,A3,A4;
end;
hence rng f c= Y;
end;
now
assume
A6: X = {};
take f = {};
thus dom f = X by A6;
thus rng f c= Y;
end;
hence thesis by A2;
end;
theorem
(for y st y in Y ex x st x in dom f & y = f.x) implies Y c= rng f
proof
assume
A1: for y st y in Y ex x st x in dom f & y = f.x;
let y be object;
assume y in Y;
then ex x st x in dom f & y = f.x by A1;
hence thesis by Def3;
end;
notation
let f,g;
synonym g*↑f for f*g;
end;
registration
let f,g;
cluster g*f -> Function-like;
coherence
proof
let x,y1,y2;
assume [x,y1] in g*f;
then consider z1 being object such that
A1: [x,z1] in f and
A2: [z1,y1] in g by RELAT_1:def 8;
assume [x,y2] in g*f;
then consider z2 being object such that
A3: [x,z2] in f and
A4: [z2,y2] in g by RELAT_1:def 8;
z1 = z2 by A1,A3,Def1;
hence thesis by A2,A4,Def1;
end;
end;
theorem
for h st (for x holds x in dom h iff x in dom f & f.x in dom g) & (for
x st x in dom h holds h.x = g.(f.x)) holds h = g*f
proof
let h;
assume that
A1: for x holds x in dom h iff x in dom f & f.x in dom g and
A2: for x st x in dom h holds h.x = g.(f.x);
now
let x,y be object;
hereby
assume
A3: [x,y] in h;
then
A4: x in dom h by XTUPLE_0:def 12;
then
A5: f.x in dom g by A1;
reconsider y1 = f.x as object;
take y1;
x in dom f by A1,A4;
hence [x,y1] in f by Def2;
reconsider yy=y as set by TARSKI:1;
yy = h.x by A3,A4,Def2
.= g.(f.x) by A2,A4;
hence [y1,y] in g by A5,Def2;
end;
given z being object such that
A6: [x,z] in f and
A7: [z,y] in g;
A8: x in dom f by A6,XTUPLE_0:def 12;
reconsider z as set by TARSKI:1;
A9: z = f.x by A6,Def2,A8;
A10: z in dom g by A7,XTUPLE_0:def 12;
then
A11: x in dom h by A1,A8,A9;
reconsider yy=y as set by TARSKI:1;
yy = g.z by A7,A10,Def2;
then y = h.x by A2,A9,A11;
hence [x,y] in h by A11,Def2;
end;
hence thesis by RELAT_1:def 8;
end;
theorem Th11:
x in dom(g*f) iff x in dom f & f.x in dom g
proof
set h = g*f;
hereby
assume x in dom h;
then consider y being object such that
A1: [x,y] in h by XTUPLE_0:def 12;
consider z being object such that
A2: [x,z] in f and
A3: [z,y] in g by A1,RELAT_1:def 8;
reconsider z as set by TARSKI:1;
thus x in dom f by A2,XTUPLE_0:def 12;
then z = f.x by A2,Def2;
hence f.x in dom g by A3,XTUPLE_0:def 12;
end;
assume
A4: x in dom f;
then consider z being object such that
A5: [x,z] in f by XTUPLE_0:def 12;
assume f.x in dom g;
then consider y being object such that
A6: [f.x,y] in g by XTUPLE_0:def 12;
reconsider z as set by TARSKI:1;
z = f.x by A4,A5,Def2;
then [x,y] in h by A5,A6,RELAT_1:def 8;
hence thesis by XTUPLE_0:def 12;
end;
theorem Th12:
x in dom(g*f) implies (g*f).x = g.(f.x)
proof
set h = g*f;
assume
A1: x in dom h;
then consider y being object such that
A2: [x,y] in h by XTUPLE_0:def 12;
consider z being object such that
A3: [x,z] in f and
A4: [z,y] in g by A2,RELAT_1:def 8;
reconsider z,y as set by TARSKI:1;
x in dom f by A3,XTUPLE_0:def 12;
then
A5: z = f.x by A3,Def2;
then f.x in dom g by A4,XTUPLE_0:def 12;
then y = g.(f.x) by A4,A5,Def2;
hence thesis by A1,A2,Def2;
end;
theorem Th13:
x in dom f implies (g*f).x = g.(f.x)
proof
assume
A1: x in dom f;
per cases;
suppose
f.x in dom g;
then x in dom(g*f) by A1,Th11;
hence thesis by Th12;
end;
suppose
A2: not f.x in dom g;
then not x in dom(g*f) by Th11;
hence (g*f).x = {} by Def2
.= g.(f.x) by A2,Def2;
end;
end;
theorem
z in rng(g*f) implies z in rng g
proof
assume z in rng(g*f);
then consider x being object such that
A1: x in dom(g*f) and
A2: z = (g*f).x by Def3;
f.x in dom g & (g*f).x = g.(f.x) by A1,Th11,Th12;
hence thesis by A2,Def3;
end;
theorem Th15:
dom(g*f) = dom f implies rng f c= dom g
proof
assume
A1: dom(g*f) = dom f;
let y be object;
assume y in rng f;
then ex x being object st x in dom f & y = f.x by Def3;
hence thesis by A1,Th11;
end;
theorem
rng f c= Y & (for g,h st dom g = Y & dom h = Y & g*f = h*f holds g = h)
implies Y = rng f
proof
assume that
A1: rng f c= Y and
A2: for g,h st dom g = Y & dom h = Y & g*f = h*f holds g = h;
Y c= rng f
proof
deffunc F(object) = {};
let y be object;
assume that
A3: y in Y and
A4: not y in rng f;
defpred P[object,object] means
($1 = y implies $2 = {{}}) & ($1 <> y implies $2 = {});
A5: x in Y implies ex y1 st P[x,y1]
proof
assume x in Y;
x = y implies thesis;
hence thesis;
end;
A6: for x,y1,y2 st x in Y & P[x,y1] & P[x,y2] holds y1 = y2;
consider h being Function such that
A7: dom h = Y and
A8: for x st x in Y holds P[x,h.x] from FuncEx(A6,A5);
A9: dom(h*f) = dom f by A1,A7,RELAT_1:27;
consider g being Function such that
A10: dom g = Y and
A11: x in Y implies g.x = F(x) from Lambda;
A12: dom(g*f) = dom f by A1,A10,RELAT_1:27;
x in dom f implies (g*f).x = (h*f).x
proof
assume
A13: x in dom f;
then f.x in rng f by Def3;
then
A14: g.(f.x) = {} & h.(f.x) = {} by A1,A4,A11,A8;
(g*f).x = g.(f.x) by A12,A13,Th12;
hence thesis by A9,A13,A14,Th12;
end;
then
A15: g = h by A2,A10,A7,A12,A9,Th2;
g.y = {} by A3,A11;
hence contradiction by A3,A8,A15;
end;
hence thesis by A1;
end;
registration
let X;
cluster id X -> Function-like;
coherence
proof
let x,y1,y2;
assume that
A1: [x,y1] in id X and
A2: [x,y2] in id X;
x = y1 by A1,RELAT_1:def 10;
hence thesis by A2,RELAT_1:def 10;
end;
end;
theorem Th17:
f = id X iff dom f = X & for x st x in X holds f.x = x
proof
hereby
assume
A1: f = id X;
hence
A2: dom f = X;
let x;
assume
A3: x in X;
then [x,x] in f by A1,RELAT_1:def 10;
hence f.x = x by A2,A3,Def2;
end;
assume that
A4: dom f = X and
A5: for x st x in X holds f.x = x;
now
let x,y be object;
hereby
assume
A6: [x,y] in f;
hence
A7: x in X by A4,Th1;
y = f.x by A6,Th1;
hence x = y by A5,A7;
end;
assume
A8: x in X;
then f.x = x by A5;
hence x = y implies [x,y] in f by A4,A8,Th1;
end;
hence thesis by RELAT_1:def 10;
end;
theorem Th18:
x in X implies (id X).x = x by Th17;
theorem Th19:
dom(f*(id X)) = dom f /\ X
proof
for x being object holds x in dom(f*(id X)) iff x in dom f /\ X
proof let x be object;
x in dom(f*(id X)) iff x in dom f & x in X
proof
thus x in dom(f*(id X)) implies x in dom f & x in X
proof
assume x in dom(f*(id X));
then
A1: x in dom((id X)) & (id X).x in dom f by Th11;
thus thesis by A1,Th17;
end;
assume
A2: x in dom f;
A3: dom((id X)) = X;
assume
A4: x in X;
then (id X).x in dom f by A2,Th17;
hence thesis by A4,A3,Th11;
end;
hence thesis by XBOOLE_0:def 4;
end;
hence thesis by TARSKI:2;
end;
theorem
x in dom f /\ X implies f.x = (f*(id X)).x
proof
assume x in dom f /\ X;
then x in X by XBOOLE_0:def 4;
then (id X).x = x & x in dom id X by Th17;
hence thesis by Th13;
end;
theorem
x in dom((id Y)*f) iff x in dom f & f.x in Y
proof
dom((id Y)) = Y;
hence thesis by Th11;
end;
theorem
(id X)*(id Y) = id(X /\ Y)
proof
A1: dom((id X)*(id Y)) = dom((id X)) /\ Y by Th19
.= X /\ Y;
A2: z in X /\ Y implies ((id X)*(id Y)).z = (id(X /\ Y)).z
proof
assume
A3: z in X /\ Y;
then
A4: z in X by XBOOLE_0:def 4;
A5: z in Y by A3,XBOOLE_0:def 4;
thus ((id X)*(id Y)).z = (id X).((id Y).z) by A1,A3,Th12
.= (id X).z by A5,Th17
.= z by A4,Th17
.= (id(X /\ Y)).z by A3,Th17;
end;
X /\ Y = dom id(X /\ Y);
hence thesis by A1,A2,Th2;
end;
theorem Th23:
rng f = dom g & g*f = f implies g = id dom g
proof
assume that
A1: rng f = dom g and
A2: g*f = f;
set X = dom g;
x in X implies g.x = x
proof
assume x in X;
then ex y being object st y in dom f & f.y = x by A1,Def3;
hence thesis by A2,Th13;
end;
hence thesis by Th17;
end;
definition
let f;
attr f is one-to-one means
:Def4:
for x1,x2 st x1 in dom f & x2 in dom f & f.x1 = f.x2 holds x1 = x2;
end;
theorem Th24:
f is one-to-one & g is one-to-one implies g*f is one-to-one
proof
assume that
A1: f is one-to-one and
A2: g is one-to-one;
now
let x1,x2;
assume
A3: x1 in dom(g*f) & x2 in dom(g*f);
then
A4: (g*f).x1 = g.(f.x1) & (g*f).x2 = g .(f.x2) by Th12;
A5: x1 in dom f & x2 in dom f by A3,Th11;
assume
A6: (g*f).x1 = (g*f).x2;
f.x1 in dom g & f.x2 in dom g by A3,Th11;
then f.x1 = f.x2 by A2,A4,A6;
hence x1 = x2 by A1,A5;
end;
hence thesis;
end;
theorem Th25:
g*f is one-to-one & rng f c= dom g implies f is one-to-one
proof
assume that
A1: g*f is one-to-one and
A2: rng f c= dom g;
now
let x1,x2;
assume that
A3: x1 in dom f & x2 in dom f and
A4: f.x1 =f.x2;
A5: x1 in dom(g*f) & x2 in dom(g*f) by A2,A3,RELAT_1:27;
(g*f).x1 = g.(f.x1) & (g*f).x2 = g.(f.x2) by A3,Th13;
hence x1 = x2 by A1,A4,A5;
end;
hence thesis;
end;
theorem
g*f is one-to-one & rng f = dom g implies f is one-to-one & g is one-to-one
proof
assume that
A1: g*f is one-to-one and
A2: rng f = dom g;
A3: dom(g*f) = dom f by A2,RELAT_1:27;
thus f is one-to-one by A1,A2,Th25;
assume not g is one-to-one;
then consider y1,y2 such that
A4: y1 in dom g and
A5: y2 in dom g and
A6: g.y1 = g.y2 & y1 <> y2;
consider x2 being object such that
A7: x2 in dom f and
A8: f.x2 = y2 by A2,A5,Def3;
A9: (g*f).x2 = g.(f.x2) by A7,Th13;
consider x1 being object such that
A10: x1 in dom f and
A11: f.x1 = y1 by A2,A4,Def3;
(g*f).x1 = g.(f.x1) by A10,Th13;
hence contradiction by A1,A6,A10,A11,A7,A8,A3,A9;
end;
theorem
f is one-to-one iff for g,h st rng g c= dom f & rng h c= dom f & dom g
= dom h & f*g = f*h holds g = h
proof
thus f is one-to-one implies for g,h st rng g c=dom f & rng h c=dom f & dom
g = dom h & f*g = f*h holds g = h
proof
assume
A1: f is one-to-one;
let g,h such that
A2: rng g c= dom f & rng h c= dom f and
A3: dom g = dom h and
A4: f*g = f*h;
x in dom g implies g.x = h.x
proof
assume
A5: x in dom g;
then
A6: g.x in rng g & h.x in rng h by A3,Def3;
(f*g).x = f.(g.x) & (f*h).x = f.(h.x) by A3,A5,Th13;
hence thesis by A1,A2,A4,A6;
end;
hence thesis by A3,Th2;
end;
assume
A7: for g,h st rng g c=dom f & rng h c=dom f & dom g = dom h & f*g = f*
h holds g = h;
x1 in dom f & x2 in dom f & f.x1 = f.x2 implies x1 = x2
proof
assume that
A8: x1 in dom f and
A9: x2 in dom f and
A10: f.x1 = f.x2;
deffunc F(object) = x1;
consider g being Function such that
A11: dom g = {{}} and
A12: for x st x in {{}} holds g.x = F(x) from Lambda;
A13: {} in {{}} by TARSKI:def 1;
then
A14: g.{} = x1 by A12;
then rng g = {x1} by A11,Th4;
then
A15: rng g c= dom f by A8,ZFMISC_1:31;
then
A16: dom(f*g) = dom g by RELAT_1:27;
deffunc F(object) = x2;
consider h being Function such that
A17: dom h = {{}} and
A18: for x st x in {{}} holds h.x = F(x) from Lambda;
A19: h.{} = x2 by A18,A13;
then rng h = {x2} by A17,Th4;
then
A20: rng h c= dom f by A9,ZFMISC_1:31;
then
A21: dom(f*h) = dom h by RELAT_1:27;
x in dom(f*g) implies (f*g).x = (f*h).x
proof
assume
A22: x in dom(f*g);
then
A23: g.x = x1 by A11,A12,A16;
(f*g).x = f.(g.x) & (f*h).x = f.(h.x) by A11,A17,A16,A21,A22,Th12;
hence thesis by A10,A11,A18,A16,A22,A23;
end;
hence thesis by A7,A11,A17,A14,A19,A15,A20,A16,A21,Th2;
end;
hence thesis;
end;
theorem
dom f = X & dom g = X & rng g c= X & f is one-to-one & f*g = f implies
g = id X
proof
assume that
A1: dom f = X and
A2: dom g = X and
A3: rng g c= X & f is one-to-one and
A4: f*g = f;
x in X implies g.x = x
proof
assume
A5: x in X;
then g.x in rng g & f.x = f.(g.x) by A2,A4,Def3,Th13;
hence thesis by A1,A3,A5;
end;
hence thesis by A2,Th17;
end;
theorem
rng(g*f) = rng g & g is one-to-one implies dom g c= rng f
proof
assume that
A1: rng(g*f) = rng g and
A2: g is one-to-one;
let y be object;
assume
A3: y in dom g;
then g.y in rng(g*f) by A1,Def3;
then consider x being object such that
A4: x in dom(g*f) and
A5: g.y = (g*f).x by Def3;
(g*f).x = g.(f.x) & f.x in dom g by A4,Th11,Th12;
then
A6: y = f.x by A2,A3,A5;
x in dom f by A4,Th11;
hence thesis by A6,Def3;
end;
registration
let X be set;
cluster id X -> one-to-one;
coherence
proof
let x1,x2;
assume that
A1: x1 in dom id X and
A2: x2 in dom id X;
x1 in X by A1;
then
A3: (id X).x1 = x1 by Th17;
x2 in X by A2;
hence thesis by A3,Th17;
end;
end;
::$CT
theorem
(ex g st g*f = id dom f) implies f is one-to-one
proof
given g such that
A1: g*f = id dom f;
dom(g*f) = dom f by A1;
then rng f c= dom g by Th15;
hence thesis by A1,Th25;
end;
registration
cluster empty -> one-to-one for Function;
coherence;
end;
registration
cluster one-to-one for Function;
existence
proof
take {};
thus thesis;
end;
end;
registration
let f be one-to-one Function;
cluster f~ -> Function-like;
coherence
proof
let x,y1,y2;
assume that
A1: [x,y1] in f~ and
A2: [x,y2] in f~;
A3: [y2,x] in f by A2,RELAT_1:def 7;
then
A4: y2 in dom f by XTUPLE_0:def 12;
reconsider x as set by TARSKI:1;
A5: x = f.y2 by A3,Def2,A4;
A6: [y1,x] in f by A1,RELAT_1:def 7;
then
A7: y1 in dom f by XTUPLE_0:def 12;
then x = f.y1 by A6,Def2;
hence thesis by A7,A4,A5,Def4;
end;
end;
definition
let f;
assume
A1: f is one-to-one;
func f" -> Function equals
:Def5:
f~;
coherence by A1;
end;
theorem Th31:
f is one-to-one implies for g being Function holds g=f" iff dom
g = rng f & for y,x holds y in rng f & x = g.y iff x in dom f & y = f.x
proof
assume
A1: f is one-to-one;
let g be Function;
thus g = f" implies dom g = rng f & for y,x holds y in rng f & x = g.y iff x
in dom f & y = f.x
proof
assume g = f";
then
A2: g = f~ by A1,Def5;
hence dom g = rng f by RELAT_1:20;
let y,x;
thus y in rng f & x = g.y implies x in dom f & y = f.x
proof
assume that
A3: y in rng f and
A4: x = g.y;
reconsider y as set by TARSKI:1;
y in dom g by A2,A3,RELAT_1:20;
then [y,x] in g by A4,Def2;
then
A5: [x,y] in f by A2,RELAT_1:def 7;
hence x in dom f by XTUPLE_0:def 12;
hence thesis by A5,Def2;
end;
assume x in dom f & y = f.x;
then
A6: [x,y] in f by Def2;
hence y in rng f by XTUPLE_0:def 13;
then
A7: y in dom g by A2,RELAT_1:20;
reconsider x as set by TARSKI:1;
[y,x] in g by A2,A6,RELAT_1:def 7;
hence thesis by A7,Def2;
end;
assume that
A8: dom g = rng f and
A9: for y,x holds y in rng f & x = g.y iff x in dom f & y = f.x;
let a,b be object;
thus [a,b] in g implies [a,b] in f"
proof
assume
A10: [a,b] in g;
reconsider b as set by TARSKI:1;
A11: a in dom g by XTUPLE_0:def 12,A10;
then b = g.a by A10,Def2;
then b in dom f & a = f.b by A8,A9,A11;
then [b,a] in f by Def2;
then [a,b] in f~ by RELAT_1:def 7;
hence thesis by A1,Def5;
end;
assume [a,b] in f";
then [a,b] in f~ by A1,Def5;
then
A12: [b,a] in f by RELAT_1:def 7;
then
A13: b in dom f by XTUPLE_0:def 12;
reconsider a as set by TARSKI:1;
a = f.b by A12,Def2,A13;
then a in rng f & b = g.a by A9,A13;
hence thesis by A8,Def2;
end;
theorem Th32:
f is one-to-one implies rng f = dom(f") & dom f = rng(f")
proof
assume f is one-to-one;
then f" = f~ by Def5;
hence thesis by RELAT_1:20;
end;
theorem Th33:
f is one-to-one & x in dom f implies x = (f").(f.x) & x = (f"*f) .x
proof
assume
A1: f is one-to-one;
assume
A2: x in dom f;
hence x = (f").(f.x) by A1,Th31;
hence thesis by A2,Th13;
end;
theorem Th34:
f is one-to-one & y in rng f implies y = f.((f").y) & y = (f*f") .y
proof
assume
A1: f is one-to-one;
assume
A2: y in rng f;
hence
A3: y = f.((f").y) by A1,Th31;
rng f = dom(f") by A1,Th32;
hence thesis by A2,A3,Th13;
end;
theorem Th35:
f is one-to-one implies dom(f"*f) = dom f & rng(f"*f) = dom f
proof
assume
A1: f is one-to-one;
then
A2: rng f = dom(f") by Th32;
then rng(f"*f) = rng(f") by RELAT_1:28;
hence thesis by A1,A2,Th32,RELAT_1:27;
end;
theorem Th36:
f is one-to-one implies dom(f*f") = rng f & rng(f*f") = rng f
proof
assume
A1: f is one-to-one;
then
A2: rng(f") = dom f by Th32;
then dom(f*f") = dom(f") by RELAT_1:27;
hence thesis by A1,A2,Th32,RELAT_1:28;
end;
theorem
f is one-to-one & dom f = rng g & rng f = dom g & (for x,y st x in dom
f & y in dom g holds f.x = y iff g.y = x) implies g = f"
proof
assume that
A1: f is one-to-one and
A2: dom f = rng g and
A3: rng f = dom g and
A4: for x,y st x in dom f & y in dom g holds f.x = y iff g.y = x;
A5: y in dom g implies g.y = (f").y
proof
assume
A6: y in dom g;
then
A7: g.y in dom f by A2,Def3;
then f.(g.y) = y by A4,A6;
hence thesis by A1,A7,Th31;
end;
rng f = dom(f") by A1,Th31;
hence thesis by A3,A5,Th2;
end;
theorem Th38:
f is one-to-one implies f"*f = id dom f & f*f" = id rng f
proof
assume
A1: f is one-to-one;
A2: x in dom(f"*f) implies (f"*f).x = x
proof
assume x in dom(f"*f);
then x in dom f by A1,Th35;
hence thesis by A1,Th33;
end;
A3: x in dom(f*f") implies (f*f").x = x
proof
assume x in dom(f*f");
then x in rng f by A1,Th36;
hence thesis by A1,Th34;
end;
dom(f"*f) = dom f by A1,Th35;
hence f"*f = id dom f by A2,Th17;
dom(f*f") = rng f by A1,Th36;
hence thesis by A3,Th17;
end;
theorem Th39:
f is one-to-one implies f" is one-to-one
proof
assume
A1: f is one-to-one;
let y1,y2;
assume that
A2: y1 in dom(f") and
A3: y2 in dom(f");
y1 in rng f by A1,A2,Th31;
then
A4: y1 = f.((f").y1) by A1,Th34;
y2 in rng f by A1,A3,Th31;
hence thesis by A1,A4,Th34;
end;
registration
let f be one-to-one Function;
cluster f" -> one-to-one;
coherence by Th39;
let g be one-to-one Function;
cluster g*f -> one-to-one;
coherence by Th24;
end;
Lm1: rng(g2) = X & f*g2 = id dom g1 & g1*f = id X implies g1 = g2
proof
A1: g1*(f*g2) = (g1*f)*g2 & g1*(id dom g1) = g1 by RELAT_1:36,51;
assume rng(g2) = X & f*g2 = id dom g1 & g1*f = id X;
hence thesis by A1,RELAT_1:53;
end;
theorem Th40:
f is one-to-one & rng f = dom g & g*f = id dom f implies g = f"
proof
assume that
A1: f is one-to-one and
A2: rng f = dom g & g*f = id dom f;
f*f" = id rng f & rng(f") = dom f by A1,Th32,Th38;
hence thesis by A2,Lm1;
end;
theorem
f is one-to-one & rng g = dom f & f*g = id rng f implies g = f"
proof
assume that
A1: f is one-to-one and
A2: rng g = dom f & f*g = id rng f;
f"*f = id dom f & dom(f") = rng f by A1,Th32,Th38;
hence thesis by A2,Lm1;
end;
theorem
f is one-to-one implies (f")" = f
proof
assume
A1: f is one-to-one;
then rng f = dom(f") by Th32;
then
A2: f*f" = id dom(f") by A1,Th38;
dom f = rng(f") by A1,Th32;
hence thesis by A1,A2,Th40;
end;
theorem
f is one-to-one & g is one-to-one implies (g*f)" = f"*g"
proof
assume that
A1: f is one-to-one and
A2: g is one-to-one;
for y being object holds y in rng(g*f) iff y in dom(f"*g")
proof let y be object;
thus y in rng(g*f) implies y in dom(f"*g")
proof
assume y in rng(g*f);
then consider x being object such that
A3: x in dom(g*f) and
A4: y = (g*f).x by Def3;
A5: f.x in dom g by A3,Th11;
A6: y = g.(f.x) by A3,A4,Th12;
then y in rng g by A5,Def3;
then
A7: y in dom(g") by A2,Th31;
A8: x in dom f by A3,Th11;
(g").(g.(f.x)) = (g"*g).(f.x) by A5,Th13
.= (id dom g).(f.x) by A2,Th38
.= f.x by A5,Th17;
then (g").y in rng f by A8,A6,Def3;
then (g").y in dom(f") by A1,Th31;
hence thesis by A7,Th11;
end;
assume
A9: y in dom(f"*g");
then y in dom(g") by Th11;
then y in rng g by A2,Th31;
then consider z being object such that
A10: z in dom g and
A11: y = g.z by Def3;
(g").y in dom(f") by A9,Th11;
then (g").(g.z) in rng f by A1,A11,Th31;
then (g"*g).z in rng f by A10,Th13;
then (id dom g).z in rng f by A2,Th38;
then z in rng f by A10,Th17;
then consider x being object such that
A12: x in dom f & z = f.x by Def3;
x in dom(g*f) & y = (g*f).x by A10,A11,A12,Th11,Th13;
hence thesis by Def3;
end;
then
A13: rng(g*f) = dom(f"*g") by TARSKI:2;
for x being object holds x in dom((f"*g")*(g*f)) iff x in dom(g*f)
proof let x be object;
thus x in dom((f"*g")*(g*f)) implies x in dom(g*f) by Th11;
assume
A14: x in dom(g*f);
then (g*f).x in rng(g*f) by Def3;
hence thesis by A13,A14,Th11;
end;
then
A15: dom((f"*g")*(g*f)) = dom(g*f) by TARSKI:2;
x in dom(g*f) implies ((f"*g")*(g*f)).x = x
proof
assume
A16: x in dom(g*f);
then
A17: f.x in dom g by Th11;
(g*f).x in rng(g*f) by A16,Def3;
then
A18: g.(f.x) in dom(f"*g") by A13,A16,Th12;
A19: x in dom f by A16,Th11;
thus ((f"*g")*(g*f)).x = (f"*g").((g*f).x) by A15,A16,Th12
.= (f"*g").(g.(f.x)) by A16,Th12
.= (f").((g").(g.(f.x))) by A18,Th12
.= (f").((g"*g).(f.x)) by A17,Th13
.= (f").((id dom g).(f.x)) by A2,Th38
.= (f").(f.x) by A17,Th17
.= x by A1,A19,Th33;
end;
then (f"*g")*(g*f) = id dom(g*f) by A15,Th17;
hence thesis by A1,A2,A13,Th40;
end;
theorem
(id X)" = id X
proof
dom id X = X;
then
A1: (id X)"*(id X) = id X by Th38;
dom((id X)") = rng id X & rng id X = X by Th32;
hence thesis by A1,Th23;
end;
registration
let f,X;
cluster f|X -> Function-like;
coherence
proof
let x,y1,y2;
assume [x,y1] in f|X & [x,y2] in f|X;
then [x,y1] in f & [x,y2] in f by RELAT_1:def 11;
hence thesis by Def1;
end;
end;
theorem
dom g = dom f /\ X & (for x st x in dom g holds g.x = f.x) implies g = f|X
proof
assume that
A1: dom g = dom f /\ X and
A2: for x st x in dom g holds g.x = f.x;
now
let x,y be object;
hereby
assume
A3: [x,y] in g;
then
A4: x in dom g by XTUPLE_0:def 12;
hence x in X by A1,XBOOLE_0:def 4;
A5: x in dom f by A1,A4,XBOOLE_0:def 4;
reconsider yy=y as set by TARSKI:1;
yy = g.x by A3,A4,Def2
.= f.x by A2,A4;
hence [x,y] in f by A5,Def2;
end;
assume
A6: x in X;
assume
A7: [x,y] in f;
then
A8: x in dom f by XTUPLE_0:def 12;
then
A9: x in dom g by A1,A6,XBOOLE_0:def 4;
reconsider yy=y as set by TARSKI:1;
yy = f.x by A7,A8,Def2
.= g.x by A2,A9;
hence [x,y] in g by A9,Def2;
end;
hence thesis by RELAT_1:def 11;
end;
theorem Th46:
x in dom(f|X) implies (f|X).x = f.x
proof
set g = f|X;
assume
A1: x in dom g;
dom g = dom f /\ X by RELAT_1:61;
then
A2: x in dom f by A1,XBOOLE_0:def 4;
g c= f & [x,g.x] in g by A1,Def2,RELAT_1:59;
hence g.x = f.x by A2,Def2;
end;
theorem Th47:
x in dom f /\ X implies (f|X).x = f.x
proof
assume x in dom f /\ X;
then x in dom(f|X) by RELAT_1:61;
hence thesis by Th46;
end;
theorem Th48:
x in X implies (f|X).x = f.x
proof
assume
A1: x in X;
per cases;
suppose
x in dom f;
then x in dom(f|X) by A1,RELAT_1:57;
hence thesis by Th46;
end;
suppose
A2: not x in dom f;
then not x in dom(f|X) by RELAT_1:57;
hence (f|X).x = {} by Def2
.= f.x by A2,Def2;
end;
end;
theorem
x in dom f & x in X implies f.x in rng(f|X)
proof
assume that
A1: x in dom f and
A2: x in X;
x in dom f /\ X by A1,A2,XBOOLE_0:def 4;
then
A3: x in dom(f|X) by RELAT_1:61;
(f|X).x = f.x by A2,Th48;
hence thesis by A3,Def3;
end;
theorem
X c= Y implies (f|X)|Y = f|X & (f|Y)|X = f|X by RELAT_1:73,74;
theorem
f is one-to-one implies f|X is one-to-one
proof
assume
A1: f is one-to-one;
let x1,x2;
assume that
A2: x1 in dom(f|X) and
A3: x2 in dom(f|X);
x1 in dom f /\ X by A2,RELAT_1:61;
then
A4: x1 in dom f by XBOOLE_0:def 4;
x2 in dom f /\ X by A3,RELAT_1:61;
then
A5: x2 in dom f by XBOOLE_0:def 4;
(f|X).x1 = f.x1 & (f|X).x2 = f.x2 by A2,A3,Th46;
hence thesis by A1,A4,A5;
end;
registration
let Y,f;
cluster Y|`f -> Function-like;
coherence
proof
let x,y1,y2;
assume [x,y1] in Y|`f & [x,y2] in Y|`f;
then [x,y1] in f & [x,y2] in f by RELAT_1:def 12;
hence thesis by Def1;
end;
end;
theorem Th52:
g = Y|`f iff (for x holds x in dom g iff x in dom f & f.x in Y) &
for x st x in dom g holds g.x = f.x
proof
hereby
assume
A1: g = Y|`f;
hereby
let x;
hereby
assume x in dom g;
then
A2: [x,g.x] in g by Def2;
then
A3: [x,g.x] in f by A1,RELAT_1:def 12;
hence x in dom f by XTUPLE_0:def 12;
then f.x = g.x by A3,Def2;
hence f.x in Y by A1,A2,RELAT_1:def 12;
end;
assume x in dom f;
then
A4: [x,f.x] in f by Def2;
assume f.x in Y;
then [x,f.x] in g by A1,A4,RELAT_1:def 12;
hence x in dom g by XTUPLE_0:def 12;
end;
let x;
assume x in dom g;
then [x,g.x] in g by Def2;
then
A5: [x,g.x] in f by A1,RELAT_1:def 12;
then x in dom f by XTUPLE_0:def 12;
hence f.x = g.x by A5,Def2;
end;
assume that
A6: for x holds x in dom g iff x in dom f & f.x in Y and
A7: for x st x in dom g holds g.x = f.x;
now
let x,y be object;
hereby
assume
A8: [x,y] in g;
then
A9: x in dom g by XTUPLE_0:def 12;
reconsider yy=y as set by TARSKI:1;
A10: yy = g.x by A8,Def2,A9
.= f.x by A7,A9;
hence y in Y by A6,A9;
x in dom f by A6,A9;
hence [x,y] in f by A10,Def2;
end;
assume
A11: y in Y;
assume
A12: [x,y] in f;
then
A13: y = f.x by Th1;
x in dom f by A12,XTUPLE_0:def 12;
then
A14: x in dom g by A6,A11,A13;
then y = g.x by A7,A13;
hence [x,y] in g by A14,Def2;
end;
hence thesis by RELAT_1:def 12;
end;
theorem
x in dom(Y|`f) iff x in dom f & f.x in Y by Th52;
theorem
x in dom(Y|`f) implies (Y|`f).x = f.x by Th52;
theorem
dom(Y|`f) c= dom f
by Th52;
theorem
X c= Y implies Y|`(X|`f) = X|`f & X|`(Y|`f) = X|`f by RELAT_1:98,99;
theorem
f is one-to-one implies Y|`f is one-to-one
proof
assume
A1: f is one-to-one;
let x1,x2 such that
A2: x1 in dom(Y|`f) & x2 in dom(Y|`f) and
A3: (Y|`f).x1 = (Y|`f).x2;
A4: x1 in dom f & x2 in dom f by A2,Th52;
(Y|`f).x1 = f.x1 & (Y|`f).x2 = f.x2 by A2,Th52;
hence thesis by A1,A3,A4;
end;
definition
let f,X;
redefine func f.:X means :: redefines .: (RELAT_1, definition)
:Def6:
for y being object holds y in it iff
ex x being object st x in dom f & x in X & y = f.x;
compatibility
proof
let Y;
hereby
assume
A1: Y = f.:X;
let y be object;
hereby
assume y in Y;
then consider x being object such that
A2: [x,y] in f and
A3: x in X by A1,RELAT_1:def 13;
reconsider x as object;
take x;
thus
A4: x in dom f by A2,XTUPLE_0:def 12;
reconsider yy=y as set by TARSKI:1;
thus x in X by A3;
yy = f.x by A2,A4,Def2;
hence y = f.x;
end;
given x being object such that
A5: x in dom f and
A6: x in X and
A7: y = f.x;
[x,y] in f by A5,A7,Def2;
hence y in Y by A1,A6,RELAT_1:def 13;
end;
assume
A8: for y being object holds y in Y iff
ex x being object st x in dom f & x in X & y = f.x;
now
let y be object;
hereby
assume y in Y;
then consider x being object such that
A9: x in dom f and
A10: x in X and
A11: y = f.x by A8;
reconsider x as object;
take x;
thus [x,y] in f by A9,A11,Def2;
thus x in X by A10;
end;
given x being object such that
A12: [x,y] in f and
A13: x in X;
x in dom f & y = f.x by A12,Th1;
hence y in Y by A8,A13;
end;
hence thesis by RELAT_1:def 13;
end;
end;
theorem Th58:
x in dom f implies Im(f,x) = {f.x}
proof
assume
A1: x in dom f;
for y being object holds y in f.:{x} iff y in {f.x}
proof let y be object;
thus y in f.:{x} implies y in {f.x}
proof
assume y in f.:{x};
then consider z being object such that
z in dom f and
A2: z in {x} and
A3: y = f.z by Def6;
z = x by A2,TARSKI:def 1;
hence thesis by A3,TARSKI:def 1;
end;
assume y in {f.x};
then
A4: y = f.x by TARSKI:def 1;
x in {x} by TARSKI:def 1;
hence thesis by A1,A4,Def6;
end;
hence thesis by TARSKI:2;
end;
theorem
x1 in dom f & x2 in dom f implies f.:{x1,x2} = {f.x1,f.x2}
proof
assume
A1: x1 in dom f & x2 in dom f;
for y be object holds y in f.:{x1,x2} iff y = f.x1 or y = f.x2
proof
let y be object;
A2: x1 in {x1,x2} & x2 in {x1,x2} by TARSKI:def 2;
thus y in f.:{x1,x2} implies y = f.x1 or y = f.x2
proof
assume y in f.:{x1,x2};
then ex x being object st x in dom f & x in {x1,x2} & y = f.x by Def6;
hence thesis by TARSKI:def 2;
end;
assume y = f.x1 or y = f.x2;
hence thesis by A1,A2,Def6;
end;
hence thesis by TARSKI:def 2;
end;
theorem
(Y|`f).:X c= f.:X
proof
let y be object;
assume y in (Y|`f).:X;
then consider x being object such that
A1: x in dom(Y|`f) and
A2: x in X and
A3: y = (Y|`f).x by Def6;
y = f.x & x in dom f by A1,A3,Th52;
hence thesis by A2,Def6;
end;
theorem Th61:
f is one-to-one implies f.:(X1 /\ X2) = f.:X1 /\ f.:X2
proof
assume
A1: f is one-to-one;
A2: f.:X1 /\ f.:X2 c= f.:(X1 /\ X2)
proof
let y be object;
assume
A3: y in f.:X1 /\ f.:X2;
then y in f.:X1 by XBOOLE_0:def 4;
then consider x1 being object such that
A4: x1 in dom f and
A5: x1 in X1 and
A6: y = f.x1 by Def6;
y in f.:X2 by A3,XBOOLE_0:def 4;
then consider x2 being object such that
A7: x2 in dom f and
A8: x2 in X2 and
A9: y = f.x2 by Def6;
x1 = x2 by A1,A4,A6,A7,A9;
then x1 in X1 /\ X2 by A5,A8,XBOOLE_0:def 4;
hence thesis by A4,A6,Def6;
end;
f.:(X1 /\ X2)c=f.:X1 /\ f.:X2 by RELAT_1:121;
hence thesis by A2;
end;
theorem
(for X1,X2 holds f.:(X1 /\ X2) = f.:X1 /\ f.:X2) implies f is one-to-one
proof
assume
A1: for X1,X2 holds f.:(X1 /\ X2) = f.:X1 /\ f.:X2;
given x1,x2 such that
A2: x1 in dom f & x2 in dom f and
A3: f.x1 = f.x2 and
A4: x1 <> x2;
A5: f.:({x1}/\{x2}) = f.:{x1}/\f.: {x2} by A1;
{x1} misses {x2} by A4,ZFMISC_1:11;
then
A6: {x1} /\ {x2} = {};
Im(f,x1) = {f.x1} & Im(f,x2) = {f.x2} by A2,Th58;
hence contradiction by A3,A6,A5;
end;
theorem
f is one-to-one implies f.:(X1 \ X2) = f.:X1 \ f.:X2
proof
assume
A1: f is one-to-one;
A2: f.:(X1 \ X2) c= f.:X1 \ f.:X2
proof
let y be object;
assume y in f.:(X1\X2);
then consider x being object such that
A3: x in dom f and
A4: x in X1\X2 and
A5: y = f.x by Def6;
A6: not x in X2 by A4,XBOOLE_0:def 5;
A7: now
assume y in f.:X2;
then ex z being object st z in dom f & z in X2 & y = f.z by Def6;
hence contradiction by A1,A3,A5,A6;
end;
y in f.:X1 by A3,A4,A5,Def6;
hence thesis by A7,XBOOLE_0:def 5;
end;
f.:X1 \ f.: X2 c= f.:(X1 \ X2) by RELAT_1:122;
hence thesis by A2;
end;
theorem
(for X1,X2 holds f.:(X1 \ X2) = f.:X1 \ f.:X2) implies f is one-to-one
proof
assume
A1: for X1,X2 holds f.:(X1 \ X2) = f.:X1 \ f.:X2;
given x1,x2 such that
A2: x1 in dom f & x2 in dom f and
A3: f.x1 = f.x2 and
A4: x1 <> x2;
A5: f.:({x1}\{x2}) = f.:{x1} by A4,ZFMISC_1:14;
A6: f.:({x1}\{x2}) = f.:{x1}\f.:{x2} by A1;
Im(f,x1) = {f.x1} & Im(f,x2) = {f.x2} by A2,Th58;
hence contradiction by A3,A5,A6,XBOOLE_1:37;
end;
theorem
X misses Y & f is one-to-one implies f.:X misses f.:Y
proof
assume X /\ Y = {} & f is one-to-one;
then f.:(X /\ Y) = {} & f.:(X /\ Y) = f.:X /\ f.:Y by Th61;
hence thesis;
end;
theorem
(Y|`f).:X = Y /\ f.:X
proof
for y being object holds y in (Y|`f).:X iff y in Y /\ f.:X
proof let y be object;
thus y in (Y|`f).:X implies y in Y /\ f.:X
proof
assume y in (Y|`f).:X;
then consider x being object such that
A1: x in dom(Y|`f) and
A2: x in X and
A3: y = (Y|`f).x by Def6;
A4: y = f.x by A1,A3,Th52;
then
A5: y in Y by A1,Th52;
x in dom f by A1,Th52;
then y in f.:X by A2,A4,Def6;
hence thesis by A5,XBOOLE_0:def 4;
end;
assume
A6: y in Y /\ f.:X;
then y in f.:X by XBOOLE_0:def 4;
then consider x being object such that
A7: x in dom f and
A8: x in X and
A9: y = f.x by Def6;
y in Y by A6,XBOOLE_0:def 4;
then
A10: x in dom(Y|`f) by A7,A9,Th52;
then (Y|`f).x = f.x by Th52;
hence thesis by A8,A9,A10,Def6;
end;
hence thesis by TARSKI:2;
end;
definition
let f,Y;
redefine func f"Y means :: redefines " (RELAT_1, definition)
:Def7:
for x holds x in it iff x in dom f & f.x in Y;
compatibility
proof
let X;
hereby
assume
A1: X = f"Y;
let x;
hereby
assume x in X;
then
A2: ex y being object st [x,y] in f & y in Y by A1,RELAT_1:def 14;
hence x in dom f by XTUPLE_0:def 12;
thus f.x in Y by A2,Th1;
end;
assume that
A3: x in dom f and
A4: f.x in Y;
[x,f.x] in f by A3,Th1;
hence x in X by A1,A4,RELAT_1:def 14;
end;
assume
A5: for x holds x in X iff x in dom f & f.x in Y;
now
let x be object;
hereby
assume
A6: x in X;
reconsider y = f.x as object;
take y;
x in dom f by A5,A6;
hence [x,y] in f by Def2;
thus y in Y by A5,A6;
end;
given y being object such that
A7: [x,y] in f and
A8: y in Y;
x in dom f & y = f.x by A7,Th1;
hence x in X by A5,A8;
end;
hence thesis by RELAT_1:def 14;
end;
end;
theorem Th67:
f"(Y1 /\ Y2) = f"Y1 /\ f"Y2
proof
for x being object holds x in f"(Y1 /\ Y2) iff x in f"Y1 /\ f"Y2
proof let x be object;
reconsider x as set by TARSKI:1;
A1: x in f"Y2 iff f.x in Y2 & x in dom f by Def7;
A2: x in f"(Y1 /\ Y2) iff f.x in Y1 /\ Y2 & x in dom f by Def7;
x in f"Y1 iff f.x in Y1 & x in dom f by Def7;
then x in f"(Y1 /\ Y2) iff x in f"Y1 /\ f"Y2 by A1,A2,XBOOLE_0:def 4;
hence thesis;
end;
hence thesis by TARSKI:2;
end;
theorem
f"(Y1 \ Y2) = f"Y1 \ f"Y2
proof
for x being object holds x in f"(Y1 \ Y2) iff x in f"Y1 \ f"Y2
proof let x be object;
A1: x in f"Y2 iff f.x in Y2 & x in dom f by Def7;
A2: x in f"(Y1 \ Y2) iff f.x in Y1 \ Y2 & x in dom f by Def7;
x in f"Y1 iff f.x in Y1 & x in dom f by Def7;
hence thesis by A1,A2,XBOOLE_0:def 5;
end;
hence thesis by TARSKI:2;
end;
theorem
(R|X)"Y = X /\ (R"Y)
proof
hereby
let x be object;
assume x in (R|X)"Y;
then
A1: ex y being object st [x,y] in R|X & y in Y by RELAT_1:def 14;
then
A2: x in X by RELAT_1:def 11;
R|X c= R by RELAT_1:59;
then x in R"Y by A1,RELAT_1:def 14;
hence x in X /\ (R"Y) by A2,XBOOLE_0:def 4;
end;
let x be object;
assume
A3: x in X /\ (R"Y);
then x in R"Y by XBOOLE_0:def 4;
then consider y being object such that
A4: [x,y] in R and
A5: y in Y by RELAT_1:def 14;
x in X by A3,XBOOLE_0:def 4;
then [x,y] in R|X by A4,RELAT_1:def 11;
hence thesis by A5,RELAT_1:def 14;
end;
theorem
for f being Function, A,B being set st A misses B holds f"A misses f"B
proof
let f be Function, A,B be set;
assume A misses B;
then A /\ B = {};
then {} = f"(A /\ B)
.= f"A /\ f"B by Th67;
hence thesis;
end;
theorem Th71:
y in rng R iff R"{y} <> {}
proof
thus y in rng R implies R"{y} <> {}
proof
assume y in rng R;
then
A1: ex x being object st [x,y] in R by XTUPLE_0:def 13;
y in {y} by TARSKI:def 1;
hence thesis by A1,RELAT_1:def 14;
end;
assume R"{y} <> {};
then consider x being object such that
A2: x in R"{y} by XBOOLE_0:def 1;
consider z being object such that
A3: [x,z] in R and
A4: z in {y} by A2,RELAT_1:def 14;
z = y by A4,TARSKI:def 1;
hence thesis by A3,XTUPLE_0:def 13;
end;
theorem
(for y st y in Y holds R"{y} <> {}) implies Y c= rng R
proof
assume
A1: for y st y in Y holds R"{y} <> {};
let y be object;
assume y in Y;
then R"{y} <> {} by A1;
hence thesis by Th71;
end;
theorem Th73:
(for y st y in rng f ex x st f"{y} = {x}) iff f is one-to-one
proof
thus (for y st y in rng f ex x st f"{y} = {x}) implies f is one-to-one
proof
assume
A1: for y st y in rng f ex x st f"{y} = {x};
let x1,x2;
assume that
A2: x1 in dom f and
A3: x2 in dom f;
f.x1 in rng f by A2,Def3;
then consider y1 such that
A4: f"{f.x1} = {y1} by A1;
f.x2 in rng f by A3,Def3;
then consider y2 such that
A5: f"{f.x2} = {y2} by A1;
f.x1 in {f.x1} by TARSKI:def 1;
then x1 in {y1} by A2,A4,Def7;
then
A6: y1 = x1 by TARSKI:def 1;
f.x2 in {f.x2} by TARSKI:def 1;
then x2 in {y2} by A3,A5,Def7;
hence thesis by A4,A5,A6,TARSKI:def 1;
end;
assume
A7: f is one-to-one;
let y;
assume y in rng f;
then consider x being object such that
A8: x in dom f & y = f.x by Def3;
take x;
for z being object holds z in f"{y} iff z = x
proof
let z be object;
thus z in f"{y} implies z = x
proof
assume
A9: z in f"{y};
then f.z in {y} by Def7;
then
A10: f.z = y by TARSKI:def 1;
z in dom f by A9,Def7;
hence thesis by A7,A8,A10;
end;
y in {y} by TARSKI:def 1;
hence thesis by A8,Def7;
end;
hence thesis by TARSKI:def 1;
end;
theorem Th74:
f.:(f"Y) c= Y
proof
let y be object;
assume y in f.:(f"Y);
then ex x being object st x in dom f & x in f"Y & y = f.x by Def6;
hence thesis by Def7;
end;
theorem Th75:
X c= dom R implies X c= R"(R.:X)
proof
assume
A1: X c= dom R;
let x be object;
assume
A2: x in X;
then consider Rx being object such that
A3: [x,Rx] in R by A1,XTUPLE_0:def 12;
Rx in R.:X by A2,A3,RELAT_1:def 13;
hence thesis by A3,RELAT_1:def 14;
end;
theorem
Y c= rng f implies f.:(f"Y) = Y
proof
assume
A1: Y c= rng f;
thus f.:(f"Y) c= Y by Th74;
let y be object;
assume
A2: y in Y;
then consider x being object such that
A3: x in dom f & y = f.x by A1,Def3;
x in f"Y by A2,A3,Def7;
hence thesis by A3,Def6;
end;
theorem
f.:(f"Y) = Y /\ f.:(dom f)
proof
f.:(f"Y) c= Y & f.:(f"(Y)) c= f.:(dom f) by Th74,RELAT_1:114;
hence f.:(f"Y) c= Y /\ f.:(dom f) by XBOOLE_1:19;
let y be object;
assume
A1: y in Y /\ f.:(dom f);
then y in f.:(dom f) by XBOOLE_0:def 4;
then consider x being object such that
A2: x in dom f and
x in dom f and
A3: y = f.x by Def6;
y in Y by A1,XBOOLE_0:def 4;
then x in f"Y by A2,A3,Def7;
hence thesis by A2,A3,Def6;
end;
theorem Th78:
f.:(X /\ f"Y) c= (f.:X) /\ Y
proof
let y be object;
assume y in f.:(X /\ f"Y);
then consider x being object such that
A1: x in dom f and
A2: x in X /\ f"Y and
A3: y = f.x by Def6;
x in f"Y by A2,XBOOLE_0:def 4;
then
A4: y in Y by A3,Def7;
x in X by A2,XBOOLE_0:def 4;
then y in f.:X by A1,A3,Def6;
hence thesis by A4,XBOOLE_0:def 4;
end;
theorem
f.:(X /\ f"Y) = (f.:X) /\ Y
proof
thus f.:(X /\ f"Y)c=(f.:X) /\ Y by Th78;
let y be object;
assume
A1: y in (f.:X) /\ Y;
then y in f.:X by XBOOLE_0:def 4;
then consider x being object such that
A2: x in dom f and
A3: x in X and
A4: y = f.x by Def6;
y in Y by A1,XBOOLE_0:def 4;
then x in f"Y by A2,A4,Def7;
then x in X /\ f"Y by A3,XBOOLE_0:def 4;
hence thesis by A2,A4,Def6;
end;
theorem
X /\ R"Y c= R"(R.:X /\ Y)
proof
let x be object;
assume
A1: x in X /\ R"Y;
then x in R"Y by XBOOLE_0:def 4;
then consider Rx being object such that
A2: [x,Rx] in R and
A3: Rx in Y by RELAT_1:def 14;
x in X by A1,XBOOLE_0:def 4;
then Rx in R.:X by A2,RELAT_1:def 13;
then Rx in R.:X /\ Y by A3,XBOOLE_0:def 4;
hence thesis by A2,RELAT_1:def 14;
end;
theorem Th81:
f is one-to-one implies f"(f.:X) c= X
proof
assume
A1: f is one-to-one;
let x be object;
assume
A2: x in f"(f.:X);
then f.x in f.:X by Def7;
then
A3: ex z being object st z in dom f & z in X & f.x = f.z by Def6;
x in dom f by A2,Def7;
hence thesis by A1,A3;
end;
theorem
(for X holds f"(f.:X) c= X) implies f is one-to-one
proof
assume
A1: for X holds f"(f.:X) c= X;
given x1,x2 such that
A2: x1 in dom f and
A3: x2 in dom f and
A4: f.x1 = f.x2 & x1 <> x2;
A5: f"(f.:{x1}) c= {x1} by A1;
A6: Im(f,x2) = {f.x2} by A3,Th58;
A7: Im(f,x1) = {f.x1} by A2,Th58;
f.x1 in rng f by A2,Def3;
then f"(f.:{x1}) <> {} by A7,Th71;
then f"(f.:{x1}) = {x1} by A5,ZFMISC_1:33;
hence contradiction by A1,A4,A7,A6,ZFMISC_1:3;
end;
theorem
f is one-to-one implies f.:X = (f")"X
proof
assume
A1: f is one-to-one;
for y being object holds y in f.:X iff y in (f")"X
proof let y be object;
thus y in f.:X implies y in (f")"X
proof
assume y in f.:X;
then consider x being object such that
A2: x in dom f and
A3: x in X and
A4: y = f.x by Def6;
y in rng f by A2,A4,Def3;
then
A5: y in dom(f") by A1,Th31;
(f").(f.x) = x by A1,A2,Th31;
hence thesis by A3,A4,A5,Def7;
end;
assume
A6: y in (f")"X;
then
A7: (f").y in X by Def7;
y in dom(f") by A6,Def7;
then y in rng(f) by A1,Th31;
then consider x being object such that
A8: x in dom(f) & y = f.x by Def3;
(f").y = x by A1,A8,Th33;
hence thesis by A7,A8,Def6;
end;
hence thesis by TARSKI:2;
end;
theorem
f is one-to-one implies f"Y = (f").:Y
proof
assume
A1: f is one-to-one;
for x being object holds x in f"Y iff x in (f").:Y
proof let x be object;
thus x in f"Y implies x in (f").:Y
proof
assume
A2: x in f"Y;
then
A3: f.x in Y by Def7;
A4: x in dom f by A2,Def7;
then f.x in rng(f) by Def3;
then
A5: f.x in dom(f") by A1,Th31;
(f").(f.x) = x by A1,A4,Th31;
hence thesis by A3,A5,Def6;
end;
assume x in (f").:Y;
then consider y being object such that
A6: y in dom(f") and
A7: y in Y and
A8: x = (f").y by Def6;
dom(f") = rng f by A1,Th31;
then y = f.x & x in dom f by A1,A6,A8,Th31;
hence thesis by A7,Def7;
end;
hence thesis by TARSKI:2;
end;
:: SUPLEMENT
theorem
Y = rng f & dom g = Y & dom h = Y & g*f = h*f implies g = h
proof
assume that
A1: Y = rng f and
A2: dom g = Y & dom h = Y and
A3: g*f = h*f;
y in Y implies g.y = h.y
proof
assume y in Y;
then consider x being object such that
A4: x in dom f & y = f.x by A1,Def3;
(g*f).x = g.y by A4,Th13;
hence thesis by A3,A4,Th13;
end;
hence thesis by A2,Th2;
end;
theorem
f.:X1 c= f.:X2 & X1 c= dom f & f is one-to-one implies X1 c= X2
proof
assume that
A1: f.:X1 c= f.:X2 and
A2: X1 c= dom f and
A3: f is one-to-one;
let x be object;
assume
A4: x in X1;
then f.x in f.:X1 by A2,Def6;
then ex x2 being object st x2 in dom f & x2 in X2 & f.x = f.x2 by A1,Def6;
hence thesis by A2,A3,A4;
end;
theorem Th87:
f"Y1 c= f"Y2 & Y1 c= rng f implies Y1 c= Y2
proof
assume that
A1: f"Y1 c= f"Y2 and
A2: Y1 c= rng f;
let y be object;
assume
A3: y in Y1;
then consider x being object such that
A4: x in dom f and
A5: y = f.x by A2,Def3;
x in f"Y1 by A3,A4,A5,Def7;
hence thesis by A1,A5,Def7;
end;
theorem
f is one-to-one iff for y ex x st f"{y} c= {x}
proof
(for y ex x st f"{y} c= {x}) iff for y st y in rng f ex x st f"{y} = {x}
proof
thus (for y ex x st f"{y} c= {x}) implies for y st y in rng f ex x st f"{y
} = {x}
proof
assume
A1: for y ex x st f"{y} c= {x};
let y;
consider x such that
A2: f"{y} c= {x} by A1;
assume y in rng f;
then consider x1 being object such that
A3: x1 in dom f and
A4: y = f.x1 by Def3;
take x;
f.x1 in {y} by A4,TARSKI:def 1;
then f"{y} <> {} by A3,Def7;
hence thesis by A2,ZFMISC_1:33;
end;
assume
A5: for y st y in rng f ex x st f"{y} = {x};
let y;
A6: now
set x = the set;
assume
A7: not y in rng f;
take x;
rng f misses {y} by A7,ZFMISC_1:50;
then f"{y} = {} by RELAT_1:138;
hence f"{y} c= {x};
end;
now
assume y in rng f;
then consider x such that
A8: f"{y} = {x} by A5;
take x;
thus f"{y} c= {x} by A8;
end;
hence thesis by A6;
end;
hence thesis by Th73;
end;
theorem
rng R c= dom S implies R"X c= (R*S)"(S.:X)
proof
assume
A1: rng R c= dom S;
let x be object;
assume x in R"X;
then consider Rx being object such that
A2: [x,Rx] in R and
A3: Rx in X by RELAT_1:def 14;
Rx in rng R by A2,XTUPLE_0:def 13;
then consider SRx being object such that
A4: [Rx,SRx] in S by A1,XTUPLE_0:def 12;
SRx in S.:X & [x,SRx] in R*S by A2,A3,A4,RELAT_1:def 8,def 13;
hence thesis by RELAT_1:def 14;
end;
theorem
for f being Function st f " X = f " Y & X c= rng f & Y c= rng f holds X = Y
by Th87;
begin :: Addenda
:: from BORSUK_1
reserve e,u for object,
A for Subset of X;
theorem
(id X).:A = A
proof
now
let e be object;
thus e in A implies
ex u being object st u in dom id X & u in A & e = (id X).u
proof
assume
A1: e in A;
take e;
thus e in dom id X by A1;
thus e in A by A1;
thus thesis by A1,Th17;
end;
assume ex u being object st u in dom id X & u in A & e = (id X).u;
hence e in A by Th17;
end;
hence thesis by Def6;
end;
:: from PBOOLE
definition
let f be Function;
redefine attr f is empty-yielding means :: redefines empty-yielding (RELAT_1, definition)
:Def8: for x st x in dom f holds f.x is empty;
compatibility
proof
hereby
assume
A1: f is empty-yielding;
let x;
assume x in dom f;
then f.x in rng f by Def3;
hence f.x is empty by A1,RELAT_1:149;
end;
assume
A2: for x st x in dom f holds f.x is empty;
let s be object;
assume s in rng f;
then ex e being object st e in dom f & s = f.e by Def3;
then s = {} by A2;
hence thesis by TARSKI:def 1;
end;
end;
:: from UNIALG_1
definition
let F be Function;
redefine attr F is non-empty means :: redefines non-empty (RELAT_1, definition)
:Def9:
for n being object st n in dom F holds F.n is non empty;
compatibility
proof
thus F is non-empty implies
for n being object st n in dom F holds F.n is non empty by Def3;
assume
A1: for n being object st n in dom F holds F.n is non empty;
assume {} in rng F;
then ex i being object st i in dom F & F.i = {} by Def3;
hence contradiction by A1;
end;
end;
:: new, 2004.08.04
registration
cluster non-empty for Function;
existence
proof
take {};
let x be object;
thus thesis;
end;
end;
:: from MSUALG_2
scheme
LambdaB { D()->non empty set, F(object)->object } :
ex f be Function st dom f = D() & for d be Element of D() holds f.d = F(d)
proof
consider f be Function such that
A1: dom f = D() & for d be object st d in D() holds f.d = F(d) from Lambda;
take f;
thus thesis by A1;
end;
:: from PUA2MSS1, 2005.08.22, A.T.
registration
let f be non-empty Function;
cluster rng f -> with_non-empty_elements;
coherence
proof
assume {} in rng f;
then ex x being object st x in dom f & {} = f.x by Def3;
hence thesis by Def9;
end;
end;
:: from SEQM_3, 2005.12.17, A.T.
definition
let f be Function;
attr f is constant means
:Def10:
x in dom f & y in dom f implies f.x = f.y;
end;
theorem
for A,B being set, f being Function st A c= dom f & f.:A c= B holds A c= f"B
proof
let A,B be set, f being Function;
assume A c= dom f;
then
A1: A c= f"(f.:A) by Th75;
assume f.:A c= B;
then f"(f.:A) c= f"B by RELAT_1:143;
hence thesis by A1;
end;
:: moved from MSAFREE3:1, AG 1.04.2006
theorem
for f being Function st X c= dom f & f is one-to-one holds f"(f.:X) = X
proof
let f be Function such that
A1: X c= dom f and
A2: f is one-to-one;
thus f"(f.:X) c= X by A2,Th81;
let x be object;
assume
A3: x in X;
then f.x in f.:X by A1,Def6;
hence thesis by A1,A3,Def7;
end;
:: added, AK 5.02.2007
definition
let f,g;
redefine pred f = g means :: redefines = (RELAT_1, redefinition) → = (XBOOLE_0, redefinition) → = (HIDDEN, definition)
dom f = dom g & for x st x in dom f holds f.x = g.x;
compatibility by Th2;
end;
:: missing, 2007.03.09, A.T.
registration
cluster non-empty non empty for Function;
existence
proof
consider f such that
A1: dom f = {{}} and
A2: rng f = {{{}}} by Th5;
take f;
not {} in rng f by A2,TARSKI:def 1;
hence f is non-empty;
thus thesis by A1;
end;
end;
:: from PRVECT_1, 2007.03.09, A.T.
registration
let a be non-empty non empty Function;
let i be Element of dom a;
cluster a.i -> non empty;
coherence
proof
a.i in rng a by Def3;
hence thesis by RELAT_1:def 9;
end;
end;
:: missing, 2007.04.13, A.T.
registration
let f be Function;
cluster -> Function-like for Subset of f;
coherence
by Def1;
end;
:: from SCMFSA6A, 2007.07.23, A.T.
theorem
for f,g being Function, D being set st D c= dom f & D c= dom g holds f
| D = g | D iff for x being set st x in D holds f.x = g.x
proof
let f,g be Function;
let D be set;
assume that
A1: D c= dom f and
A2: D c= dom g;
A3: dom (g | D) = dom g /\ D by RELAT_1:61
.= D by A2,XBOOLE_1:28;
hereby
assume
A4: f | D = g | D;
hereby
let x be set;
assume
A5: x in D;
hence f.x = (g | D).x by A4,Th48
.= g.x by A5,Th48;
end;
end;
assume
A6: for x being set st x in D holds f.x = g.x;
A7: now
let x be object;
assume
A8: x in D;
hence (f | D).x = f.x by Th48
.= g.x by A6,A8
.= (g | D).x by A8,Th48;
end;
dom (f | D) = dom f /\ D by RELAT_1:61
.= D by A1,XBOOLE_1:28;
hence thesis by A3,A7;
end;
:: from SCMBSORT, 2007.07.26, A.T.
theorem
for f,g being Function, X being set st dom f = dom g & (for x being
set st x in X holds f.x = g.x) holds f|X = g|X
proof
let f,g be Function, X be set such that
A1: dom f = dom g and
A2: for x being set st x in X holds f.x = g.x;
A3: dom (f|X) =dom f /\ X by RELAT_1:61;
then
A4: dom (f|X) = dom (g|X) by A1,RELAT_1:61;
now
let x be object;
assume
A5: x in dom (f|X);
then
A6: x in X by A3,XBOOLE_0:def 4;
(f|X).x = f.x & (g|X).x = g.x by A4,A5,Th46;
hence (f|X).x = (g|X).x by A2,A6;
end;
hence thesis by A4;
end;
:: missing, 2007.10.28, A.T.
theorem Th96:
rng(f|{X}) c= {f.X}
proof
let x be object;
assume x in rng(f|{X});
then consider y being object such that
A1: y in dom(f|{X}) and
A2: x = (f|{X}).y by Def3;
dom(f|{X}) c= {X} by RELAT_1:58;
then y = X by A1,TARSKI:def 1;
then x = f.X by A1,A2,Th46;
hence thesis by TARSKI:def 1;
end;
theorem
X in dom f implies rng(f|{X}) ={f.X}
proof
A1: X in {X} by TARSKI:def 1;
assume X in dom f;
then
A2: X in dom(f|{X}) by A1,RELAT_1:57;
thus rng(f|{X}) c= {f.X} by Th96;
let x be object;
assume x in {f.X};
then x = f.X by TARSKI:def 1;
then x = (f|{X}).X by A2,Th46;
hence thesis by A2,Def3;
end;
:: from RFUNCT_1, 2008.09.04, A.T.
registration
cluster empty -> constant for Function;
coherence;
end;
:: from WAYBEL35, 2008.08.04, A.T.
registration
let f be constant Function;
cluster rng f -> trivial;
coherence
proof
per cases;
suppose
f is empty;
then reconsider g = f as empty Function;
rng g is empty;
hence thesis;
end;
suppose
f <> {};
then consider x being object such that
A1: x in dom f by XBOOLE_0:def 1;
for y being object holds y in {f.x}
iff ex z being object st z in dom f & y = f.z
proof
let y be object;
hereby
assume
A2: y in {f.x};
reconsider x as object;
take x;
thus x in dom f & y = f.x by A1,A2,TARSKI:def 1;
end;
given z being object such that
A3: z in dom f & y = f.z;
y = f.x by A1,A3,Def10;
hence thesis by TARSKI:def 1;
end;
hence thesis by Def3;
end;
end;
end;
registration
cluster non constant for Function;
existence
proof
set f = {[{},{}],[{{}},{{}}]};
f is Function-like
proof
let x,y,z be object;
assume that
A1: [x,y] in f and
A2: [x,z] in f;
[x,y] = [{},{}] or [x,y] =[{{}},{{}}] by A1,TARSKI:def 2;
then
A3: x = {} & y = {} or x = {{}} & y = {{}} by XTUPLE_0:1;
[x,z] = [{},{}] or [x,z] =[{{}},{{}}] by A2,TARSKI:def 2;
hence thesis by A3,XTUPLE_0:1;
end;
then reconsider f as Function;
take f, {}, {{}};
A4: [{{}},{{}}] in f by TARSKI:def 2;
A5: [{},{}] in f by TARSKI:def 2;
hence
A6: {} in dom f & {{}} in dom f by A4,XTUPLE_0:def 12;
then f.{} = {} by A5,Def2;
hence thesis by A4,A6,Def2;
end;
end;
registration
let f be non constant Function;
cluster rng f -> non trivial;
coherence
proof
assume
A1: rng f is trivial;
per cases;
suppose
rng f is empty;
then reconsider f as empty Function;
f is trivial;
hence thesis;
end;
suppose
rng f is non empty;
then consider x being object such that
A2: x in rng f;
f is constant
proof
let y,z be object;
assume that
A3: y in dom f and
A4: z in dom f;
A5: f.z in rng f by A4,Def3;
f.y in rng f by A3,Def3;
hence f.y = x by A1,A2
.= f.z by A1,A2,A5;
end;
hence thesis;
end;
end;
end;
registration
cluster non constant -> non trivial for Function;
coherence
proof
let f be Function;
assume f is non constant;
then consider n1,n2 being object such that
A1: n1 in dom f and
A2: n2 in dom f and
A3: f.n1 <> f.n2;
reconsider f as non empty Function by A1;
f is non trivial
proof
reconsider x = [n1,f.n1], y = [n2,f.n2] as Element of f by A1,A2,Th1;
take x,y;
thus x in f & y in f;
thus thesis by A3,XTUPLE_0:1;
end;
hence thesis;
end;
end;
registration
cluster trivial -> constant for Function;
coherence;
end;
:: from RFUNCT_2, 2008.09.14, A.T.
theorem
for F,G be Function, X holds (G|(F.:X))*(F|X) = (G*F)|X
proof
let F,G be Function,X;
set Y = dom ((G*F)|X);
now
let x be object;
thus x in dom ((G|(F.:X))*(F|X)) implies x in Y
proof
assume
A1: x in dom ((G|(F.:X))*(F|X));
then
A2: x in dom (F|X) by Th11;
then
A3: x in dom F /\ X by RELAT_1:61;
then
A4: x in X by XBOOLE_0:def 4;
(F|X).x in dom (G|(F.:X)) by A1,Th11;
then F.x in dom (G|(F.:X)) by A2,Th46;
then F.x in dom G /\ (F.:X) by RELAT_1:61;
then
A5: F.x in dom G by XBOOLE_0:def 4;
x in dom F by A3,XBOOLE_0:def 4;
then x in dom (G*F) by A5,Th11;
then x in dom (G*F)/\ X by A4,XBOOLE_0:def 4;
hence thesis by RELAT_1:61;
end;
assume x in Y;
then
A6: x in dom (G*F) /\ X by RELAT_1:61;
then
A7: x in dom (G*F) by XBOOLE_0:def 4;
then
A8: F.x in dom G by Th11;
A9: x in X by A6,XBOOLE_0:def 4;
x in dom F by A7,Th11;
then x in dom F /\ X by A9,XBOOLE_0:def 4;
then
A10: x in dom (F|X) by RELAT_1:61;
x in dom F by A7,Th11;
then F.x in F.:X by A9,Def6;
then F.x in dom G /\ (F.:X) by A8,XBOOLE_0:def 4;
then F.x in dom (G|(F.:X)) by RELAT_1:61;
then (F|X).x in dom (G|(F.:X)) by A10,Th46;
hence x in dom ((G|(F.:X))*(F|X)) by A10,Th11;
end;
then
A11: Y = dom ((G|(F.:X))*(F|X)) by TARSKI:2;
now
let x;
assume
A12: x in Y;
then
A13: x in dom (G*F) /\ X by RELAT_1:61;
then x in dom (G*F) by XBOOLE_0:def 4;
then
A14: x in dom F by Th11;
A15: x in X by A13,XBOOLE_0:def 4;
then
A16: F.x in F.:X by A14,Def6;
thus ((G|(F.:X))*(F|X)).x =(G|(F.:X)).((F|X).x) by A11,A12,Th12
.= (G|(F.:X)).(F.x) by A15,Th48
.= G.(F.x) by A16,Th48
.= (G*F).x by A14,Th13
.= ((G*F)|X).x by A13,Th47;
end;
hence thesis by A11;
end;
theorem
for F,G be Function, X,X1 holds (G|X1)*(F|X) = (G*F)|(X /\ (F"X1))
proof
let F,G be Function,X,X1;
set Y = dom ((G|X1)*(F|X));
now
let x be object;
thus x in dom ((G*F)|(X /\ (F"X1))) implies x in Y
proof
assume x in dom ((G*F)|(X /\ (F"X1)));
then
A1: x in dom (G*F) /\ (X /\ (F"X1)) by RELAT_1:61;
then
A2: x in dom (G*F) by XBOOLE_0:def 4;
A3: x in X /\ (F"X1) by A1,XBOOLE_0:def 4;
then
A4: x in X by XBOOLE_0:def 4;
x in dom F by A2,Th11;
then x in dom F /\ X by A4,XBOOLE_0:def 4;
then
A5: x in dom (F|X) by RELAT_1:61;
x in (F"X1) by A3,XBOOLE_0:def 4;
then
A6: F.x in X1 by Def7;
F.x in dom G by A2,Th11;
then F.x in dom G /\ X1 by A6,XBOOLE_0:def 4;
then F.x in dom (G|X1) by RELAT_1:61;
then (F|X).x in dom (G|X1) by A5,Th46;
hence thesis by A5,Th11;
end;
assume
A7: x in Y;
then
A8: x in dom(F|X) by Th11;
then
A9: x in dom F /\ X by RELAT_1:61;
then
A10: x in dom F by XBOOLE_0:def 4;
A11: x in X by A9,XBOOLE_0:def 4;
(F|X).x in dom(G|X1) by A7,Th11;
then F.x in dom (G|X1) by A8,Th46;
then
A12: F.x in dom G /\ X1 by RELAT_1:61;
then F.x in X1 by XBOOLE_0:def 4;
then x in F"X1 by A10,Def7;
then
A13: x in X /\ F"X1 by A11,XBOOLE_0:def 4;
F.x in dom G by A12,XBOOLE_0:def 4;
then x in dom (G*F) by A10,Th11;
then x in dom (G*F) /\ (X/\(F"X1)) by A13,XBOOLE_0:def 4;
hence x in dom ((G*F)|(X /\ (F"X1))) by RELAT_1:61;
end;
then
A14: Y = dom ((G*F)|(X /\ (F"X1))) by TARSKI:2;
now
let x;
assume
A15: x in Y;
then
A16: x in dom (F|X) by Th11;
then
A17: x in dom F /\ X by RELAT_1:61;
then
A18: x in dom F by XBOOLE_0:def 4;
A19: (F|X).x in dom (G|X1) by A15,Th11;
then
A20: F.x in dom (G|X1) by A16,Th46;
A21: x in X by A17,XBOOLE_0:def 4;
F.x in dom (G|X1) by A16,A19,Th46;
then F.x in dom G /\ X1 by RELAT_1:61;
then F.x in X1 by XBOOLE_0:def 4;
then x in F"X1 by A18,Def7;
then
A22: x in X /\ F"X1 by A21,XBOOLE_0:def 4;
thus ((G|X1)*(F|X)).x =(G|X1).((F|X).x) by A15,Th12
.= (G|X1).(F.x) by A16,Th46
.= G.(F.x) by A20,Th46
.= (G*F).x by A18,Th13
.= ((G*F)|(X/\(F"X1))).x by A22,Th48;
end;
hence thesis by A14;
end;
theorem
for F,G be Function,X holds X c= dom (G*F) iff X c= dom F & F.:X c= dom G
proof
let F,G be Function,X;
thus X c= dom (G*F) implies X c= dom F & F.:X c= dom G
proof
assume
A1: X c= dom (G*F);
then for x being object st x in X holds x in dom F by Th11;
hence X c= dom F;
let x be object;
assume x in F.:X;
then ex y being object st y in dom F & y in X & x=F.y by Def6;
hence thesis by A1,Th11;
end;
assume that
A2: X c= dom F and
A3: F.:X c= dom G;
let x be object;
assume
A4: x in X;
then F.x in F.:X by A2,Def6;
hence thesis by A2,A3,A4,Th11;
end;
:: from YELLOW_6, 2008.12.26, A.T.
definition
let f be Function;
assume
A1: f is non empty constant;
func the_value_of f -> object means
ex x being set st x in dom f & it = f.x;
existence
proof
consider x1 being object such that
A2: x1 in dom f by A1,XBOOLE_0:def 1;
take f.x1;
thus thesis by A2;
end;
uniqueness by A1;
end;
:: from QC_LANG4, 2009.01.23, A.T
registration
let X,Y;
cluster X-defined Y-valued for Function;
existence
proof
take {};
thus dom{} c= X & rng{} c= Y;
end;
end;
theorem
for X being set, f being X-valued Function for x being set st x in dom
f holds f.x in X
proof
let X be set, f be X-valued Function;
let x be set;
assume x in dom f;
then
A1: f.x in rng f by Def3;
rng f c= X by RELAT_1:def 19;
hence thesis by A1;
end;
:: from FRAENKEL, 2009.05.06, A.K.
definition
let IT be set;
attr IT is functional means
:Def13:
for x being object st x in IT holds x is Function;
end;
registration
cluster empty -> functional for set;
coherence;
let f be Function;
cluster { f } -> functional;
coherence
by TARSKI:def 1;
let g be Function;
cluster { f,g } -> functional;
coherence
by TARSKI:def 2;
end;
registration
cluster non empty functional for set;
existence
proof
take { {} };
thus thesis;
end;
end;
registration
let P be functional set;
cluster -> Function-like Relation-like for Element of P;
coherence
proof
let x be Element of P;
per cases;
suppose
P is empty;
hence thesis by SUBSET_1:def 1;
end;
suppose
P is non empty;
hence thesis by Def13;
end;
end;
end;
registration
let A be functional set;
cluster -> functional for Subset of A;
coherence;
end;
:: new, 2009.09.30, A.T.
definition let g,f be Function;
attr f is g-compatible means
:Def14: x in dom f implies f.x in g.x;
end;
theorem
f is g-compatible & dom f = dom g implies g is non-empty;
theorem
{} is f-compatible;
registration
let I be set, f be Function;
cluster empty I-defined f-compatible for Function;
existence
proof
take {};
thus thesis by RELAT_1:171;
end;
end;
registration let X be set;
let f be Function, g be f-compatible Function;
cluster g|X -> f-compatible;
coherence
proof let x;
A1: dom(g|X) c= dom g by RELAT_1:60;
assume
A2: x in dom(g|X);
then g.x in f.x by A1,Def14;
hence (g|X).x in f.x by A2,Th46;
end;
end;
registration let I be set;
cluster non-empty I-defined for Function;
existence
proof
take {};
thus {} is non-empty;
thus dom {} c= I;
end;
end;
theorem Th104:
for g being f-compatible Function holds dom g c= dom f
proof
let g be f-compatible Function;
let x be object;
assume x in dom g;
then g.x in f.x by Def14;
hence x in dom f by Def2;
end;
registration let X;
let f be X-defined Function;
cluster f-compatible -> X-defined for Function;
coherence
proof let g be Function;
assume g is f-compatible;
then
A1: dom g c= dom f by Th104;
dom f c= X by RELAT_1:def 18;
hence dom g c= X by A1;
end;
end;
theorem
for f being X-valued Function st x in dom f holds f.x is Element of X
proof let f be X-valued Function;
assume x in dom f;
then
A1: f.x in rng f by Def3;
rng f c= X by RELAT_1:def 19;
hence f.x is Element of X by A1;
end;
:: from JGRAPH_6, 2010.03.15, A.T.
theorem
for f being Function,A being set st f is one-to-one & A c= dom f
holds f".:(f.:A)=A
proof
let f be Function,A be set;
set B = f.:A;
assume that
A1: f is one-to-one and
A2: A c= dom f;
A3: f".:B c= A
proof
let y be object;
assume y in f".:B;
then consider x being object such that
x in dom (f") and
A4: x in B and
A5: y=f".x by Def6;
ex y2 being object st ( y2 in dom f)&( y2 in A)&( x=f.y2) by A4,Def6;
hence thesis by A1,A5,Th31;
end;
A c= f".:B
proof
let x be object;
assume
A6: x in A;
set y0=f.x;
A7: f".y0=x by A1,A2,A6,Th33;
y0 in rng f by A2,A6,Def3;
then
A8: y0 in dom (f") by A1,Th32;
y0 in B by A2,A6,Def6;
hence thesis by A7,A8,Def6;
end;
hence thesis by A3;
end;
registration
let A be functional set, x be object;
let F be A-valued Function;
cluster F.x -> Function-like Relation-like;
coherence
proof
per cases;
suppose x in dom F;
then
A1: F.x in rng F by Def3;
rng F c= A by RELAT_1:def 19;
hence thesis by A1;
end;
suppose not x in dom F;
hence thesis by Def2;
end;
end;
end;
:: missing, 2011.03.06, A.T.
theorem Th107:
x in X & x in dom f implies f.x in f.:X
proof assume that
A1: x in X and
A2: x in dom f;
x in X /\ dom f by A1,A2,XBOOLE_0:def 4;
then x in dom(f|X) by RELAT_1:61;
then
A3: (f|X).x in rng(f|X) by Def3;
(f|X).x = f.x by A1,Th48;
hence f.x in f.:X by A3,RELAT_1:115;
end;
theorem
X <> {} & X c= dom f implies f.:X <> {}
proof assume X <> {};
then ex x being object st x in X by XBOOLE_0:def 1;
hence thesis by Th107;
end;
registration
let f be non trivial Function;
cluster dom f -> non trivial;
coherence
proof
consider u,w being object such that
A1: u in f and
A2: w in f and
A3: u <> w by ZFMISC_1:def 10;
consider u1,u2 being object such that
A4: u = [u1,u2] by A1,RELAT_1:def 1;
consider w1,w2 being object such that
A5: w = [w1,w2] by A2,RELAT_1:def 1;
take u1,w1;
thus u1 in dom f & w1 in dom f by A4,A5,A1,A2,XTUPLE_0:def 12;
thus u1 <> w1 by A1,A2,A3,A4,A5,Def1;
end;
end;
:: from HAHNBAN, 2011.04.26, A.T.
theorem
for B being non empty functional set, f being Function
st f = union B
holds dom f = union the set of all dom g where g is Element of B
& rng f = union the set of all rng g where g is Element of B
proof
let B be non empty functional set, f be Function such that
A1: f = union B;
set X = the set of all dom g where g is Element of B;
now
let x be object;
hereby
assume x in dom f;
then [x,f.x] in f by Th1;
then consider g being set such that
A2: [x,f.x] in g and
A3: g in B by A1,TARSKI:def 4;
reconsider g as Function by A3;
take Z = dom g;
thus x in Z & Z in X by A2,A3,Th1;
end;
given Z being set such that
A4: x in Z and
A5: Z in X;
consider g being Element of B such that
A6: Z = dom g by A5;
[x,g.x] in g by A4,A6,Th1;
then [x,g.x] in f by A1,TARSKI:def 4;
hence x in dom f by Th1;
end;
hence dom f = union X by TARSKI:def 4;
set X = the set of all rng g where g is Element of B;
now
let y be object;
hereby
assume y in rng f;
then consider x being object such that
A7: x in dom f & y = f.x by Def3;
[x,y] in f by A7,Th1;
then consider g being set such that
A8: [x,y] in g and
A9: g in B by A1,TARSKI:def 4;
reconsider g as Function by A9;
take Z = rng g;
x in dom g & y = g.x by A8,Th1;
hence y in Z & Z in X by A9,Def3;
end;
given Z being set such that
A10: y in Z and
A11: Z in X;
consider g being Element of B such that
A12: Z = rng g by A11;
consider x being object such that
A13: x in dom g & y = g.x by A10,A12,Def3;
[x,y] in g by A13,Th1;
then [x,y] in f by A1,TARSKI:def 4;
hence y in rng f by XTUPLE_0:def 13;
end;
hence thesis by TARSKI:def 4;
end;
scheme
LambdaS { A() -> set,F(object) -> object } :
ex f being Function st dom f = A() &
for X st X in A() holds f.X = F(X)
proof
defpred P[object,object] means $2 = F($1);
A1: for x st x in A() ex y st P[x,y];
A2: for x,y1,y2 st x in A() & P[x,y1] & P[x,y2] holds y1 = y2;
consider f being Function such that
A3: dom f = A() and
A4: for x st x in A() holds P[x,f.x] from FuncEx(A2,A1);
take f;
thus dom f = A() by A3;
thus thesis by A4;
end;
theorem Th110: :: WELLORD2:28
for M being set
st for X st X in M holds X <> {}
ex f being Function
st dom f = M & for X st X in M holds f.X in X
proof let M be set;
assume
A1: for X st X in M holds X <> {};
deffunc F(set) = the Element of $1;
consider f being Function such that
A2: dom f = M and
A3: for X st X in M holds f.X = F(X) from LambdaS;
take f;
thus dom f = M by A2;
let X;
assume
A4: X in M;
then
A5: f.X = the Element of X by A3;
X <> {} by A1,A4;
hence f.X in X by A5;
end;
scheme
NonUniqBoundFuncEx { X() -> set, Y() -> set, P[object,object] }:
ex f being Function st dom f = X() & rng f c= Y()
& for x being object st x in X() holds P[x,f.x]
provided
A1: for x being object st x in X() ex y being object st y in Y() & P[x,y]
proof
per cases;
suppose
A2: X() = {};
take {};
thus thesis by A2;
end;
suppose
A3: X() <> {};
defpred Q[object,object] means
ex D2 being set st D2 = $2 & for y holds y in D2 iff y in Y() & P[$1,y];
A4: for e,u1,u2 being object st e in X() & Q[e,u1] & Q[e,u2] holds u1 = u2
proof
let e,u1,u2 be object such that
e in X();
given U1 being set such that
A5: U1 = u1 and
A6: for y holds y in U1 iff y in Y() & P[e,y];
defpred A[object] means $1 in Y() & P[e,$1];
A7: for x be object holds x in U1 iff A[x] by A6;
given U2 being set such that
A8: U2 = u2 and
A9: for y holds y in U2 iff y in Y() & P[e,y];
A10: for x be object holds x in U2 iff A[x] by A9;
U1 = U2 from XBOOLE_0:sch 2(A7,A10);
hence thesis by A5,A8;
end;
A11: for x st x in X() ex y st Q[x,y]
proof
let x such that
x in X();
defpred R[object] means P[x,$1];
consider X such that
A12: for y being object holds y in X iff y in Y() & R[y] from XBOOLE_0:sch 1;
take X;
thus thesis by A12;
end;
consider G being Function such that
A13: dom G = X() & for x st x in X() holds Q[x,G.x] from FuncEx(A4,A11);
reconsider D = rng G as non empty set by A13,A3,RELAT_1:42;
now
let X;
assume X in D;
then consider x being object such that
A14: x in dom G & X = G.x by Def3;
consider y being object such that
A15: y in Y() & P[x,y] by A1,A13,A14;
Q[x,G.x] by A13,A14;
then y in X by A15,A14;
hence X <> {};
end;
then consider F be Function such that
A16: dom F = D and
A17: for X st X in D holds F.X in X by Th110;
A18: dom (F*G) = X() by A13,A16,RELAT_1:27;
take f = F*G;
thus dom f = X() by A13,A16,RELAT_1:27;
rng F c= Y()
proof
let x be object;
assume x in rng F;
then consider y being object such that
A19: y in dom F and
A20: x = F.y by Def3;
consider z being object such that
A21: z in dom G & y = G.z by A16,A19,Def3;
reconsider y as set by TARSKI:1;
A22: x in y by A16,A17,A19,A20;
Q[z,G.z] by A13,A21;
hence thesis by A21,A22;
end;
hence rng f c= Y() by A16,RELAT_1:28;
let x be object;
assume
A23: x in X();
then f.x = F.(G.x) & G.x in D by A13,A18,Th12,Def3;
then
A24: f.x in G.x by A17;
Q[x,G.x] by A13,A23;
hence thesis by A24;
end;
end;
registration
let f be empty-yielding Function;
let x;
cluster f.x -> empty;
coherence
proof
x in dom f or not x in dom f;
hence thesis by Def2,Def8;
end;
end;
:: from PNPROC_1, 2012.02.20, A.T.
theorem
for f,g,h being Function st
f c= h & g c= h & f misses g holds dom f misses dom g
proof
let f,g,h be Function such that
A1: f c= h and
A2: g c= h and
A3: f misses g;
for x being object st x in dom f holds not x in dom g
proof
let x be object;
assume x in dom f;
then
A4: [x,f.x] in f by Def2;
now
assume x in dom g;
then
A5: [x,g.x] in g by Def2;
then f.x = g.x by A1,A2,A4,Def1;
hence contradiction by A3,A4,A5,XBOOLE_0:3;
end;
hence thesis;
end;
hence thesis by XBOOLE_0:3;
end;
theorem
for Y being set, f being Function holds Y|`f = f|(f"Y)
proof
let Y be set, f be Function;
A1: Y|`f c= f|(f"Y) by RELAT_1:188;
f|(f"Y) c= Y|`f
proof let x,y be object;
assume
A2: [x,y] in f|(f"Y);
then
A3: x in f"Y by RELAT_1:def 11;
A4: [x,y] in f by A2,RELAT_1:def 11;
f.x in Y by A3,Def7;
then y in Y by A4,Th1;
hence thesis by A4,RELAT_1:def 12;
end;
hence thesis by A1;
end;
registration
let X be set;
let x be Element of X;
reduce (id X).x to x;
reducibility
proof
per cases;
suppose
A1: X is empty;
then x is empty by SUBSET_1:def 1;
hence thesis by A1;
end;
suppose X is non empty;
hence thesis by Th18;
end;
end;
end;
theorem
rng f c= rng g implies
for x being object st x in dom f
ex y being object st y in dom g & f.x = g. y
proof
assume that
A1: rng f c= rng g;
let x be object;
assume x in dom f;
then f.x in rng f by Def3;
then
A2: f.x in rng g by A1;
ex y being object st y in dom g & f.x = g.y by Def3,A2;
hence thesis;
end;