:: The Modification of a Function by a Function
:: and the Iteration of the Composition of a Function
:: by Czes{\l}aw Byli\'nski
::
:: Received March 1, 1990
:: 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, FUNCT_1, TARSKI, ZFMISC_1, RELAT_1, FUNCOP_1, SUBSET_1,
PARTFUN1, FUNCT_2, ORDINAL1, FUNCT_4, REALSET1;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, ORDINAL1, RELAT_1,
FUNCT_1, RELSET_1, REALSET1, FUNCT_2, BINOP_1, PARTFUN1, FUNCOP_1;
constructors PARTFUN1, BINOP_1, FUNCOP_1, RELSET_1, ORDINAL1, REALSET1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FUNCOP_1, RELSET_1, ZFMISC_1,
SUBSET_1, REALSET1;
requirements BOOLE, SUBSET;
definitions TARSKI, FUNCT_2, PARTFUN1, XBOOLE_0, FUNCOP_1, FUNCT_1;
equalities BINOP_1, FUNCOP_1, REALSET1;
expansions TARSKI, PARTFUN1, XBOOLE_0, FUNCT_1, ZFMISC_1;
theorems TARSKI, FUNCT_1, FUNCT_2, GRFUNC_1, PARTFUN1, FUNCOP_1, ZFMISC_1,
RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, ENUMSET1, ORDINAL1, XTUPLE_0,
SUBSET_1;
schemes FUNCT_1, PARTFUN1, XBOOLE_0;
begin :: Auxiliary theorems
reserve a,b,p,x,x9,x1,x19,x2,y,y9,y1,y19,y2,z,z9,z1,z2 for object,
X,X9,Y,Y9,Z,Z9 for set;
reserve A,D,D9 for non empty set;
reserve f,g,h for Function;
Lm1:
for x,y,x1,y1,x9,y9,x19,y19 being object holds
[[x,x9],[y,y9]] = [[x1,x19],[y1,y19]] implies x = x1 & y = y1 & x9= x19 &
y9 = y19
proof let x,y,x1,y1,x9,y9,x19,y19 be object;
assume [[x,x9],[y,y9]] = [[x1,x19],[y1,y19]];
then [x,x9] = [x1,x19] & [y,y9] = [y1,y19] by XTUPLE_0:1;
hence thesis by XTUPLE_0:1;
end;
theorem Th1:
(for z being object st z in Z holds ex x,y being object st z = [x,y])
implies ex X,Y st Z c= [:X,Y:]
proof
assume
A1: for z being object st z in Z holds ex x,y being object st z = [x,y];
defpred P[object] means ex y being object st [ $1,y] in Z;
consider X such that
A2: for x being object holds
x in X iff x in union union Z & P[ x] from XBOOLE_0:sch 1;
defpred P[object] means ex x being object st [x,$1] in Z;
consider Y such that
A3: for y being object holds
y in Y iff y in union union Z & P[y] from XBOOLE_0:sch 1;
take X,Y;
let z be object;
assume
A4: z in Z;
then consider x,y being object such that
A5: z = [x,y] by A1;
x in union union Z by A4,A5,ZFMISC_1:134;
then
A6: x in X by A2,A4,A5;
y in union union Z by A4,A5,ZFMISC_1:134;
then y in Y by A3,A4,A5;
hence thesis by A5,A6,ZFMISC_1:87;
end;
theorem
g*f = (g|rng f)*f
proof
for x being object holds x in dom(g*f) iff x in dom((g|rng f)*f)
proof let x be object;
A1: dom(g|rng f) = dom g /\ rng f by RELAT_1:61;
thus x in dom(g*f) implies x in dom((g|rng f)*f)
proof
assume
A2: x in dom(g*f);
then
A3: x in dom f by FUNCT_1:11;
x in dom f by A2,FUNCT_1:11;
then
A4: f.x in rng f by FUNCT_1:def 3;
f.x in dom g by A2,FUNCT_1:11;
then f.x in dom(g|rng f) by A1,A4,XBOOLE_0:def 4;
hence thesis by A3,FUNCT_1:11;
end;
assume
A5: x in dom((g|rng f)*f);
then f.x in dom(g|rng f) by FUNCT_1:11;
then
A6: f.x in dom g by A1,XBOOLE_0:def 4;
x in dom f by A5,FUNCT_1:11;
hence thesis by A6,FUNCT_1:11;
end;
then
A7: dom(g*f) = dom((g|rng f)*f) by TARSKI:2;
for x being object holds x in dom(g*f) implies (g*f).x = ((g|rng f)*f).x
proof let x be object;
assume
A8: x in dom(g*f);
then
A9: x in dom f by FUNCT_1:11;
then
A10: f.x in rng f by FUNCT_1:def 3;
thus (g*f).x = g.(f.x) by A8,FUNCT_1:12
.= (g|rng f).(f.x) by A10,FUNCT_1:49
.= ((g|rng f)*f).x by A9,FUNCT_1:13;
end;
hence thesis by A7;
end;
theorem
id X c= id Y iff X c= Y
proof
thus id X c= id Y implies X c= Y
proof
assume
A1: id X c= id Y;
let x be object;
assume x in X;
then [x,x] in id X by RELAT_1:def 10;
hence thesis by A1,RELAT_1:def 10;
end;
assume
A2: X c= Y;
let z be object;
assume
A3: z in id X;
then consider x,x9 being object such that
A4: x in X and
x9 in X and
A5: z = [x,x9] by ZFMISC_1:84;
x = x9 by A3,A5,RELAT_1:def 10;
hence thesis by A2,A4,A5,RELAT_1:def 10;
end;
theorem
X c= Y implies X --> a c= Y --> a
proof
assume
A2: X c= Y;
A3: now
let x be object;
assume
A4: x in dom(X --> a);
then (X --> a).x = a by FUNCOP_1:7;
hence (X --> a).x = (Y --> a).x by A2,A4,FUNCOP_1:7;
end;
dom(Y --> a) = Y;
hence thesis by A2,A3,GRFUNC_1:2;
end;
theorem Th5:
for a,b being object holds
X --> a c= Y --> b implies X c= Y
proof let a,b be object;
assume X --> a c= Y --> b;
then
A1: dom(X --> a) c= dom(Y --> b) by RELAT_1:11;
thus thesis by A1;
end;
theorem
for a,b being object holds
X <> {} & X --> a c= Y --> b implies a = b
proof let a,b be object;
assume
A1: X <> {};
set x = the Element of X;
assume
A2: X --> a c= Y --> b;
then X c= Y by Th5;
then x in Y by A1;
then
A3: (Y --> b).x = b by FUNCOP_1:7;
dom(X --> a) = X & (X --> a).x = a by A1,FUNCOP_1:7;
hence thesis by A1,A2,A3,GRFUNC_1:2;
end;
theorem
x in dom f implies x .--> f.x c= f
proof
A1: now
let y be object;
assume y in dom (x .--> f.x);
then x = y by FUNCOP_1:75;
hence (x .--> f.x).y = f.y by FUNCOP_1:72;
end;
assume
A2: x in dom f;
dom (x .--> f.x) c= dom f
by A2,FUNCOP_1:75;
hence thesis by A1,GRFUNC_1:2;
end;
:: Natural order on functions
theorem
Y|`f|X c= f
proof
Y|`f|X c= Y|`f & Y|`f c= f by RELAT_1:59,86;
hence thesis;
end;
theorem
f c= g implies Y|`f|X c= Y|`g|X
proof
assume f c= g;
then Y|`f c= Y|`g by RELAT_1:101;
hence thesis by RELAT_1:76;
end;
definition
let f,g;
func f +* g -> Function means
:Def1:
dom it = dom f \/ dom g &
for x being object st x in dom f \/ dom g holds
(x in dom g implies it.x = g.x) &
(not x in dom g implies it.x = f.x);
existence
proof
deffunc G(object) = f.$1;
deffunc F(object) = g.$1;
defpred P[object] means $1 in dom g;
thus ex F being Function st dom F = dom f \/ dom g &
for x being object st x in dom f \/ dom g holds
(P[x] implies F.x = F(x)) & (not P[x] implies F.x = G(x))
from PARTFUN1:sch 1;
end;
uniqueness
proof
let h1,h2 be Function such that
A1: dom h1 = dom f \/ dom g and
A2: for x being object
st x in dom f \/ dom g holds (x in dom g implies h1.x = g.x)
& (not x in dom g implies h1.x = f.x) and
A3: dom h2 = dom f \/ dom g and
A4: for x being object
st x in dom f \/ dom g holds (x in dom g implies h2.x = g.x)
& (not x in dom g implies h2.x = f.x);
for x being object st x in dom f \/ dom g holds h1.x = h2.x
proof
let x be object;
assume
A5: x in dom f \/ dom g;
then
A6: not x in dom g implies h1.x = f.x & h2.x = f.x by A2,A4;
x in dom g implies h1.x = g.x & h2.x = g.x by A2,A4,A5;
hence thesis by A6;
end;
hence thesis by A1,A3;
end;
idempotence;
end;
theorem Th10:
dom f c= dom(f+*g) & dom g c= dom(f+*g)
proof
dom(f+*g) = dom f \/ dom g by Def1;
hence thesis by XBOOLE_1:7;
end;
theorem Th11:
for x being object holds
not x in dom g implies (f +* g).x = f.x
proof let x be object;
assume
A1: not x in dom g;
per cases;
suppose
x in dom f;
then x in dom f \/ dom g by XBOOLE_0:def 3;
hence thesis by A1,Def1;
end;
suppose
A2: not x in dom f;
then not x in dom f \/ dom g by A1,XBOOLE_0:def 3;
then not x in dom(f+*g) by Def1;
hence (f+*g).x = {} by FUNCT_1:def 2
.= f.x by A2,FUNCT_1:def 2;
end;
end;
theorem Th12:
for x being object holds
x in dom(f +* g) iff x in dom f or x in dom g
proof let x be object;
x in dom(f +* g) iff x in dom f \/ dom g by Def1;
hence thesis by XBOOLE_0:def 3;
end;
theorem Th13:
for x being object holds
x in dom g implies (f+*g).x = g.x
proof let x be object;
x in dom g implies x in dom f \/ dom g by XBOOLE_0:def 3;
hence thesis by Def1;
end;
theorem Th14:
f +* g +* h = f +* (g +* h)
proof
A1: now
let x be object such that
x in dom f \/ dom(g +* h);
hereby
assume
A2: x in dom(g +* h);
per cases by A2,Th12;
suppose
A3: x in dom g & not x in dom h;
hence (f +* g +* h).x = (f +* g).x by Th11
.= g.x by A3,Th13
.= (g +* h).x by A3,Th11;
end;
suppose
A4: x in dom h;
hence (f +* g +* h).x = h.x by Th13
.= (g +* h).x by A4,Th13;
end;
end;
assume
A5: not x in dom(g +* h);
then
A6: not x in dom g by Th12;
not x in dom h by A5,Th12;
hence (f +* g +* h).x = (f +* g).x by Th11
.= f.x by A6,Th11;
end;
dom(f +* g +* h) = dom(f +* g) \/ dom h by Def1
.= dom f \/ dom g \/ dom h by Def1
.= dom f \/ (dom g \/ dom h) by XBOOLE_1:4
.= dom f \/ dom(g +* h) by Def1;
hence thesis by A1,Def1;
end;
theorem Th15:
f tolerates g & x in dom f implies (f+*g).x = f.x
proof
assume that
A1: f tolerates g and
A2: x in dom f;
now
per cases;
suppose
x in dom g;
then x in dom f /\ dom g & (f+*g).x = g.x by A2,Th13,XBOOLE_0:def 4;
hence thesis by A1;
end;
suppose
not x in dom g;
hence thesis by Th11;
end;
end;
hence thesis;
end;
theorem
dom f misses dom g & x in dom f implies (f +* g).x = f.x
proof
assume dom f /\ dom g = {} & x in dom f;
then not x in dom g by XBOOLE_0:def 4;
hence thesis by Th11;
end;
theorem Th17:
rng(f +* g) c= rng f \/ rng g
proof
let y be object;
assume y in rng(f +* g);
then consider x being object such that
A1: x in dom (f +* g) and
A2: y = (f +* g).x by FUNCT_1:def 3;
x in dom f & not x in dom g or x in dom g by A1,Th12;
then x in dom f & (f +* g).x = f.x or x in dom g & (f +* g).x = g.x by Th11
,Th13;
then y in rng f or y in rng g by A2,FUNCT_1:def 3;
hence thesis by XBOOLE_0:def 3;
end;
theorem
rng g c= rng(f +* g)
proof
let y be object;
assume y in rng g;
then consider x being object such that
A1: x in dom g & y = g.x by FUNCT_1:def 3;
x in dom(f +* g) & (f +* g).x = y by A1,Th12,Th13;
hence thesis by FUNCT_1:def 3;
end;
theorem Th19:
dom f c= dom g implies f +* g = g
proof
assume dom f c= dom g;
then dom f \/ dom g = dom g by XBOOLE_1:12;
then dom(f +* g) = dom g &
for x being object st x in dom g holds (f +* g).x = g.x by Def1;
hence thesis;
end;
registration let f; let g be empty Function;
reduce g +* f to f;
reducibility
proof
dom g c= dom f;
hence thesis by Th19;
end;
reduce f +* g to f;
reducibility
proof
A1: for x being object st x in dom f holds (f +* g).x = f.x
proof
let x be object;
assume x in dom f;
then x in dom f \ dom g;
hence thesis by Th11;
end;
dom f \/ dom g = dom f;
then dom(f +* g) = dom f by Def1;
hence thesis by A1;
end;
end;
theorem
{} +* f = f;
theorem
f +* {} = f;
theorem
id(X) +* id(Y) = id(X \/ Y)
proof
A1: for x being object holds
x in dom id(X \/ Y) implies (id(X) +* id(Y)).x = id(X \/ Y).x
proof let x be object;
assume
A2: x in dom id(X \/ Y);
now
per cases;
suppose
A3: x in Y;
dom id Y = Y;
hence (id(X) +* id(Y)).x = (id Y).x by A3,Th13
.= x by A3,FUNCT_1:18
.= id(X \/ Y).x by A2,FUNCT_1:18;
end;
suppose
A4: not x in Y;
then
A5: x in X by A2,XBOOLE_0:def 3;
not x in dom id Y by A4;
hence (id(X) +* id(Y)).x = (id X).x by Th11
.= x by A5,FUNCT_1:18
.= id(X \/ Y).x by A2,FUNCT_1:18;
end;
end;
hence thesis;
end;
dom(id(X) +* id(Y)) = dom id X \/ dom id Y by Def1
.= X \/ dom id Y
.= X \/ Y
.= dom id(X \/ Y);
hence thesis by A1;
end;
theorem Th23:
(f +* g)|(dom g) = g
proof
dom f \/ dom g = dom(f +* g) by Def1;
then
A1: dom((f +* g)|(dom g)) = dom g by RELAT_1:62,XBOOLE_1:7;
for x being object st x in dom g holds ((f +* g)|(dom g)).x = g.x
proof
let x be object;
x in dom g implies (f +* g).x = g.x by Th13;
hence thesis by A1,FUNCT_1:47;
end;
hence thesis by A1;
end;
registration
let f,g be Function;
reduce (f +* g)|(dom g) to g;
reducibility by Th23;
end;
theorem Th24:
((f +* g)|(dom f \ dom g)) c= f
proof
A1: for x being object
st x in dom((f +* g)|(dom f \ dom g)) holds ((f +* g)|(dom f \ dom
g)).x = f.x
proof
let x be object such that
A2: x in dom((f +* g)|(dom f \ dom g));
dom((f +* g)|(dom f \ dom g)) c= dom f \ dom g by RELAT_1:58;
then not x in dom g by A2,XBOOLE_0:def 5;
then (f +* g).x = f.x by Th11;
hence thesis by A2,FUNCT_1:47;
end;
dom((f +* g)|(dom f \ dom g)) c= dom f \ dom g by RELAT_1:58;
then dom((f +* g)|(dom f \ dom g)) c= dom f by XBOOLE_1:1;
hence thesis by A1,GRFUNC_1:2;
end;
theorem Th25:
g c= f +* g
proof
dom(f +* g) = dom f \/ dom g by Def1;
then
A1: dom g c= dom(f +* g) by XBOOLE_1:7;
for x being object st x in dom g holds (f+*g).x = g.x by Th13;
hence thesis by A1,GRFUNC_1:2;
end;
theorem
f tolerates g +* h implies f|(dom f \ dom h) tolerates g
proof
assume
A1: f tolerates g +* h;
let x be object;
assume
A2: x in dom(f|(dom f \ dom h)) /\ dom g;
then
A3: x in dom(f|(dom f \ dom h)) by XBOOLE_0:def 4;
x in dom g by A2,XBOOLE_0:def 4;
then
A4: x in dom(g +* h) by Th12;
A5: dom(f|(dom f \ dom h)) c= dom f \ dom h by RELAT_1:58;
then x in dom f by A3,XBOOLE_0:def 5;
then
A6: x in dom f /\ dom(g +* h) by A4,XBOOLE_0:def 4;
not x in dom h by A3,A5,XBOOLE_0:def 5;
then (g +* h).x = g.x by Th11;
then f.x = g.x by A1,A6;
hence thesis by A3,A5,FUNCT_1:49;
end;
theorem Th27:
f tolerates g +* h implies f tolerates h
proof
assume
A1: f tolerates g +* h;
let x be object;
assume
A2: x in dom f /\ dom h;
then
A3: x in dom f by XBOOLE_0:def 4;
A4: x in dom h by A2,XBOOLE_0:def 4;
then x in dom(g +* h) by Th12;
then
A5: x in dom f /\ dom(g +* h) by A3,XBOOLE_0:def 4;
(g +* h).x = h.x by A4,Th13;
hence thesis by A1,A5;
end;
theorem Th28:
f tolerates g iff f c= f +* g
proof
thus f tolerates g implies f c= (f +* g)
proof
dom f \/ dom g = dom(f +* g) by Def1;
then
A1: dom f c= dom(f +* g) by XBOOLE_1:7;
assume f tolerates g;
then for x being object st x in dom f holds (f +* g).x = f.x by Th15;
hence thesis by A1,GRFUNC_1:2;
end;
thus thesis by Th27,PARTFUN1:54;
end;
theorem Th29:
f +* g c= f \/ g
proof
let p be object;
assume
A1: p in f +* g;
then consider x,y being object such that
A2: p = [x,y] by RELAT_1:def 1;
x in dom(f +* g) by A1,A2,FUNCT_1:1;
then x in dom f & not x in dom g or x in dom g by Th12;
then
A3: x in dom f & (f +* g).x = f.x or x in dom g & (f +* g).x = g.x by Th11,Th13
;
y = (f +* g).x by A1,A2,FUNCT_1:1;
then p in f or p in g by A2,A3,FUNCT_1:1;
hence thesis by XBOOLE_0:def 3;
end;
theorem Th30:
f tolerates g iff f \/ g = f +* g
proof
thus f tolerates g implies f \/ g = f +* g
proof
assume f tolerates g;
then
A1: f c= f +* g by Th28;
A2: f +* g c= f \/ g by Th29;
g c= f +* g by Th25;
then f \/ g c= f +* g by A1,XBOOLE_1:8;
hence thesis by A2;
end;
thus thesis by PARTFUN1:51;
end;
theorem Th31:
dom f misses dom g implies f \/ g = f +* g by Th30,PARTFUN1:56;
theorem Th32:
dom f misses dom g implies f c= f +* g
proof
assume dom f misses dom g;
then f \/ g = f +* g by Th31;
hence thesis by XBOOLE_1:7;
end;
theorem
dom f misses dom g implies (f +* g)|(dom f) = f
proof
assume dom f misses dom g;
then
A1: dom f \ dom g = dom f by XBOOLE_1:83;
dom((f +* g)|(dom f)) = dom(f +* g) /\ dom f by RELAT_1:61
.= (dom f \/ dom g) /\ dom f by Def1
.= dom f by XBOOLE_1:21;
hence thesis by A1,Th24,GRFUNC_1:3;
end;
theorem Th34:
f tolerates g iff f +* g = g +* f
proof
thus f tolerates g implies f +* g = g +* f
proof
assume
A1: f tolerates g;
A2: for x being object st x in dom(f +* g) holds (f +* g).x = (g +* f).x
proof
let x being object such that
A3: x in dom(f +* g);
now
A4: dom(f +* g) = dom f \/ dom g by Def1;
per cases by A3,A4,XBOOLE_0:def 3;
suppose
A5: x in dom f & x in dom g;
then
A6: (g +* f).x = f.x by Th13;
x in dom f /\ dom g & (f +* g).x = g.x by A5,Th13,XBOOLE_0:def 4;
hence thesis by A1,A6;
end;
suppose
A7: x in dom f & not x in dom g;
then (f +* g).x = f.x by Th11;
hence thesis by A7,Th13;
end;
suppose
A8: not x in dom f & x in dom g;
then (f +* g).x = g.x by Th13;
hence thesis by A8,Th11;
end;
end;
hence thesis;
end;
dom(f +* g) = dom g \/ dom f by Def1
.= dom(g +* f) by Def1;
hence thesis by A2;
end;
assume
A9: f +* g = g +* f;
let x be object;
assume
A10: x in dom f /\ dom g;
then x in dom g by XBOOLE_0:def 4;
then
A11: (f +* g).x = g.x by Th13;
x in dom f by A10,XBOOLE_0:def 4;
hence thesis by A9,A11,Th13;
end;
theorem Th35:
dom f misses dom g implies f +* g = g +* f by Th34,PARTFUN1:56;
theorem
for f,g being PartFunc of X,Y st g is total holds f +* g = g
proof
let f,g be PartFunc of X,Y;
assume dom g = X;
then dom f c= dom g;
hence thesis by Th19;
end;
theorem Th37:
for f,g being Function of X,Y holds f +* g = g
proof
let f,g be Function of X,Y;
per cases;
suppose Y = {} implies X = {};
then dom f = X & dom g = X by FUNCT_2:def 1;
hence thesis by Th19;
end;
suppose Y = {} & X <> {};
then f = {} & g = {};
hence thesis;
end;
end;
theorem
for f,g being Function of X,X holds f +* g = g by Th37;
theorem
for f,g being Function of X,D holds f +* g = g by Th37;
theorem
for f,g being PartFunc of X,Y holds f +* g is PartFunc of X,Y
proof
let f,g be PartFunc of X,Y;
rng (f +* g) c= rng f \/ rng g by Th17;
then
A1: rng(f +* g) c= Y by XBOOLE_1:1;
dom (f +* g) = dom f \/ dom g by Def1;
hence thesis by A1,RELSET_1:4;
end;
:: The converse function whenever domain
definition
let f;
func ~f -> Function means
:Def2:
(for x being object holds x in dom it iff
ex y,z being object st x = [z,y] & [y,z] in dom f) &
for y,z being object st [y,z] in dom f holds it.(z,y) = f.(y,z);
existence
proof
defpred P[object,object] means
ex y,z being object st $1 = [z,y] & $2 = f.[y,z];
defpred Q[object] means ex y being object st [ $1,y] in dom f;
consider D1 being set such that
A1: for x being object holds
x in D1 iff x in union union dom f & Q[ x] from XBOOLE_0:sch 1;
defpred Q[object] means ex y being object st [y,$1] in dom f;
consider D2 being set such that
A2: for y being object holds
y in D2 iff y in union union dom f & Q[y] from XBOOLE_0:sch 1;
defpred Q[object] means
ex y,z being object st $1 = [z,y] & [y,z] in dom f;
consider D being set such that
A3: for x being object holds
x in D iff x in [:D2,D1:] & Q[ x] from XBOOLE_0:sch 1;
A4: for x,y1,y2 being object st x in D & P[x,y1] & P[x,y2] holds y1 = y2
proof
let x,y1,y2 being object such that x in D;
given y,z being object such that
A5: x = [z,y] and
A6: y1 = f.[y,z];
given y9,z9 being object such that
A7: x = [z9,y9] and
A8: y2 = f.[y9,z9];
z = z9 by A5,A7,XTUPLE_0:1;
hence thesis by A5,A6,A7,A8,XTUPLE_0:1;
end;
A9: for x being object st x in D ex y1 being object st P[x,y1]
proof
let x be object;
assume x in D;
then consider y1,z1 being object such that
A10: x = [z1,y1] and
[y1,z1] in dom f by A3;
take f.[y1,z1];
thus thesis by A10;
end;
consider h being Function such that
A11: dom h = D and
A12: for x being object st x in D holds P[x,h.x] from FUNCT_1:sch 2(A4,A9);
take h;
thus
A13: for x being object holds x in dom h iff
ex y,z being object st x = [z,y] & [y,z] in dom f
proof
let x be object;
thus x in dom h implies
ex y,z being object st x = [z,y] & [y,z] in dom f by A3,A11;
given y,z being object such that
A14: x = [z,y] and
A15: [y,z] in dom f;
y in union union dom f by A15,ZFMISC_1:134; then
A16: y in D1 by A1,A15;
z in union union dom f by A15,ZFMISC_1:134;
then z in D2 by A2,A15;
then [z,y] in [:D2,D1:] by A16,ZFMISC_1:87;
hence thesis by A3,A11,A14,A15;
end;
let y,z be object;
assume [y,z] in dom f;
then [z,y] in D by A11,A13;
then consider y9,z9 being object such that
A17: [z,y] = [z9,y9] and
A18: h.(z,y) = f.[y9,z9] by A12;
z = z9 by A17,XTUPLE_0:1;
hence thesis by A17,A18,XTUPLE_0:1;
end;
uniqueness
proof
let h1,h2 be Function such that
A19: for x being object
holds x in dom h1 iff
ex y,z being object st x = [z,y] & [y,z] in dom f and
A20: for y,z being object st [y,z] in dom f holds h1.(z,y) = f.(y,z) and
A21: for x being object
holds x in dom h2 iff
ex y,z being object st x = [z,y] & [y,z] in dom f and
A22: for y,z being object st [y,z] in dom f holds h2.(z,y) = f.(y,z);
A23: for x being object holds x in dom h1 implies h1.x = h2.x
proof let x be object;
assume x in dom h1;
then consider x1,x2 being object such that
A24: x = [x2,x1] and
A25: [x1,x2] in dom f by A19;
h1.(x2,x1) = f.(x1,x2) by A20,A25
.= h2.(x2,x1) by A22,A25;
hence thesis by A24;
end;
for x being object holds x in dom h1 iff x in dom h2
proof let x be object;
x in dom h1 iff ex y,z being object st x = [z,y] & [y,z] in dom f
by A19;
hence thesis by A21;
end;
then dom h1 = dom h2 by TARSKI:2;
hence thesis by A23;
end;
end;
theorem Th41:
rng ~f c= rng f
proof
let y be object;
assume y in rng ~f;
then consider x being object such that
A1: x in dom ~f and
A2: y = (~f).x by FUNCT_1:def 3;
consider x1,x2 being object such that
A3: x = [x2,x1] and
A4: [x1,x2] in dom f by A1,Def2;
y = (~f).(x2,x1) by A2,A3
.= f.(x1,x2) by A4,Def2;
hence thesis by A4,FUNCT_1:def 3;
end;
theorem Th42:
for x,y being object holds [x,y] in dom f iff [y,x] in dom ~f
proof let x,y be object;
thus [x,y] in dom f implies [y,x] in dom ~f by Def2;
assume [y,x] in dom ~f;
then consider x1,y1 being object such that
A1: [y,x] = [y1,x1] and
A2: [x1,y1] in dom f by Def2;
x1 = x by A1,XTUPLE_0:1;
hence thesis by A1,A2,XTUPLE_0:1;
end;
registration
let f be empty Function;
cluster ~f -> empty;
coherence
proof rng f = {};
then rng~f = {} by Th41,XBOOLE_1:3;
hence thesis;
end;
end;
theorem Th43:
for x,y being object holds [y,x] in dom ~f implies (~f).(y,x) = f.(x,y)
proof let x,y be object;
assume [y,x] in dom ~f;
then [x,y] in dom f by Th42;
hence thesis by Def2;
end;
theorem
ex X,Y st dom ~f c= [:X,Y:]
proof
now
let z be object;
assume z in dom ~f;
then ex x,y being object st z = [y,x] & [x,y] in dom f by Def2;
hence ex x,y being object st z = [x,y];
end;
hence thesis by Th1;
end;
theorem Th45:
dom f c= [:X,Y:] implies dom ~f c= [:Y,X:]
proof
assume
A1: dom f c= [:X,Y:];
let z be object;
assume z in dom ~f;
then ex x,y being object st z = [y,x] & [x,y] in dom f by Def2;
hence thesis by A1,ZFMISC_1:88;
end;
theorem Th46:
dom f = [:X,Y:] implies dom ~f = [:Y,X:]
proof
assume
A1: dom f = [:X,Y:];
hence dom ~f c= [:Y,X:] by Th45;
let z be object;
assume z in [:Y,X:];
then consider y,x being object such that
A2: y in Y & x in X and
A3: z = [y,x] by ZFMISC_1:def 2;
[x,y] in dom f by A1,A2,ZFMISC_1:def 2;
hence thesis by A3,Def2;
end;
theorem Th47:
dom f c= [:X,Y:] implies rng ~f = rng f
proof
assume
A1: dom f c= [:X,Y:];
thus rng ~f c= rng f by Th41;
let y be object;
assume y in rng f;
then consider x being object such that
A2: x in dom f and
A3: y = f.x by FUNCT_1:def 3;
consider x1,y1 being object such that
x1 in X and
y1 in Y and
A4: x =[x1,y1] by A1,A2,ZFMISC_1:84;
A5: [y1,x1] in dom ~f by A2,A4,Th42;
y = f.(x1,y1) by A3,A4
.= (~f).(y1,x1) by A2,A4,Def2;
hence thesis by A5,FUNCT_1:def 3;
end;
theorem Th48:
for f being PartFunc of [:X,Y:],Z holds ~f is PartFunc of [:Y,X:],Z
proof
let f be PartFunc of [:X,Y:],Z;
A1: dom f c= [:X,Y:];
then
A2: dom ~f c= [:Y,X:] by Th45;
rng f c= Z;
then rng ~f c= Z by A1,Th47;
hence thesis by A2,RELSET_1:4;
end;
definition
let X,Y,Z;
let f be PartFunc of [:X,Y:],Z;
redefine func ~f -> PartFunc of [:Y,X:],Z; :: redefines ~ (FUNCT_4, definition)
coherence by Th48;
end;
theorem Th49:
for f being Function of [:X,Y:],Z holds ~f is Function of [:Y,X:],Z
proof
let f be Function of [:X,Y:],Z;
per cases;
suppose
A1: Z = {};
then reconsider f as empty set;
~f = {};
hence thesis by A1,FUNCT_2:130;
end;
suppose
A1: Z <> {};
reconsider R = ~f as Relation of [:Y,X:],Z;
R is quasi_total
proof
per cases;
case Z <> {};
dom f = [:X,Y:] by A1,FUNCT_2:def 1;
hence thesis by Th46;
end;
case Z = {};
hence thesis;
end;
end;
hence thesis;
end;
end;
definition
let X,Y,Z;
let f be Function of [:X,Y:],Z;
redefine func ~f -> Function of [:Y,X:],Z; :: redefines ~ (FUNCT_4, definition)
coherence by Th49;
end;
theorem
for f being Function of [:X,Y:],Z holds ~f is Function of [:Y,X:],Z;
theorem Th51:
~~f c= f
proof
A1: now
let x be object;
assume x in dom ~~f;
then consider y2,z2 being object such that
A2: x = [z2,y2] & [y2,z2] in dom ~f by Def2;
take y2,z2;
thus x = [z2,y2] & [y2,z2] in dom ~ f & [z2,y2] in dom f by A2,Th42;
end;
A3: for x being object holds x in dom ~~f implies (~~f).x = f.x
proof let x be object;
assume x in dom ~~f;
then consider y2,z2 being object such that
A4: x = [z2,y2] and
A5: [y2,z2] in dom ~f and
A6: [z2,y2] in dom f by A1;
(~~f).(z2,y2) = (~f).(y2,z2) by A5,Def2
.= f.(z2,y2) by A6,Def2;
hence thesis by A4;
end;
dom ~~f c= dom f
proof
let x be object;
assume x in dom ~~f;
then
ex y2,z2 being object
st x = [z2,y2] & [y2,z2] in dom ~ f & [z2,y2] in dom f by A1;
hence thesis;
end;
hence thesis by A3,GRFUNC_1:2;
end;
theorem Th52:
dom f c= [:X,Y:] implies ~~f = f
proof
assume
A1: dom f c= [:X,Y:];
A2: ~~f c= f by Th51;
dom ~~ f = dom f
proof
thus dom ~~f c= dom f by A2,RELAT_1:11;
let z be object;
assume
A3: z in dom f;
then consider x,y being object such that
x in X and
y in Y and
A4: z = [x,y] by A1,ZFMISC_1:84;
[y,x] in dom ~f by A3,A4,Th42;
hence thesis by A4,Th42;
end;
hence thesis by Th51,GRFUNC_1:3;
end;
theorem
for f being PartFunc of [:X,Y:],Z holds ~~f = f
proof
let f be PartFunc of [:X,Y:],Z;
dom f c= [:X,Y:];
hence thesis by Th52;
end;
:: Product of 2'ary functions
definition
let f,g;
func |:f,g:| -> Function means
:Def3:
(for z being object holds z in dom it
iff ex x,y,x9,y9 being object
st z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g) &
for x,y,x9,y9 being object
st [x,y] in dom f & [x9,y9] in dom g holds it.([x,x9],[y,y9]) = [f.(x,y),g.(x9,
y9)];
existence
proof
defpred P[object,object] means
ex x,y,x9,y9 being object st $1 = [[x,x9],[y,y9]] & $2 = [f.[x
,y],g.[x9,y9]];
defpred Q[object] means ex y being object st [ $1,y] in dom f;
consider D1 being set such that
A1: for x being object holds
x in D1 iff x in union union dom f & Q[ x] from XBOOLE_0:sch 1;
defpred Q[object] means ex x being object st [x,$1] in dom f;
consider D2 being set such that
A2: for y being object holds
y in D2 iff y in union union dom f & Q[y] from XBOOLE_0:sch 1;
defpred Q[object] means ex y being object st [ $1,y] in dom g;
consider D19 being set such that
A3: for x being object holds
x in D19 iff x in union union dom g & Q[ x] from XBOOLE_0:sch 1;
defpred Q[object] means ex x being object st [x,$1] in dom g;
consider D29 being set such that
A4: for y being object holds
y in D29 iff y in union union dom g & Q[y] from XBOOLE_0:sch 1;
defpred Q[object] means
ex x,y,x9,y9 being object st $1 = [[x,x9],[y,y9]] & [x,y] in dom f
& [x9,y9] in dom g;
consider D being set such that
A5: for z being object holds
z in D iff z in [:[:D1,D19:],[:D2,D29:]:] & Q[z] from XBOOLE_0:sch
1;
A6: for z,z1,z2 being object st z in D & P[z,z1] & P[z,z2] holds z1 = z2
proof
let z,z1,z2 being object such that
z in D;
given x,y,x9,y9 being object such that
A7: z = [[x,x9],[y,y9]] and
A8: z1 = [f.[x,y],g.[x9,y9]];
given x1,y1,x19,y19 being object such that
A9: z = [[x1,x19],[y1,y19]] and
A10: z2 = [f.[x1,y1],g.[x19,y19]];
A11: x9 = x19 by A7,A9,Lm1;
x = x1 & y = y1 by A7,A9,Lm1;
hence thesis by A7,A8,A9,A10,A11,Lm1;
end;
A12: for z being object st z in D holds ex z1 being object st P[z,z1]
proof
let z be object;
assume z in D;
then consider x1,y1,x8,y8 being object such that
A13: z = [[x1,x8],[y1,y8]] and
[x1,y1] in dom f and
[x8,y8] in dom g by A5;
take [f.[x1,y1],g.[x8,y8]];
thus thesis by A13;
end;
consider h being Function such that
A14: dom h = D and
A15: for z being object st z in D holds P[z,h.z] from FUNCT_1:sch 2(A6,A12);
take h;
thus
A16: for z being object holds z in dom h iff
ex x,y,x9,y9 being object st z = [[x,x9],[y,y9]] &
[x,y] in dom f & [x9,y9] in dom g
proof
let z be object;
thus z in dom h implies
ex x,y,x9,y9 being object st z = [[x,x9],[y,y9]] & [x,y] in
dom f & [x9,y9] in dom g by A5,A14;
given x,y,x9,y9 being object such that
A17: z = [[x,x9],[y,y9]] and
A18: [x,y] in dom f and
A19: [x9,y9] in dom g;
y9 in union union dom g by A19,ZFMISC_1:134;
then
A20: y9 in D29 by A4,A19;
y in union union dom f by A18,ZFMISC_1:134;
then y in D2 by A2,A18;
then
A21: [y,y9] in [:D2,D29:] by A20,ZFMISC_1:87;
x9 in union union dom g by A19,ZFMISC_1:134;
then
A22: x9 in D19 by A3,A19;
x in union union dom f by A18,ZFMISC_1:134;
then x in D1 by A1,A18;
then [x,x9] in [:D1,D19:] by A22,ZFMISC_1:87;
then z in [:[:D1,D19:],[:D2,D29:]:] by A17,A21,ZFMISC_1:87;
hence thesis by A5,A14,A17,A18,A19;
end;
let x,y,x9,y9 be object;
assume [x,y] in dom f & [x9,y9] in dom g;
then [[x,x9],[y,y9]] in D by A14,A16;
then consider x1,y1,x19,y19 being object such that
A23: [[x,x9],[y,y9]] = [[x1,x19],[y1,y19]] and
A24: h.[[x,x9],[y,y9]] = [f.[x1,y1],g.[x19,y19]] by A15;
A25: x9= x19 by A23,Lm1;
x = x1 & y = y1 by A23,Lm1;
hence thesis by A23,A24,A25,Lm1;
end;
uniqueness
proof
let h1,h2 be Function such that
A26: for z being object holds z in dom h1 iff
ex x,y,x9,y9 being object st z = [[x,x9],[y,y9]] &
[x,y] in dom f & [x9,y9] in dom g and
A27: for x,y,x9,y9 being object
st [x,y] in dom f & [x9,y9] in dom g holds h1.([x,
x9],[y,y9]) = [f.(x,y),g.(x9,y9)] and
A28: for z being object holds z in dom h2 iff
ex x,y,x9,y9 being object st z = [[x,x9],[y,y9]] &
[x,y] in dom f & [x9,y9] in dom g and
A29: for x,y,x9,y9 being object
st [x,y] in dom f & [x9,y9] in dom g holds h2.([x,
x9],[y,y9]) = [f.(x,y),g.(x9,y9)];
A30: for z being object holds z in dom h1 implies h1.z = h2.z
proof let z be object;
assume z in dom h1;
then consider x,y,x9,y9 being object such that
A31: z = [[x,x9],[y,y9]] and
A32: [x,y] in dom f & [x9,y9] in dom g by A26;
h1.([x,x9],[y,y9]) = [f.(x,y),g.(x9,y9)] by A27,A32
.= h2.([x,x9],[y,y9]) by A29,A32;
hence thesis by A31;
end;
for z being object holds z in dom h1 iff z in dom h2
proof let z be object;
z in dom h1 iff
ex x,y,x9,y9 being object st z = [[x,x9],[y,y9]] & [x,y] in dom
f & [x9,y9] in dom g by A26;
hence thesis by A28;
end;
then dom h1 = dom h2 by TARSKI:2;
hence thesis by A30;
end;
end;
theorem Th54:
[[x,x9],[y,y9]] in dom |:f,g:| iff [x,y] in dom f & [x9,y9] in dom g
proof
thus [[x,x9],[y,y9]] in dom |:f,g:| implies [x,y] in dom f & [x9,y9] in dom
g
proof
assume [[x,x9],[y,y9]] in dom |:f,g:|;
then consider x1,y1,x19,y19 being object such that
A1: [[x,x9],[y,y9]] = [[x1,x19],[y1,y19]] and
A2: [x1,y1] in dom f & [x19,y19] in dom g by Def3;
x = x1 & x9= x19 by A1,Lm1;
hence thesis by A1,A2,Lm1;
end;
thus thesis by Def3;
end;
theorem
[[x,x9],[y,y9]] in dom |:f,g:| implies |:f,g:|.([x,x9],[y,y9]) = [f.(x
,y),g.(x9,y9)]
proof
assume [[x,x9],[y,y9]] in dom |:f,g:|;
then [x,y] in dom f & [x9,y9] in dom g by Th54;
hence thesis by Def3;
end;
theorem Th56:
rng |:f,g:| c= [:rng f,rng g:]
proof
let z be object;
assume z in rng |:f,g:|;
then consider p being object such that
A1: p in dom |:f,g:| and
A2: z = |:f,g:|.p by FUNCT_1:def 3;
consider x,y,x9,y9 being object such that
A3: p = [[x,x9],[y,y9]] and
A4: [x,y] in dom f & [x9,y9] in dom g by A1,Def3;
A5: f.[x,y] in rng f & g.[x9,y9] in rng g by A4,FUNCT_1:def 3;
z = |:f,g:|.([x,x9],[y,y9]) by A2,A3
.= [f.(x,y),g.(x9,y9)] by A4,Def3;
hence thesis by A5,ZFMISC_1:87;
end;
theorem Th57:
dom f c= [:X,Y:] & dom g c= [:X9,Y9:] implies dom|:f,g:| c= [:[:
X,X9:],[:Y,Y9:]:]
proof
assume
A1: dom f c= [:X,Y:] & dom g c= [:X9,Y9:];
let xy be object;
assume xy in dom|:f,g:|;
then consider x,y,x9,y9 being object such that
A2: xy = [[x,x9],[y,y9]] and
A3: [x,y] in dom f & [x9,y9] in dom g by Def3;
y in Y & y9 in Y9 by A1,A3,ZFMISC_1:87;
then
A4: [y,y9] in [:Y,Y9:] by ZFMISC_1:87;
x in X & x9 in X9 by A1,A3,ZFMISC_1:87;
then [x,x9] in [:X,X9:] by ZFMISC_1:87;
hence thesis by A2,A4,ZFMISC_1:87;
end;
theorem Th58:
dom f = [:X,Y:] & dom g = [:X9,Y9:] implies
dom|:f,g:| = [:[:X,X9:],[:Y,Y9:]:]
proof
assume
A1: dom f = [:X,Y:] & dom g = [:X9,Y9:];
hence dom|:f,g:| c= [:[:X,X9:],[:Y,Y9:]:] by Th57;
let z be object;
assume z in [:[:X,X9:],[:Y,Y9:]:];
then consider xx,yy being object such that
A2: xx in [:X,X9:] and
A3: yy in [:Y,Y9:] and
A4: z = [xx,yy] by ZFMISC_1:def 2;
consider y,y9 being object such that
A5: y in Y & y9 in Y9 and
A6: yy = [y,y9] by A3,ZFMISC_1:def 2;
consider x,x9 being object such that
A7: x in X & x9 in X9 and
A8: xx = [x,x9] by A2,ZFMISC_1:def 2;
[x,y] in dom f & [x9,y9] in dom g by A1,A7,A5,ZFMISC_1:87;
hence thesis by A4,A8,A6,Def3;
end;
theorem Th59:
for f being PartFunc of [:X,Y:],Z for g being PartFunc of [:X9,Y9:],Z9
holds |:f,g:| is PartFunc of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:]
proof
let f be PartFunc of [:X,Y:],Z;
let g be PartFunc of [:X9,Y9:],Z9;
rng |:f,g:| c= [:rng f,rng g:] & [:rng f,rng g:] c= [:Z,Z9:] by Th56,
ZFMISC_1:96;
then
A1: rng|:f,g:| c= [:Z,Z9:];
dom f c= [:X,Y:] & dom g c= [:X9,Y9:];
then dom|:f,g:| c= [:[:X,X9:],[:Y,Y9:]:] by Th57;
hence thesis by A1,RELSET_1:4;
end;
theorem Th60:
for f being Function of [:X,Y:],Z for g being Function of [:X9,
Y9:],Z9 st Z <> {} & Z9 <> {} holds |:f,g:| is Function of [:[:X,X9:],[:Y,Y9:]
:],[:Z,Z9:]
proof
let f be Function of [:X,Y:],Z;
let g be Function of [:X9,Y9:],Z9;
rng |:f,g:| c= [:rng f,rng g:] & [:rng f,rng g:] c= [:Z,Z9:] by Th56,
ZFMISC_1:96;
then
A1: rng|:f,g:| c= [:Z,Z9:];
assume
A2: Z <> {} & Z9 <> {};
then dom f = [:X,Y:] & dom g = [:X9,Y9:] by FUNCT_2:def 1;
then [:[:X,X9:],[:Y,Y9:]:] = dom|:f,g:| by Th58;
then reconsider
R = |:f,g:| as Relation of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:] by A1,RELSET_1:4;
R is quasi_total
proof
per cases;
case [:Z,Z9:] <> {};
dom f = [:X,Y:] & dom g = [:X9,Y9:] by A2,FUNCT_2:def 1;
hence thesis by Th58;
end;
case [:Z,Z9:] = {};
hence thesis;
end;
end;
hence thesis;
end;
theorem
for f being Function of [:X,Y:],D for g being Function of [:X9,Y9:],D9
holds |:f,g:| is Function of [:[:X,X9:],[:Y,Y9:]:],[:D,D9:] by Th60;
definition
let x,y,a,b be object;
func (x,y) --> (a,b) -> set equals
(x .--> a) +* (y .--> b);
correctness;
end;
registration
let x,y,a,b be object;
cluster (x,y) --> (a,b) -> Function-like Relation-like;
coherence;
end;
theorem Th62:
for x1,x2,y1,y2 being object holds
dom((x1,x2) --> (y1,y2)) = {x1,x2} & rng((x1,x2) --> (y1,y2)) c= {y1,y2}
proof let x1,x2,y1,y2 be object;
set f = {x1} --> y1, g = {x2} -->y2, h = (x1,x2) --> (y1,y2);
rng f \/ rng g c= {y1} \/ {y2} by XBOOLE_1:13;
then
A1: rng f \/ rng g c= {y1,y2} by ENUMSET1:1;
dom f \/ dom g = {x1,x2} by ENUMSET1:1;
hence dom h = {x1,x2} by Def1;
rng h c= rng f \/ rng g by Th17;
hence thesis by A1;
end;
theorem Th63:
for x1,x2,y1,y2 being object holds
(x1 <> x2 implies ((x1,x2) --> (y1,y2)).x1 = y1) &
((x1,x2) --> (y1,y2)).x2 = y2
proof let x1,x2,y1,y2 be object;
set f = {x1} --> y1, g = {x2} -->y2, h = (x1,x2) --> (y1,y2);
A1: x2 in {x2} by TARSKI:def 1;
A2: x1 in {x1} by TARSKI:def 1;
hereby
assume x1 <> x2;
then not x1 in dom g by TARSKI:def 1;
then h.x1 = f.x1 by Th11;
hence h.x1 = y1 by A2,FUNCOP_1:7;
end;
{x2} = dom g;
then h.x2 = g.x2 by A1,Th13;
hence thesis by A1,FUNCOP_1:7;
end;
theorem
for x1,x2,y1,y2 being object holds
x1 <> x2 implies rng((x1,x2) --> (y1,y2)) = {y1,y2}
proof let x1,x2,y1,y2 be object;
set h = (x1,x2) --> (y1,y2);
assume
A1: x1 <> x2;
thus rng h c= {y1,y2} by Th62;
let y be object;
assume y in {y1,y2};
then y = y1 or y = y2 by TARSKI:def 2;
then
A2: h.x1 = y or h.x2 = y by A1,Th63;
dom h = {x1,x2} by Th62;
then x1 in dom h & x2 in dom h by TARSKI:def 2;
hence thesis by A2,FUNCT_1:def 3;
end;
theorem
for x1,x2,y being object holds
(x1,x2) --> (y,y) = {x1,x2} --> y
proof let x1,x2,y be object;
set F = (x1,x2)-->(y,y), f = {x1}-->y, g = {x2}-->y, F9 = {x1,x2}-->y;
now
thus
A1: dom F = {x1,x2} & dom F9 = {x1,x2} by Th62;
let x be object such that
A2: x in {x1,x2};
now
per cases by A1,A2,Th12;
suppose
A3: x in dom f & not x in dom g;
then F.x = f.x by Th11;
hence F.x = y & F9.x = y by A2,A3,FUNCOP_1:7;
end;
suppose
A4: x in dom g;
then F.x = g.x by Th13;
hence F.x = y & F9.x = y by A2,A4,FUNCOP_1:7;
end;
end;
hence F.x = F9.x;
end;
hence thesis;
end;
definition
let A,x1,x2;
let y1,y2 be Element of A;
redefine func (x1,x2) --> (y1,y2) -> Function of {x1,x2},A; :: redefines --> (FUNCT_4, definition)
coherence
proof
set f = {x1} --> y1, g = {x2} -->y2, h = (x1,x2) --> (y1,y2);
rng h c= rng f \/ rng g by Th17;
then
A1: rng h c= A by XBOOLE_1:1;
dom h = {x1,x2} by Th62;
hence thesis by A1,FUNCT_2:def 1,RELSET_1:4;
end;
end;
theorem
for a,b,c,d being object, g being Function st dom g = {a,b} & g.a = c & g
.b = d holds g = (a,b) --> (c,d)
proof
let a,b,c,d be object;
let h be Function such that
A1: dom h = {a,b} and
A2: h.a = c and
A3: h.b = d;
set f = {a} --> c, g = {b} -->d;
A4: b in {b} by TARSKI:def 1;
A5: a in {a} by TARSKI:def 1;
A6: now
let x be object such that
A7: x in dom f \/ dom g;
thus x in dom g implies h.x = g.x
proof
assume x in dom g;
then x = b by TARSKI:def 1;
hence thesis by A3,A4,FUNCOP_1:7;
end;
assume not x in dom g;
then x in dom f by A7,XBOOLE_0:def 3;
then x = a by TARSKI:def 1;
hence h.x = f.x by A2,A5,FUNCOP_1:7;
end;
dom h = dom f \/ dom g by A1,ENUMSET1:1;
hence thesis by A6,Def1;
end;
theorem Th67:
for a,b,c,d being object st a <> c holds (a,c) --> (b,d) = { [a,b],
[c,d] }
proof
let a,b,c,d be object such that
A1: a <> c;
set f = {a} --> b, g = {c} --> d;
{a} --> b = {[a,b]} & {c} --> d = {[c,d]} by ZFMISC_1:29;
hence (a,c) --> (b,d) = {[a,b]} \/ {[c,d]} by A1,Th31,ZFMISC_1:11
.= { [a,b], [c,d] } by ENUMSET1:1;
end;
theorem
for a,b,x,y,x9,y9 being object st a <> b & (a,b) --> (x,y) = (a,b) --> (
x9,y9) holds x = x9 & y = y9
proof
let a,b,x,y,x9,y9 be object such that
A1: a <> b and
A2: (a,b) --> (x,y) = (a,b) --> (x9,y9);
thus x = ((a,b) --> (x,y)).a by A1,Th63
.= x9 by A1,A2,Th63;
thus y = ((a,b) --> (x,y)).b by Th63
.= y9 by A2,Th63;
end;
begin :: Addenda
:: from CIRCCOMB
theorem
for f1,f2, g1,g2 being Function st rng g1 c= dom f1 & rng g2 c= dom f2
& f1 tolerates f2 holds (f1+*f2)*(g1+*g2) = (f1*g1)+*(f2*g2)
proof
let f1,f2, g1,g2 be Function;
assume that
A1: rng g1 c= dom f1 & rng g2 c= dom f2 and
A2: f1 tolerates f2;
A3: rng (g1+*g2) c= (rng g1) \/ rng g2 & dom (f1+*f2) = (dom f1) \/ dom f2
by Def1,Th17;
(rng g1) \/ rng g2 c= (dom f1) \/ dom f2 by A1,XBOOLE_1:13;
then
A4: dom ((f1+*f2)*(g1+*g2)) = dom (g1+*g2) by A3,RELAT_1:27,XBOOLE_1:1
.= (dom g1) \/ dom g2 by Def1;
A5: dom (f1*g1) = dom g1 & dom (f2*g2) = dom g2 by A1,RELAT_1:27;
A6: now
let x be object;
A7: not x in dom g2 or x in dom g2;
assume
A8: x in (dom g1) \/ dom g2;
then
A9: ((f1+*f2)*(g1+*g2)).x = (f1+*f2).((g1+*g2).x) by A4,FUNCT_1:12;
x in dom g1 or x in dom g2 by A8,XBOOLE_0:def 3;
then
(g1+*g2).x = g1.x & ((f1*g1)+*(f2*g2)).x = (f1*g1).x & (f1*g1).x = f1
.(g1.x) & g1.x in rng g1 & (g1.x in rng g1 implies g1.x in dom f1) or (g1+*g2).
x = g2.x & ((f1*g1)+*(f2*g2)).x = (f2*g2).x & (f2*g2).x = f2.(g2.x) & g2.x in
rng g2 & (g2.x in rng g2 implies g2.x in dom f2) by A1,A5,A8,A7,Def1,
FUNCT_1:12,def 3;
hence ((f1+*f2)*(g1+*g2)).x = ((f1*g1)+*(f2*g2)).x by A2,A9,Th13,Th15;
end;
dom ((f1*g1)+*(f2*g2)) = (dom g1) \/ dom g2 by A5,Def1;
hence thesis by A4,A6;
end;
:: from AMI_1
reserve A,B for set;
theorem Th70:
dom f c= A \/ B implies f|A +* f|B = f
proof
A1: dom(f|A) = dom f /\ A & dom(f|B) = dom f /\ B by RELAT_1:61;
A2: for x being object holds
x in dom(f|A) \/ dom(f|B) implies (x in dom(f|B) implies f.x = f|B.x) &
(not x in dom(f|B) implies f.x = f|A.x)
proof let x be object;
assume
A3: x in dom(f|A) \/ dom(f|B);
thus x in dom(f|B) implies f.x = f|B.x by FUNCT_1:47;
assume not x in dom(f|B);
then x in dom(f|A) by A3,XBOOLE_0:def 3;
hence thesis by FUNCT_1:47;
end;
assume dom f c= A \/ B;
then dom f = dom f /\ (A \/ B) by XBOOLE_1:28
.= dom(f|A) \/ dom(f|B) by A1,XBOOLE_1:23;
hence thesis by A2,Def1;
end;
:: from AMI_5
theorem Th71:
for p,q being Function , A being set holds (p +* q)|A = p|A +* q|A
proof
let p,q be Function , A be set;
A1: dom ((p +* q)|A) = dom (p +* q) /\ A by RELAT_1:61
.= (dom p \/ dom q) /\ A by Def1
.= (dom p /\ A) \/ (dom q /\ A) by XBOOLE_1:23
.= dom (p|A) \/ (dom q /\ A) by RELAT_1:61
.= dom (p|A) \/ dom (q|A) by RELAT_1:61;
for x being object st x in dom (p|A) \/ dom (q|A) holds (x in dom (q|A)
implies ((p +* q)|A).x = (q|A).x) & (not x in dom (q|A) implies ((p +* q)|A).x
= (p|A).x)
proof
let x be object;
assume
A2: x in dom (p|A) \/ dom (q|A);
then x in dom (p|A) or x in dom (q|A) by XBOOLE_0:def 3;
then x in (dom p /\ A) or x in dom q /\ A by RELAT_1:61;
then
A3: x in A by XBOOLE_0:def 4;
hereby
assume
A4: x in dom (q|A);
then x in (dom q /\ A) by RELAT_1:61;
then
A5: x in dom q by XBOOLE_0:def 4;
thus ((p +* q)|A).x = (p +* q).x by A1,A2,FUNCT_1:47
.= q.x by A5,Th13
.= (q|A).x by A4,FUNCT_1:47;
end;
assume
A6: not x in dom (q|A);
then not x in (dom q /\ A) by RELAT_1:61;
then
A7: not x in dom q by A3,XBOOLE_0:def 4;
A8: x in dom (p|A) by A2,A6,XBOOLE_0:def 3;
then x in dom p /\ A by RELAT_1:61;
then x in dom p by XBOOLE_0:def 4;
then x in dom (p +* q) by Th12;
then x in dom (p +* q) /\ A by A3,XBOOLE_0:def 4;
then x in dom ((p +* q)|A) by RELAT_1:61;
hence ((p +* q)|A).x = (p +* q).x by FUNCT_1:47
.= p.x by A7,Th11
.= (p|A).x by A8,FUNCT_1:47;
end;
hence thesis by A1,Def1;
end;
theorem Th72:
for f,g being Function, A being set st A misses dom g holds
(f +* g)|A = f|A
proof
let f,g be Function, A be set;
assume A misses dom g;
then dom g /\ A = {};
then dom (g|A) = {} by RELAT_1:61;
then g|A = {};
hence (f +* g)|A = f|A +* {} by Th71
.= f|A;
end;
theorem
for f,g being Function , A being set holds dom f misses A implies
(f +* g)|A = g|A
proof
let f,g be Function , A be set;
assume dom f misses A;
then dom f /\ A = {};
then dom (f|A) = {} by RELAT_1:61;
then f|A = {};
hence (f +* g)|A = {} +* g|A by Th71
.= g|A;
end;
theorem
for f,g,h being Function st dom g = dom h holds f +* g +* h = f +* h
proof
let f,g,h be Function;
assume
A1: dom g = dom h;
thus f +* g +* h = f +* (g +* h) by Th14
.= f +* h by A1,Th19;
end;
Lm2:
for f,g being Function holds f c= g implies g +* f = g
proof
let f,g be Function;
assume
A1: f c= g;
then f tolerates g by PARTFUN1:54;
hence g+*f = f\/ g by Th30
.= g by A1,XBOOLE_1:12;
end;
theorem
for f being Function, A being set holds f +* f|A = f by Lm2,RELAT_1:59;
theorem
for f,g being Function, B,C being set st dom f c= B & dom g c= C & B
misses C holds (f +* g)|B = f & (f +* g)|C = g
proof
let f,g be Function, B,C be set;
assume that
A1: dom f c= B and
A2: dom g c= C and
A3: B misses C;
dom f misses C by A1,A3,XBOOLE_1:63;
then dom f /\ C = {};
then dom (f|C) = {} by RELAT_1:61;
then
A4: f|C = {};
dom g misses B by A2,A3,XBOOLE_1:63;
then dom g /\ B = {};
then dom (g|B) = {} by RELAT_1:61;
then
A5: g|B = {};
thus (f +* g)|B = f|B +* g|B by Th71
.= f|B by A5
.= f by A1,RELAT_1:68;
thus (f +* g)|C = f|C +* g|C by Th71
.= g|C by A4
.= g by A2,RELAT_1:68;
end;
theorem
for p,q being Function, A being set holds dom p c= A & dom q misses A
implies (p +* q)|A = p
proof
let p,q be Function, A be set;
assume that
A1: dom p c= A and
A2: dom q misses A;
thus (p +* q )|A = p|A by A2,Th72
.= p by A1,RELAT_1:68;
end;
theorem
for f being Function, A,B being set holds f|(A \/ B) = f|A +* f|B
proof
let f be Function, A,B be set;
A1: f|(A \/ B)|B = f|((A \/ B) /\ B) by RELAT_1:71
.= f|B by XBOOLE_1:21;
A2: dom (f|(A \/ B)) c= A \/ B by RELAT_1:58;
f|(A \/ B)|A = f|((A \/ B) /\ A) by RELAT_1:71
.= f|A by XBOOLE_1:21;
hence thesis by A1,A2,Th70;
end;
:: from ALTCAT_1, CQC_LANG, 2007.03.13, A.T.
reserve x,y,i,j,k for object;
theorem
(i,j):->k = [i,j].-->k;
theorem
((i,j):->k).(i,j) = k by FUNCOP_1:71;
:: from AMI_1, 2006.03.14, A.T.
theorem Th81:
for a,b,c being object holds (a,a) --> (b,c) = a .--> c
proof
let a,b,c be object;
dom(a .-->c) = {a}
.= dom({a} -->b);
hence thesis by Th19;
end;
theorem
for x,y holds x .--> y = {[x,y]} by ZFMISC_1:29;
:: from SCMPDS_9, 2006.03.26, A.T.
theorem
for f being Function, a,b,c being object st a <> c holds (f +* (a .-->b))
.c = f.c
proof
let f be Function, a,b,c be object such that
A1: a <> c;
set g = a .-->b;
not c in dom g by A1,TARSKI:def 1;
hence thesis by Th11;
end;
theorem Th84:
for f being Function, a,b,c,d being object st a <> b holds
(f +* ((a,b)-->(c,d))) .a = c & (f +* ((a,b)-->(c,d))) .b = d
proof
let f be Function, a,b,c,d be object such that
A1: a <> b;
set g = (a,b)-->(c,d);
A2: dom g = {a,b} by Th62;
then a in dom g by TARSKI:def 2;
hence (f +* g).a = g.a by Th13
.= c by A1,Th63;
b in dom g by A2,TARSKI:def 2;
hence (f +* g).b = g.b by Th13
.= d by Th63;
end;
:: from AMI_3, 2007.06.14, A.T.
theorem Th85:
for a,b being set, f being Function st a in dom f & f.a = b
holds a .--> b c= f
proof
let a,b be set, f be Function;
assume a in dom f & f.a = b;
then [a,b] in f by FUNCT_1:1;
then {[a,b]} c= f by ZFMISC_1:31;
hence thesis by ZFMISC_1:29;
end;
theorem
for a,b,c,d being set, f being Function st
a in dom f & c in dom f & f.a = b & f.c = d holds (a,c) --> (b,d) c= f
proof
let a,b,c,d be set, f be Function;
assume that
A1: a in dom f and
A2: c in dom f and
A3: f.a = b & f.c = d;
per cases;
suppose
A4: a <> c;
[a,b] in f & [c,d] in f by A1,A2,A3,FUNCT_1:1;
then { [a,b], [c,d]} c= f by ZFMISC_1:32;
hence thesis by A4,Th67;
end;
suppose
a = c;
hence thesis by A1,A3,Th85;
end;
end;
:: from SCMFSA6A, 2007.07.23, A.T.
theorem Th87:
for f,g,h being Function st f c= h & g c= h holds f +* g c= h
proof
let f,g,h be Function;
assume f c= h & g c= h;
then
A1: f \/ g c= h by XBOOLE_1:8;
f +* g c= f \/ g by Th29;
hence thesis by A1;
end;
:: from SCMFSA6B, 2007.07.25, A.T.
theorem
for f, g being Function, A being set st A /\ dom f c= A /\ dom g holds
(f+*g|A)|A = g|A
proof
let f, g be Function, A be set;
assume
A1: A /\ dom f c= A /\ dom g;
A2: dom (f|A) = A /\ dom f & dom (g|A) = A /\ dom g by RELAT_1:61;
thus (f+*g|A)|A = (f|A)+*(g|A)|A by Th71
.= (f|A)+*g|A
.= g|A by A1,A2,Th19;
end;
:: from SCMBSORT, 2007.07.26, A.T.
theorem Th89:
for f be Function, a,b,n,m be object holds
(f +* (a .--> b) +* (m .--> n)).m = n
proof
let f be Function, a,b,n,m be object;
set mn=m .--> n;
m in dom mn by TARSKI:def 1;
hence (f +* (a .--> b) +* mn).m=mn.m by Th13
.=n by FUNCOP_1:72;
end;
theorem
for f be Function, n,m be object holds (f +* (n .--> m) +* (m .--> n)).n=
m
proof
let f be Function,n,m be object;
set mn=m .--> n, nm=n .--> m;
A1: m in dom mn by TARSKI:def 1;
per cases;
suppose
A2: n=m;
hence (f +* nm +* mn).n=mn.m by A1,Th13
.=m by A2,FUNCOP_1:72;
end;
suppose
A3: n<>m;
A4: n in dom nm by TARSKI:def 1;
not n in dom mn by A3,TARSKI:def 1;
hence (f +* nm +* mn).n=(f +* nm).n by Th11
.=nm.n by A4,Th13
.=m by FUNCOP_1:72;
end;
end;
theorem
for f be Function, a,b,n,m,x be object st x <> m & x <> a
holds (f +* (a.--> b) +* (m .--> n)).x=f.x
proof
let f be Function, a,b,n,m,x be object;
assume that
A1: x<>m and
A2: x<>a;
set mn=m .--> n, nm=a .--> b;
A3: not x in dom nm by A2,TARSKI:def 1;
not x in dom mn by A1,TARSKI:def 1;
hence (f +* nm +* mn).x=(f +* nm).x by Th11
.=f.x by A3,Th11;
end;
:: from KNASTER, 2007.010.28, A.T.
theorem
f is one-to-one & g is one-to-one & rng f misses rng g implies
f+*g is one-to-one
proof
set fg = f+*g;
assume that
A1: f is one-to-one and
A2: g is one-to-one and
A3: rng f misses rng g;
let x1,x2 be object;
assume that
A4: x1 in dom fg and
A5: x2 in dom fg and
A6: fg.x1 = fg.x2;
A7: x1 in dom f or x1 in dom g by A4,Th12;
A8: x2 in dom f or x2 in dom g by A5,Th12;
per cases;
suppose
A9: x1 in dom g & x2 in dom g;
then fg.x1 = g.x1 & fg.x2 = g.x2 by Th13;
hence thesis by A2,A6,A9;
end;
suppose
A10: x1 in dom g & not x2 in dom g;
then x2 in dom f by A5,Th12;
then
A11: f.x2 in rng f by FUNCT_1:def 3;
A12: g.x1 in rng g by A10,FUNCT_1:def 3;
fg.x1 = g.x1 & fg.x2 = f.x2 by A10,Th11,Th13;
hence thesis by A3,A6,A12,A11,XBOOLE_0:3;
end;
suppose
A13: not x1 in dom g & x2 in dom g;
then x1 in dom f by A4,Th12;
then
A14: f.x1 in rng f by FUNCT_1:def 3;
A15: g.x2 in rng g by A13,FUNCT_1:def 3;
fg.x1 = f.x1 & fg.x2 = g.x2 by A13,Th11,Th13;
hence thesis by A3,A6,A15,A14,XBOOLE_0:3;
end;
suppose
A16: not x1 in dom g & not x2 in dom g;
then fg.x1 = f.x1 & fg.x2 = f.x2 by Th11;
hence thesis by A1,A6,A7,A8,A16;
end;
end;
registration let f,g be Function;
reduce f +* g +* g to f +* g;
reducibility
proof
thus f +* g +* g = f +*( g +* g ) by Th14
.= f +* g;
end;
end;
:: from SCMFSA_9, 2008.03.04, A.T.
theorem
for f,g being Function holds f +* g +* g = f +* g;
theorem
for f,g,h being Function, D being set holds (f +* g)|D =h | D implies
(h +* g) | D = (f +* g) | D
proof
let f,g,h be Function, D be set;
assume
A1: (f +* g)|D =h | D;
A2: dom ((f +* g) | D) = dom (f +* g) /\ D by RELAT_1:61
.= (dom f \/ dom g) /\ D by Def1;
A3: dom ((h +* g) | D) = dom (h +* g) /\ D by RELAT_1:61
.= (dom h \/ dom g) /\ D by Def1;
then
A4: dom ((h +* g) | D) = (dom h /\ D) \/ (dom g /\ D) by XBOOLE_1:23
.= ((dom f \/ dom g) /\ D) \/ (dom g /\ D) by A1,A2,RELAT_1:61
.= ((dom f \/ dom g) \/ dom g) /\ D by XBOOLE_1:23
.= (dom f \/ (dom g \/ dom g)) /\ D by XBOOLE_1:4
.= (dom f \/ dom g ) /\ D;
now
let x be object;
assume
A5: x in dom ((f +* g) | D);
then
A6: x in dom f \/ dom g by A2,XBOOLE_0:def 4;
A7: x in D by A2,A5,XBOOLE_0:def 4;
A8: x in dom h \/ dom g & ((h +* g) | D).x = (h +* g).x by A2,A3,A4,A5,
FUNCT_1:47,XBOOLE_0:def 4;
per cases;
suppose
A9: x in dom g;
((f +* g) | D).x = (f +* g).x by A5,FUNCT_1:47
.=g.x by A6,A9,Def1;
hence ((h +* g) | D).x =((f +* g) | D).x by A8,A9,Def1;
end;
suppose
not x in dom g;
hence ((h +* g) | D).x = h.x by A8,Def1
.=((f +* g) | D).x by A1,A7,FUNCT_1:49;
end;
end;
hence thesis by A2,A4;
end;
theorem
for f,g,h being Function, D being set holds f | D =h | D implies (h +*
g) | D = (f +* g) | D
proof
let f,g,h be Function, D be set;
assume
A1: f |D = h | D;
A2: dom ((f +* g) | D) = dom (f +* g) /\ D by RELAT_1:61
.= (dom f \/ dom g) /\ D by Def1;
A3: dom ((h +* g) | D) = dom (h +* g) /\ D by RELAT_1:61
.= (dom h \/ dom g) /\ D by Def1;
then
A4: dom ((h +* g) | D) = (dom h /\ D) \/ (dom g /\ D) by XBOOLE_1:23
.= dom (f| D) \/ (dom g /\ D) by A1,RELAT_1:61
.= (dom f /\ D) \/ (dom g /\ D) by RELAT_1:61
.= (dom f \/ dom g ) /\ D by XBOOLE_1:23;
now
let x be object;
assume
A5: x in dom ((f +* g) | D);
then
A6: x in dom f \/ dom g by A2,XBOOLE_0:def 4;
A7: x in D by A2,A5,XBOOLE_0:def 4;
A8: x in dom h \/ dom g & ((h +* g) | D).x = (h +* g).x by A2,A3,A4,A5,
FUNCT_1:47,XBOOLE_0:def 4;
per cases;
suppose
A9: x in dom g;
((f +* g) | D).x = (f +* g).x by A5,FUNCT_1:47
.=g.x by A6,A9,Def1;
hence ((h +* g) | D).x =((f +* g) | D).x by A8,A9,Def1;
end;
suppose
A10: not x in dom g;
then
A11: ((h +* g) | D).x = h.x by A8,Def1
.=(h | D ).x by A7,FUNCT_1:49;
thus ((f +* g) | D).x = (f +* g).x by A5,FUNCT_1:47
.=f.x by A6,A10,Def1
.=((h +* g) | D).x by A1,A7,A11,FUNCT_1:49;
end;
end;
hence thesis by A2,A4;
end;
:: missing, 2008.03.20, A.T.
theorem Th96:
x .--> x = id{x}
proof
for y,z being object holds [y,z] in x .--> x iff y in {x} & y = z
proof
let y,z be object;
A1: x .--> x = {[x,x]} by ZFMISC_1:29;
thus [y,z] in x .--> x implies y in {x} & y = z
proof
assume [y,z] in x .--> x;
then
A2: [y,z] = [x,x] by A1,TARSKI:def 1;
then y = x by XTUPLE_0:1;
hence thesis by A2,TARSKI:def 1,XTUPLE_0:1;
end;
assume y in {x};
then y = x by TARSKI:def 1;
hence thesis by A1,TARSKI:def 1;
end;
hence thesis by RELAT_1:def 10;
end;
theorem Th97:
f c= g implies f+*g = g
proof
assume
A1: f c= g;
then f tolerates g by PARTFUN1:54;
hence f+*g = f\/ g by Th30
.= g by A1,XBOOLE_1:12;
end;
theorem Th98:
f c= g implies g+*f = g
proof
assume
A1: f c= g;
then f tolerates g by PARTFUN1:54;
hence g+*f = f\/ g by Th30
.= g by A1,XBOOLE_1:12;
end;
begin :: Changing a value in the range, 2008.03.20, A.T.
definition
let f,x,y;
func f+~(x,y) -> set equals
f+*((x .--> y)*f);
coherence;
end;
registration
let f,x,y;
cluster f+~(x,y) -> Relation-like Function-like;
coherence;
end;
theorem Th99:
for x,y being object holds
dom(f+~(x,y)) = dom f
proof let x,y be object;
thus dom(f+~(x,y)) = dom f \/ dom((x .--> y)*f) by Def1
.= dom f by RELAT_1:25,XBOOLE_1:12;
end;
theorem Th100:
for x,y being object holds
x <> y implies not x in rng(f+~(x,y))
proof let x,y be object;
assume
A1: x <> y;
assume x in rng(f+~(x,y));
then consider z being object such that
A2: z in dom(f+~(x,y)) and
A3: (f+~(x,y)).z = x by FUNCT_1:def 3;
A4: z in dom f by A2,Th99;
A5: now
assume
A6: not z in dom((x .--> y)*f);
then f.z = x by A3,Th11;
then f.z in dom(x .--> y) by FUNCOP_1:74;
hence contradiction by A4,A6,FUNCT_1:11;
end;
(x .--> y).(f.z) = ((x .--> y)*f).z by A4,FUNCT_1:13
.= x by A3,A5,Th13;
then f.z <> x by A1,FUNCOP_1:72;
then not f.z in dom(x .--> y) by FUNCOP_1:75;
hence thesis by A5,FUNCT_1:11;
end;
theorem
for x,y being object holds
x in rng f implies y in rng(f+~(x,y))
proof let x,y be object;
assume x in rng f;
then consider z being object such that
A1: z in dom f and
A2: f.z = x by FUNCT_1:def 3;
A3: dom((x .--> y)*f) c= dom(f+~(x,y)) by Th10;
x in dom(x.-->y) by FUNCOP_1:74;
then
A4: z in dom((x .--> y)*f) by A1,A2,FUNCT_1:11;
then (f+~(x,y)).z = ((x .--> y)*f).z by Th13
.= (x .--> y).(f.z) by A1,FUNCT_1:13
.= y by A2,FUNCOP_1:72;
hence thesis by A4,A3,FUNCT_1:3;
end;
theorem Th102:
for x being object holds
f+~(x,x) = f
proof let x be object;
thus f+~(x,x) = f+*((id{x})*f) by Th96
.= f by Th98,RELAT_1:50;
end;
theorem Th103:
for x,y being object holds
not x in rng f implies f+~(x,y) = f
proof let x,y be object;
assume not x in rng f;
then dom (x .--> y) misses rng f by ZFMISC_1:50;
then (x .--> y)*f = {} by RELAT_1:44;
hence thesis;
end;
theorem
for x,y being object holds
rng(f+~(x,y)) c= rng f \ {x} \/ {y}
proof let x,y be object;
per cases;
suppose
A1: not x in rng f;
then f+~(x,y) = f by Th103;
then rng(f+~(x,y)) = rng f \ {x} by A1,ZFMISC_1:57;
hence thesis by XBOOLE_1:7;
end;
suppose that
A2: x in rng f and
A3: x = y;
f+~(x,y) = f by A3,Th102;
hence thesis by A2,A3,ZFMISC_1:116;
end;
suppose that
A4: x <> y;
not x in rng(f+~(x,y)) by A4,Th100;
then
A5: rng(f+~(x,y)) \ {x} = rng(f+~(x,y)) by ZFMISC_1:57;
rng(x .--> y) = {y} by FUNCOP_1:8;
then
A6: rng f \/ rng((x .--> y)*f) c= rng f \/ {y} by RELAT_1:26,XBOOLE_1:9;
rng(f+~(x,y)) c= rng f \/ rng((x .--> y)*f) by Th17;
then rng(f+~(x,y)) c= rng f \/ {y} by A6;
then rng(f+~(x,y)) c= rng f \/ {y} \ {x} by A5,XBOOLE_1:33;
hence thesis by A4,ZFMISC_1:123;
end;
end;
theorem
for x,y,z being object holds
f.z <> x implies (f+~(x,y)).z = f.z
proof let x,y,z be object;
assume f.z <> x;
then not f.z in dom(x.-->y) by FUNCOP_1:75;
then not z in dom((x.-->y)*f) by FUNCT_1:11;
hence thesis by Th11;
end;
theorem
z in dom f & f.z = x implies (f+~(x,y)).z = y
proof
assume that
A1: z in dom f and
A2: f.z = x;
f.z in dom(x.-->y) by A2,FUNCOP_1:74;
then
A3: z in dom((x.-->y)*f) by A1,FUNCT_1:11;
hence (f+~(x,y)).z = ((x.-->y)*f).z by Th13
.= (x.-->y).x by A2,A3,FUNCT_1:12
.= y by FUNCOP_1:72;
end;
:: missing, 2008.04.06, A.T.
theorem
not x in dom f implies f c= f +*(x .--> y)
proof
assume not x in dom f;
then dom f misses {x} by ZFMISC_1:50;
then dom f misses dom(x .--> y);
hence thesis by Th32;
end;
theorem
for f being PartFunc of X,Y, x,y st x in X & y in Y holds f+*(x .--> y
) is PartFunc of X,Y
proof
let f be PartFunc of X,Y, x,y;
assume that
A1: x in X and
A2: y in Y;
A3: {x} c= X by A1,ZFMISC_1:31;
{y} c= Y by A2,ZFMISC_1:31;
then rng(x .--> y) c= Y by FUNCOP_1:8;
then
A4: rng f \/ rng(x .--> y) c= Y by XBOOLE_1:8;
rng(f+*(x .--> y)) c= rng f \/ rng(x .--> y) by Th17;
then
A5: rng(f+*(x .--> y)) c= Y by A4;
dom(f+*(x .--> y)) = dom f \/ dom(x .--> y) by Def1
.= dom f \/ {x};
hence thesis by A3,A5,RELSET_1:4,XBOOLE_1:8;
end;
:: from FINSEQ_1, 2008.05.06, A.T.
registration
let f be Function, g be non empty Function;
cluster f +* g -> non empty;
coherence
proof
dom (f+*g) = dom f \/ dom g by Def1;
hence thesis;
end;
cluster g +* f -> non empty;
coherence
proof
dom (g+*f) = dom g \/ dom f by Def1;
hence thesis;
end;
end;
:: from CIRCCOMB, 2009.01.26, A.T.
registration
let f,g be non-empty Function;
cluster f+*g -> non-empty;
coherence
proof
set h = f+*g;
A1: dom (f+*g) = dom f \/ dom g by Def1;
not {} in rng h
proof
assume {} in rng h;
then consider x being object such that
A2: x in dom (f+*g) & {} = h.x by FUNCT_1:def 3;
not x in dom g or x in dom g;
then {} = f.x & x in dom f or {} = g.x & x in dom g by A1,A2,Def1,
XBOOLE_0:def 3;
then {} in rng f or {} in rng g by FUNCT_1:def 3;
hence thesis by RELAT_1:def 9;
end;
hence thesis by RELAT_1:def 9;
end;
end;
definition let X,Y be set;
let f,g be PartFunc of X,Y;
redefine func f +* g -> PartFunc of X,Y; :: redefines +* (FUNCT_4, definition)
coherence
proof
A1: dom(f+* g) c= dom f \/ dom g by Def1;
A2: dom(f+* g) c= X by A1,XBOOLE_1:1;
A3: rng(f+* g) c= rng f \/ rng g by Th17;
rng(f+* g) c= Y by A3,XBOOLE_1:1;
then f+* g is Relation of X,Y by A2,RELSET_1:4;
hence thesis;
end;
end;
:: 2009.08.31, A.T.
reserve x for set;
theorem
dom ((x --> y)+*(x .-->z)) = succ x
proof
thus dom ((x --> y)+*(x .-->z))
= dom (x --> y) \/ dom (x .-->z) by Def1
.= x \/ dom (x .-->z)
.= x \/ {x}
.= succ x by ORDINAL1:def 1;
end;
theorem
dom ((x --> y)+*(x .-->z)+*(succ x .-->z)) = succ succ x
proof
thus dom ((x --> y)+*(x .-->z)+*(succ x .-->z))
= dom ((x --> y)+*(x .-->z)) \/ dom(succ x .-->z) by Def1
.= dom (x --> y) \/ dom (x .-->z) \/ dom(succ x .-->z) by Def1
.= x \/ dom (x .-->z) \/ dom(succ x .-->z)
.= x \/ {x} \/ dom(succ x .-->z)
.= x \/ {x} \/ {succ x}
.= succ x \/ {succ x} by ORDINAL1:def 1
.= succ succ x by ORDINAL1:def 1;
end;
:: 2009.09.08, A.T.
reserve x for object;
registration let f,g be Function-yielding Function;
cluster f+*g -> Function-yielding;
coherence
proof
let x be object;
assume x in dom(f+*g);
then
A1: x in dom f \/ dom g by Def1;
per cases by A1,XBOOLE_0:def 3;
suppose
x in dom g;
then (f+*g).x = g.x by Th13;
hence (f+*g).x is Function;
end;
suppose
x in dom f & not x in dom g;
then (f+*g).x = f.x by Th11;
hence (f+*g).x is Function;
end;
end;
end;
:: 2009.10.03, A.T.
registration
let I be set;
let f,g be I-defined Function;
cluster f+*g -> I-defined;
coherence
proof
dom (f+*g) = dom f \/ dom g by Def1;
then dom (f+*g) c= I;
hence thesis by RELAT_1:def 18;
end;
end;
registration
let I be set;
let f be total I-defined Function;
let g be I-defined Function;
cluster f+*g -> total for I-defined Function;
coherence
proof
dom f = I by PARTFUN1:def 2;
then dom (f+*g) = I \/ dom g by Def1
.= I by XBOOLE_1:12;
hence thesis;
end;
cluster g+*f -> total for I-defined Function;
coherence
proof
dom f = I by PARTFUN1:def 2;
then dom (g+*f) = I \/ dom g by Def1
.= I by XBOOLE_1:12;
hence thesis;
end;
end;
registration let I be set;
let g,h be I-valued Function;
cluster g+*h -> I-valued;
coherence
proof
A1: rng(g+*h) c= rng g \/ rng h by Th17;
rng(g+*h) c= I by A1,XBOOLE_1:1;
hence thesis by RELAT_1:def 19;
end;
end;
registration let f be Function;
let g,h be f-compatible Function;
cluster g+*h -> f-compatible;
coherence
proof
let x be object;
assume
A1: x in dom(g+*h);
A2: dom(g+*h) = dom g \/ dom h by Def1;
per cases by A1,A2,XBOOLE_0:def 3;
suppose
A3: x in dom g & not x in dom h;
then g.x in f.x by FUNCT_1:def 14;
hence (g+*h).x in f.x by A3,Th11;
end;
suppose
A4: x in dom h;
then h.x in f.x by FUNCT_1:def 14;
hence (g+*h).x in f.x by A4,Th13;
end;
end;
end;
:: missing, 2010.01.6, A.T
theorem
f|A +* f = f by Th97,RELAT_1:59;
:: from AMISTD_3, 2010.01.10, A.T
theorem
for R being Relation st dom R = {x} & rng R = {y}
holds R = x .--> y
proof let R be Relation;
assume that
A1: dom R = {x} and
A2: rng R = {y};
set g = x .--> y;
A3: g = {[x,y]} by ZFMISC_1:29;
for a, b being object holds [a,b] in R iff [a,b] in g
proof
let a, b be object;
hereby
assume
A4: [a,b] in R;
then b in rng R by XTUPLE_0:def 13;
then
A5: b = y by A2,TARSKI:def 1;
a in dom R by A4,XTUPLE_0:def 12;
then a = x by A1,TARSKI:def 1;
hence [a,b] in g by A3,A5,TARSKI:def 1;
end;
assume [a,b] in g;
then
A6: [a,b] = [x,y] by A3,TARSKI:def 1;
then
A7: b = y by XTUPLE_0:1;
a = x by A6,XTUPLE_0:1;
then a in dom R by A1,TARSKI:def 1;
then consider z being object such that
A8: [a,z] in R by XTUPLE_0:def 12;
z in rng R by A8,XTUPLE_0:def 13;
hence thesis by A2,A7,A8,TARSKI:def 1;
end;
hence thesis by RELAT_1:def 2;
end;
theorem
(f +* (x .-->y)).x = y
proof
A1: x in {x} by TARSKI:def 1;
then dom(x .--> y) = {x} & x in dom f \/ {x} by XBOOLE_0:def 3;
hence (f +* (x .-->y) ).x = (x .-->y).x by A1,Def1
.= y by FUNCOP_1:72;
end;
theorem
f +* (x .--> z1) +* (x .--> z2) = f +* (x .--> z2)
proof
A1: dom (x .--> z1) = {x}
.= dom (x .--> z2);
thus f +* (x .--> z1) +* (x .--> z2)
= f +* ((x .--> z1) +* (x .--> z2)) by Th14
.= f +* (x .--> z2) by A1,Th19;
end;
registration let A be non empty set, a,b be Element of A, x,y be set;
cluster (a,b) --> (x,y) -> A-defined;
coherence;
end;
theorem
dom g misses dom h implies f +* g +* h +* g = f +* g +* h
proof assume
A1: dom g misses dom h;
thus f +* g +* h +* g
= f +* (g +* h) +* g by Th14
.= f +* (g +* h +* g) by Th14
.= f +* (h +* g +* g) by A1,Th35
.= f +* (h +* g)
.= f +* (g +* h) by A1,Th35
.= f +* g +* h by Th14;
end;
theorem
dom f misses dom h & f c= g +* h implies f c= g
proof assume that
A1: dom f misses dom h and
A2: f c= g +* h;
A3: (g +* h)|dom f = g|dom f +* h|dom f by Th71
.= g|dom f +* {} by A1,RELAT_1:66
.= g|dom f;
f|dom f = f;
then f c= g|dom f by A2,A3,RELAT_1:76;
hence f c= g by RELAT_1:184;
end;
theorem Th117:
dom f misses dom h & f c= g implies f c= g +* h
proof assume that
A1: dom f misses dom h and
A2: f c= g;
A3: (g +* h)|dom f = g|dom f +* h|dom f by Th71
.= g|dom f +* {} by A1,RELAT_1:66
.= g|dom f;
f|dom f = f;
then f c= (g +* h)|dom f by A2,A3,RELAT_1:76;
hence f c= g +* h by RELAT_1:184;
end;
theorem
dom g misses dom h implies f +* g +* h = f +* h +* g
proof assume
A1: dom g misses dom h;
thus f +* g +* h = f +* (g +* h) by Th14
.= f +* (h +* g) by A1,Th35
.= f +* h +* g by Th14;
end;
theorem
dom f misses dom g implies (f +* g) \ g = f
proof assume
A1: dom f misses dom g;
then
A2: f misses g by RELAT_1:179;
thus (f +* g) \ g
= (f \/ g) \ g by A1,Th31
.= f by A2,XBOOLE_1:88;
end;
theorem
dom f misses dom g implies f \ g = f by RELAT_1:179,XBOOLE_1:83;
theorem
dom g misses dom h implies (f \ g) +* h = (f +* h) \ g
proof
assume
A1: dom g misses dom h;
A2: dom(f+*h) = dom f \/ dom h by Def1;
A3: dom((f\g)+*h) = dom(f\g) \/ dom h by Def1;
A4: dom((f\g)+*h) = dom((f+*h)\g)
proof
thus dom((f\g)+*h) c= dom((f+*h)\g)
proof
let x be object;
assume
A5: x in dom((f\g)+*h);
per cases by A3,A5,XBOOLE_0:def 3;
suppose that
A6: x in dom(f\g) and
A7: not x in dom h;
consider y being object such that
A8: [x,y] in f\g by A6,XTUPLE_0:def 12;
A9: x in dom f by A8,XTUPLE_0:def 12;
then
A10: x in dom(f+*h) by A2,XBOOLE_0:def 3;
A11: not [x,y] in g by A8,XBOOLE_0:def 5;
A12: (f+*h).x = f.x by A7,Th11;
reconsider y as set by TARSKI:1;
f.x = y by A8,A9,FUNCT_1:def 2;
then [x,y] in f+*h by A12,A10,FUNCT_1:def 2;
then [x,y] in (f+*h)\g by A11,XBOOLE_0:def 5;
hence thesis by XTUPLE_0:def 12;
end;
suppose
A13: x in dom h;
then
A14: not x in dom g by A1,XBOOLE_0:3;
x in dom(f+*h) by A2,A13,XBOOLE_0:def 3;
then
A15: x in dom(f+*h) \ dom g by A14,XBOOLE_0:def 5;
dom(f+*h) \ dom g c= dom((f+*h)\g) by XTUPLE_0:25;
hence thesis by A15;
end;
end;
let x be object;
assume x in dom((f+*h)\g);
then consider y being object such that
A16: [x,y] in (f+*h)\g by XTUPLE_0:def 12;
reconsider y as set by TARSKI:1;
A17: x in dom(f+*h) by A16,XTUPLE_0:def 12;
then
A18: y = (f+*h).x by A16,FUNCT_1:def 2;
per cases by A2,A17,XBOOLE_0:def 3;
suppose that
A19: x in dom f and
A20: not x in dom h;
A21: not [x,y] in g by A16,XBOOLE_0:def 5;
(f+*h).x = f.x by A20,Th11;
then [x,y] in f by A19,A18,FUNCT_1:def 2;
then [x,y] in f\g by A21,XBOOLE_0:def 5;
then x in dom(f\g) by XTUPLE_0:def 12;
hence thesis by A3,XBOOLE_0:def 3;
end;
suppose x in dom h;
hence thesis by A3,XBOOLE_0:def 3;
end;
end;
now
let x be object;
assume
A22: x in dom((f\g)+*h);
per cases by A3,A22,XBOOLE_0:def 3;
suppose that
A23: x in dom(f\g) and
A24: not x in dom h;
thus ((f\g)+*h).x = (f\g).x by A24,Th11
.= f.x by A23,GRFUNC_1:2
.= (f+*h).x by A24,Th11
.= ((f+*h)\g).x by A4,A22,GRFUNC_1:2;
end;
suppose
A25: x in dom h;
then
A26: not x in dom g by A1,XBOOLE_0:3;
x in dom(f+*h) by A25,A2,XBOOLE_0:def 3;
then x in dom(f+*h) \ dom g by A26,XBOOLE_0:def 5;
hence ((f+*h)\g).x = (f+*h).x by GRFUNC_1:32
.= h.x by A25,Th13
.= ((f\g)+*h).x by A25,Th13;
end;
end;
hence thesis by A4;
end;
theorem
for f1,f2,g1,g2 being Function
st f1 c= g1 & f2 c= g2 & dom f1 misses dom g2
holds f1 +* f2 c= g1 +* g2
proof
let f1,f2,g1,g2 be Function such that
A1: f1 c= g1 and
A2: f2 c= g2 and
A3: dom f1 misses dom g2;
A4: f1 c= g1 +* g2 by A1,A3,Th117;
g2 c= g1 +* g2 by Th25;
then f2 c= g1 +* g2 by A2;
hence f1 +* f2 c= g1 +* g2 by A4,Th87;
end;
theorem Th123:
for f, g, h being Function st f c= g holds f +* h c= g +* h
proof
let f, g, h be Function;
assume
A1: f c= g;
now
dom (f +* h) = dom f \/ dom h & dom (g +* h) = dom g \/ dom h by Def1;
hence dom (f +* h) c= dom (g +* h) by A1,RELAT_1:11,XBOOLE_1:9;
let x be object;
assume x in dom (f +* h);
then
A2: x in dom f or x in dom h by Th12;
per cases;
suppose
A3: x in dom h;
hence (f +* h).x = h.x by Th13
.= (g +* h).x by A3,Th13;
end;
suppose
A4: not x in dom h;
then (f +* h).x = f.x & (g +* h).x = g.x by Th11;
hence (f +* h).x = (g +* h).x by A1,A2,A4,GRFUNC_1:2;
end;
end;
hence thesis by GRFUNC_1:2;
end;
theorem
for f, g, h being Function st f c= g & dom f misses dom h holds f c= g +* h
proof
let f, g, h be Function;
assume f c= g;
then
A1: f +* h c= g +* h by Th123;
assume dom f misses dom h;
then f c= f +* h by Th32;
hence thesis by A1;
end;
registration
let x, y be set;
cluster x .--> y -> trivial;
coherence;
end;
:: from CIRCCOMB, 2011.04.19, A.T
theorem
for f,g,h being Function st f tolerates g & g tolerates h & h
tolerates f holds f+*g tolerates h
proof
let f,g,h be Function such that
A1: f tolerates g and
A2: g tolerates h and
A3: h tolerates f;
let x be object;
assume
A4: x in (dom (f+*g)) /\ dom h;
then x in dom (f+*g) by XBOOLE_0:def 4;
then
A5: x in dom f or x in dom g by Th12;
x in dom h by A4,XBOOLE_0:def 4;
then
x in (dom h) /\ dom f & (f+*g).x = f.x or x in (dom g) /\ dom h & (f+*g)
.x = g.x by A1,A5,Th13,Th15,XBOOLE_0:def 4;
hence thesis by A2,A3;
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 A,B be non empty set;
let f be PartFunc of [:A,A:],A;
let g be PartFunc of [:B,B:],B;
redefine func |:f,g:| -> PartFunc of [:[:A,B:],[:A,B:]:],[:A,B:]; :: redefines |: (FUNCT_4, definition)
coherence by Th59;
end;
theorem
for f being PartFunc of [:A1,A1:],A1, g being PartFunc of [:A2,A2
:],A2 for F being PartFunc of [:Y1,Y1:],Y1 st F = f||Y1 for G being PartFunc of
[:Y2,Y2:],Y2 st G = g||Y2 holds |:F,G:| = |:f,g:| ||[:Y1,Y2:]
proof
let f be PartFunc of [:A1,A1:],A1, g be PartFunc of [:A2,A2:],A2;
let F be PartFunc of [:Y1,Y1:],Y1 such that
A1: F = f||Y1;
A2: dom F c= dom f by A1,RELAT_1:60;
let G be PartFunc of [:Y2,Y2:],Y2 such that
A3: G = g||Y2;
set X = dom|:F,G:|;
A4: dom G c= dom g by A3,RELAT_1:60;
A5: X = dom(|:f,g:| ||[:Y1,Y2:])
proof
thus X c= dom(|:f,g:| ||[:Y1,Y2:])
proof
let x be object;
assume x in X;
then consider x11,x21,x12,x22 being object such that
A6: x = [[x11,x12],[x21,x22]] and
A7: [x11,x21] in dom F and
A8: [x12,x22] in dom G by Def3;
A9: x12 in Y2 by A8,ZFMISC_1:87;
A10: x22 in Y2 by A8,ZFMISC_1:87;
x21 in Y1 by A7,ZFMISC_1:87;
then
A11: [x21,x22] in [:Y1,Y2:] by A10,ZFMISC_1:87;
x11 in Y1 by A7,ZFMISC_1:87;
then [x11,x12] in [:Y1,Y2:] by A9,ZFMISC_1:87;
then
A12: x in [:[:Y1,Y2:],[:Y1,Y2:]:] by A6,A11,ZFMISC_1:87;
x in dom|:f,g:| by A2,A4,A6,A7,A8,Def3;
then x in dom|:f,g:|/\[:[:Y1,Y2:],[:Y1,Y2:]:] by A12,XBOOLE_0:def 4;
hence thesis by RELAT_1:61;
end;
let x be object;
A13: dom F = (dom f)/\[:Y1,Y1:] by A1,RELAT_1:61;
assume x in dom(|:f,g:| ||[:Y1,Y2:]);
then
A14: x in dom|:f,g:|/\[:[:Y1,Y2:],[:Y1,Y2:]:] by RELAT_1:61;
then
A15: x in [:[:Y1,Y2:],[:Y1,Y2:]:] by XBOOLE_0:def 4;
A16: dom G = (dom g)/\[:Y2,Y2:] by A3,RELAT_1:61;
x in dom|:f,g:| by A14,XBOOLE_0:def 4;
then consider x11,x21,x12,x22 being object such that
A17: x = [[x11,x12],[x21,x22]] and
A18: [x11,x21] in dom f and
A19: [x12,x22] in dom g by Def3;
A20: [x21,x22] in [:Y1,Y2:] by A17,A15,ZFMISC_1:87;
then
A21: x22 in Y2 by ZFMISC_1:87;
A22: [x11,x12] in [:Y1,Y2:] by A17,A15,ZFMISC_1:87;
then x12 in Y2 by ZFMISC_1:87;
then [x12,x22] in [:Y2,Y2:] by A21,ZFMISC_1:87;
then
A23: [x12,x22] in dom G by A19,A16,XBOOLE_0:def 4;
A24: x21 in Y1 by A20,ZFMISC_1:87;
x11 in Y1 by A22,ZFMISC_1:87;
then [x11,x21] in [:Y1,Y1:] by A24,ZFMISC_1:87;
then [x11,x21] in dom F by A18,A13,XBOOLE_0:def 4;
hence thesis by A17,A23,Def3;
end;
now
let x be set;
assume
A25: x in X;
then consider x11,x21,x12,x22 being object such that
A26: x = [[x11,x12],[x21,x22]] and
A27: [x11,x21] in dom F and
A28: [x12,x22] in dom G by Def3;
thus |:F,G:|.x = |:F,G:|.([x11,x12],[x21,x22]) by A26
.= [F.(x11,x21),G.(x12,x22)] by A27,A28,Def3
.= [f.[x11,x21],G.[x12,x22]] by A1,A27,FUNCT_1:47
.= [f.(x11,x21),g.(x12,x22)] by A3,A28,FUNCT_1:47
.= |:f,g:|.([x11,x12],[x21,x22]) by A2,A4,A27,A28,Def3
.= (|:f,g:| ||[:Y1,Y2:]).x by A5,A25,A26,FUNCT_1:47;
end;
then
A29: for x being Element of [:[:Y1,Y2:],[:Y1,Y2:]:] st x in X holds |:F,G:|.
x = (|:f,g:| ||[:Y1,Y2:]).x;
thus thesis by A5,A29;
end;
theorem
for f being Function, x,y being object st x <> y
holds f+~(x,y)+~(x,z) = f+~(x,y)
proof let f be Function,x,y be object;
assume x <> y;
then not x in rng(f+~(x,y)) by Th100;
hence f+~(x,y)+~(x,z) = f+~(x,y) by Th103;
end;
:: 28.12.2012, A.T.
:: from BORSUK_7
reserve a,b,c,x,y,z,w,d for object;
definition
let a,b,c,x,y,z be object;
func (a,b,c) --> (x,y,z) -> set equals
((a,b) --> (x,y)) +* (c .--> z);
coherence;
end;
registration
let a,b,c,x,y,z be object;
cluster (a,b,c) --> (x,y,z) -> Function-like Relation-like;
coherence;
end;
theorem Th128:
dom((a,b,c) --> (x,y,z)) = {a,b,c}
proof
A1: dom (a,b) --> (x,y) = {a,b} & dom(c .--> z) = {c} by Th62;
thus dom((a,b,c) --> (x,y,z))
= dom (a,b) --> (x,y) \/ dom(c .--> z) by Def1
.= {a,b,c} by A1, ENUMSET1:3;
end;
theorem
rng((a,b,c) --> (x,y,z)) c= {x,y,z}
proof
A1: {x,y} \/ {z} = {x,y,z} by ENUMSET1:3;
A2: rng((a,b,c) --> (x,y,z)) c= rng((a,b) --> (x,y)) \/ rng(c .--> z)
by Th17;
A3: rng(c .--> z) = {z} by FUNCOP_1:8;
rng((a,b) --> (x,y)) c= {x,y} by Th62;
then rng((a,b) --> (x,y)) \/ rng(c .--> z) c= {x,y} \/ {z}
by A3,XBOOLE_1:13;
hence thesis by A2,A1;
end;
theorem
(a,a,a) --> (x,y,z) = a .--> z
proof
thus (a,a,a) --> (x,y,z) = (a,a) --> (y,z) by Th81
.= a .--> z by Th81;
end;
theorem
(a,a,b) --> (x,y,z) = (a,b) --> (y,z) by Th81;
theorem Th132:
a <> b implies (a,b,a) --> (x,y,z) = (a,b) --> (z,y)
proof
assume
A1: a <> b;
A2: dom ((a,b,a) --> (x,y,z)) = {a,b,a} by Th128
.= {a,a,b} by ENUMSET1:57
.= {a,b} by ENUMSET1:30;
hence dom ((a,b,a) --> (x,y,z)) = dom ((a,b) --> (z,y)) by Th62;
let k be object;
assume
A3: k in dom ((a,b,a) --> (x,y,z));
per cases by A2,A3,TARSKI:def 2;
suppose
A4: k = a;
hence ((a,b,a) --> (x,y,z)).k = z by Th89
.= ((a,b) --> (z,y)).k by A1,A4,Th63;
end;
suppose
A5: k = b;
thus ((a,b,a) --> (x,y,z)).k = ((a .--> x) +* ((b,a) --> (y,z))).k
by Th14
.= y by A1,A5,Th84
.= ((a,b) --> (z,y)).k by A5,Th63;
end;
end;
theorem
(a,b,b) --> (x,y,z) = (a,b) --> (x,z)
proof
thus (a,b,b) --> (x,y,z) = (a .--> x) +* ((b,b) -->(y,z)) by Th14
.= (a,b) --> (x,z) by Th81;
end;
theorem Th134:
a <> b & a <> c implies ((a,b,c) --> (x,y,z)).a = x
proof assume that
A1: a <> b and
A2: a <> c;
not a in dom(c.-->z) by A2,TARSKI:def 1;
hence ((a,b,c) --> (x,y,z)).a = ((a,b) --> (x,y)).a by Th11
.= x by A1,Th63;
end;
theorem Th135:
(b <> c implies ((a,b,c) --> (x,y,z)).b = y) &
((a,b,c) --> (x,y,z)).c = z
proof
set f = (a,b) --> (x,y);
set g = c .--> z;
set h = (a,b,c) --> (x,y,z);
A1: c in {c} by TARSKI:def 1;
A2: dom g = {c};
hereby assume b <> c;
then
A3: not b in {c} by TARSKI:def 1;
thus h.b = f.b by A3,A2,Th11
.= y by Th63;
end;
thus h.c = g.c by A1,A2,Th13
.= z by FUNCOP_1:72;
end;
theorem
for f being Function st dom f = {a,b,c} & f.a = x & f.b = y & f.c = z holds
f = (a,b,c) --> (x,y,z)
proof
let f be Function such that
A1: dom f = {a,b,c} and
A2: f.a = x & f.b = y & f.c = z;
set g = (a,b,c) --> (x,y,z);
thus dom f = dom g by A1,Th128;
let k be object;
assume k in dom f;
then
A3: k = a or k = b or k = c by A1,ENUMSET1:def 1;
per cases;
suppose a,b,c are_mutually_distinct;
hence thesis by A2,A3,Th134,Th135;
end;
suppose
A4: a = b & a <> c;
then g = (a,c) --> (y,z) by Th81;
hence thesis by A4,A2,A3,Th63;
end;
suppose
A5: a = c;
per cases;
suppose
A6: a <> b;
then g = (a,b) --> (z,y) by A5,Th132;
hence thesis by A5,A2,A3,A6,Th63;
end;
suppose a = b;
hence thesis by A5,A2,A3,FUNCOP_1:72;
end;
end;
suppose
A7: b = c & a <> c;
thus thesis by A7,A2,A3,Th63;
end;
end;
:: from QUATERNI
definition
let x,y,w,z,a,b,c,d be object;
func (x,y,w,z) --> (a,b,c,d) -> set equals
((x,y) --> (a,b)) +* ((w,z) --> (c,d));
coherence;
end;
registration
let x,y,w,z,a,b,c,d be object;
cluster (x,y,w,z) --> (a,b,c,d) -> Function-like Relation-like;
coherence;
end;
theorem Th137:
dom (x,y,w,z) --> (a,b,c,d) = {x,y,w,z}
proof
set f=(x,y) --> (a,b), g=(w,z) --> (c,d);
A1: dom f={x,y} by Th62;
dom g={w,z} by Th62;
then dom f \/ dom g = {x,y,w,z} by A1,ENUMSET1:5;
hence thesis by Def1;
end;
theorem Th138:
rng ((x,y,w,z) --> (a,b,c,d)) c= {a,b,c,d}
proof
set f=(x,y) --> (a,b),g=(w,z) --> (c,d),
h=((x,y) --> (a,b)) +* ((w,z) --> (c,d));
A1: rng f c= {a,b} by Th62;
rng g c= {c,d} by Th62;
then rng f \/ rng g c= {a,b} \/ {c,d} by A1,XBOOLE_1:13;
then
A2: rng f \/ rng g c= {a,b,c,d} by ENUMSET1:5;
rng h c= rng f \/ rng g by Th17;
hence thesis by A2;
end;
theorem Th139:
((x,y,w,z) --> (a,b,c,d)).z=d
proof
set f=(x,y) --> (a,b),g=(w,z) --> (c,d);
A1: g.z=d by Th63;
A2: dom g = {w,z} by Th62;
z in dom g by A2,TARSKI:def 2;
hence thesis by A1,Th13;
end;
theorem Th140:
w <> z implies ((x,y,w,z) --> (a,b,c,d)).w=c
proof
assume
A1: w <> z;
A2: w<>z by A1;
set f=(x,y) --> (a,b),g=(w,z) --> (c,d);
A3: g.w=c by A2,Th63;
A4: dom g = {w,z} by Th62;
A5: w in dom g by A4,TARSKI:def 2;
thus thesis by A3,A5,Th13;
end;
theorem Th141:
y <> w & y <> z implies
((x,y,w,z) --> (a,b,c,d)).y=b
proof
assume that
A1: y<>w and
A2: y<>z;
set f=(x,y) --> (a,b),g=(w,z) --> (c,d);
A3: f.y=b by Th63;
A4: dom g = {w,z} by Th62;
A5: not y in dom g by A1,A2,A4,TARSKI:def 2;
thus thesis by A3,A5,Th11;
end;
theorem Th142:
x <> y & x <> w & x <> z implies
((x,y,w,z) --> (a,b,c,d)).x=a
proof
assume that
A1: x<>y and
A2: x<>w and
A3: x<>z;
set f=(x,y) --> (a,b),g=(w,z) --> (c,d);
A4: f.x=a by A1,Th63;
dom g = {w,z} by Th62; then
A5: not x in dom g by A2,A3,TARSKI:def 2;
thus thesis by A4,A5,Th11;
end;
theorem
x,y,w,z are_mutually_distinct implies
rng ((x,y,w,z) --> (a,b,c,d)) = {a,b,c,d}
proof
set h=(x,y,w,z) --> (a,b,c,d);
assume
A1: x,y,w,z are_mutually_distinct;
A2: rng h c= {a,b,c,d} by Th138;
{a,b,c,d} c= rng h
proof
set h=(x,y,w,z) --> (a,b,c,d);
let y1 be object;
assume y1 in {a,b,c,d}; then
A3: y1=a or y1=b or y1=c or y1=d by ENUMSET1:def 2;
A4: dom h = {x,y,w,z} by Th137;
A5: h.x=y1 or h.y=y1 or h.w=y1 or h.z=y1 by A1,A3,Th139,Th140,Th141,Th142;
A6: x in dom h by A4,ENUMSET1:def 2;
A7: y in dom h by A4,ENUMSET1:def 2;
A8: w in dom h by A4,ENUMSET1:def 2;
z in dom h by A4,ENUMSET1:def 2;
hence thesis by A5,A6,A7,A8,FUNCT_1:def 3;
end;
hence thesis by A2;
end;
theorem
for a,b,c,d,e,i,j,k being object, g being Function
st dom g = {a,b,c,d} & g.a = e & g.b = i & g.c = j & g.d=k
holds g = (a,b,c,d) --> (e,i,j,k)
proof
let a,b,c,d,e,i,j,k be object;
let h be Function such that
A1: dom h = {a,b,c,d} and
A2: h.a = e and
A3: h.b = i and
A4: h.c = j and
A5: h.d=k;
set f = (a,b) --> (e,i);
set g = (c,d) --> (j,k);
A6: dom f = {a,b} by Th62;
A7: dom g = {c,d} by Th62;
then
A8: dom h = dom f \/ dom g by A1,A6,ENUMSET1:5;
now
let x be object such that
A9: x in dom f \/ dom g;
thus x in dom g implies h.x = g.x
proof
assume
A10: x in dom g;
per cases by A7,A10,TARSKI:def 2;
suppose x=c & c <> d;
hence thesis by A4,Th63;
end;
suppose x=d;
hence thesis by A5,Th63;
end;
end;
thus not x in dom g implies h.x = f.x
proof
assume not x in dom g;
then
A11: x in dom f by A9,XBOOLE_0:def 3;
per cases by A6,A11,TARSKI:def 2;
suppose x=a & a <> b;
hence thesis by A2,Th63;
end;
suppose x=b;
hence thesis by A3,Th63;
end;
end;
end;
hence thesis by A8,Def1;
end;
theorem
for a,c,b,d,x,y,z,w being object holds
a,c,x,w are_mutually_distinct
implies (a,c,x,w) --> (b,d,y,z) = { [a,b], [c,d],[x,y],[w,z] }
proof
let a,c,b,d,x,y,z,w be object;
assume
A1: a,c,x,w are_mutually_distinct;
then
A2: a <> c;
A3: a <> x by A1;
A4: a <> w by A1;
A5: c <> x by A1;
A6: c <> w by A1;
A7: x<>w by A1;
set m=(a,c) --> (b,d), n = (x,w) --> (y,z);
A8: dom m = {a,c} by Th62;
A9: dom n = {x,w} by Th62;
A10: not a in {x,w} by A3,A4,TARSKI:def 2;
not c in {x,w} by A5,A6,TARSKI:def 2;
then (a,c,x,w) --> (b,d,y,z) = m \/ n by A8,A9,A10,Th31,ZFMISC_1:51
.={ [a,b], [c,d] } \/ n by A2,Th67
.={ [a,b], [c,d] } \/ {[x,y],[w,z]} by A7,Th67
.={ [a,b], [c,d], [x,y],[w,z]} by ENUMSET1:5;
hence thesis;
end;
theorem
for a,b,c,d,x,y,z,w,x9,y9,z9,w9 being object
st a,b,c,d are_mutually_distinct &
(a,b,c,d) --> (x,y,z,w) = (a,b,c,d) --> (x9,y9,z9,w9)
holds x = x9 & y = y9 & z=z9 & w=w9
proof
let a,b,c,d,x,y,z,w,x9,y9,z9,w9 be object such that
A1: a,b,c,d are_mutually_distinct and
A2: (a,b,c,d) --> (x,y,z,w) = (a,b,c,d) --> (x9,y9,z9,w9);
A3: x=((a,b,c,d) --> (x,y,z,w)).a by A1,Th142
.=x9 by A1,A2,Th142;
A4: y=((a,b,c,d) --> (x,y,z,w)).b by A1,Th141
.=y9 by A1,A2,Th141;
A5: z=((a,b,c,d) --> (x,y,z,w)).c by A1,Th140
.=z9 by A1,A2,Th140;
w=((a,b,c,d) --> (x,y,z,w)).d by Th139
.=w9 by A2,Th139;
hence thesis by A3,A4,A5;
end;
:: from AOFA_A00
theorem
for a1,a2,a3,b1,b2,b3 being object
st a1,a2,a3 are_mutually_distinct
holds
rng ((a1,a2,a3)-->(b1,b2,b3)) = {b1,b2,b3}
proof
let a1,a2,a3,b1,b2,b3 be object;
assume
A1: a1,a2,a3 are_mutually_distinct;
set f = (a1,a2,a3)-->(b1,b2,b3);
thus rng (f) c= {b1,b2,b3}
proof
let x be object; assume x in rng f; then
consider y being object such that
A2: y in dom f & x = f.y by FUNCT_1:def 3;
dom f = {a1,a2,a3} by Th128; then
y = a1 or y = a2 or y = a3 by A2,ENUMSET1:def 1; then
x = b1 or x = b2 or x = b3 by A2,A1,Th134,Th135;
hence thesis by ENUMSET1:def 1;
end;
let x be object; assume x in {b1,b2,b3}; then
A3: x = b1 or x = b2 or x = b3 by ENUMSET1:def 1;
A4: a1 in {a1,a2,a3} & a2 in {a1,a2,a3} & a3 in {a1,a2,a3} by ENUMSET1:def 1;
A5: dom f = {a1,a2,a3} by Th128;
f.a1 = b1 & f.a2 = b2 & f.a3 = b3 by A1,Th134,Th135;
hence thesis by A3,A4,A5,FUNCT_1:def 3;
end;
definition
let C,D,E be non empty set;
let f be Function of [:C,D:],E;
redefine func ~f -> Function of [:D,C:],E means :: redefines ~ (FUNCT_4, definition)
for d being Element of D, c being Element of C holds it.(d,c) = f.(c,d);
coherence
proof
thus ~f is Function of [:D,C:],E;
end;
compatibility
proof
let g be Function of [:D,C:],E;
A1: dom(g) = [:D,C:] by FUNCT_2:def 1;
hence g = ~f implies
for d being Element of D, c being Element of C holds g.(d,c) = f.(c,d)
by ZFMISC_1:87,Th43;
assume
A3: for d being Element of D, c being Element of C holds g.(d,c) = f.(c,d);
thus
A6: dom g = dom ~f by A1,FUNCT_2:def 1;
let x be object;
assume x in dom g;
then consider d being Element of D, c being Element of C such that
A4: x = [d,c] by SUBSET_1:43;
thus g.x = g.(d,c) by A4
.= f.(c,d) by A3
.= (~f).(d,c) by A1,A6,ZFMISC_1:87,Th43
.= (~f).x by A4;
end;
end;