:: Curried and Uncurried Functions
:: by Grzegorz Bancerek
::
:: Received March 6, 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 FUNCT_1, RELAT_1, XBOOLE_0, ZFMISC_1, TARSKI, SUBSET_1, MCART_1,
FUNCT_2, PARTFUN1, CARD_1, FUNCOP_1, FUNCT_4, BINOP_1, FUNCT_5;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1, FUNCT_1,
DOMAIN_1, WELLORD2, ORDINAL1, RELSET_1, FUNCT_2, MCART_1, BINOP_1,
PARTFUN1, FUNCT_3, CARD_1, FUNCOP_1, FUNCT_4;
constructors PARTFUN1, WELLORD2, BINOP_1, FUNCT_3, FUNCOP_1, FUNCT_4, CARD_1,
RELSET_1, DOMAIN_1, XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, XTUPLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI, FUNCT_1, WELLORD2, XBOOLE_0, FUNCOP_1;
equalities BINOP_1, FUNCOP_1;
expansions TARSKI, FUNCT_1, WELLORD2, XBOOLE_0;
theorems TARSKI, ZFMISC_1, FUNCT_1, WELLORD2, FUNCT_2, MCART_1, FUNCT_3,
RELAT_1, CARD_1, PARTFUN1, FUNCOP_1, FUNCT_4, ENUMSET1, XBOOLE_0,
XBOOLE_1, RELSET_1, XTUPLE_0;
schemes FUNCT_1, PARTFUN1, XBOOLE_0;
begin
reserve X,Y,Z,X1,X2,Y1,Y2 for set, x,y,z,t,x1,x2 for object,
f,g,h,f1,f2,g1,g2 for Function;
scheme
LambdaFS { FS()->set, f(object)-> object }:
ex f st dom f = FS() & for g st g in FS () holds f.g = f(g);
consider f such that
A1: dom f = FS() &
for x being object st x in FS() holds f.x = f(x) from FUNCT_1:sch
3;
take f;
thus thesis by A1;
end;
theorem Th1:
~{} = {}
proof
[:{} qua set,{}:] = {} & dom {} = {} by ZFMISC_1:90;
then dom ~{} = {} by FUNCT_4:46;
hence thesis;
end;
::$CT 6
theorem Th2:
proj1 {} = {} & proj2 {} = {};
theorem Th3:
Y <> {} or [:X,Y:] <> {} or [:Y,X:] <> {} implies proj1 [:X,Y:]
= X & proj2 [:Y,X:] = X
proof
set y = the Element of Y;
assume Y <> {} or [:X,Y:] <> {} or [:Y,X:] <> {};
then
A1: Y <> {} by ZFMISC_1:90;
now
let x be object;
x in X implies [x,y] in [:X,Y:] by A1,ZFMISC_1:87;
hence x in X iff ex y being object st [x,y] in [:X,Y:] by ZFMISC_1:87;
end;
hence proj1 [:X,Y:] = X by XTUPLE_0:def 12;
now
let x be object;
x in X implies [y,x] in [:Y,X:] by A1,ZFMISC_1:87;
hence x in X iff ex y being object st [y,x] in [:Y,X:] by ZFMISC_1:87;
end;
hence thesis by XTUPLE_0:def 13;
end;
theorem Th4:
proj1 [:X,Y:] c= X & proj2 [:X,Y:] c= Y
proof
thus proj1 [:X,Y:] c= X
proof
let x be object;
assume x in proj1 [:X,Y:];
then ex y being object st [x,y] in [:X,Y:] by XTUPLE_0:def 12;
hence thesis by ZFMISC_1:87;
end;
let y be object;
assume y in proj2 [:X,Y:];
then ex x being object st [x,y] in [:X,Y:] by XTUPLE_0:def 13;
hence thesis by ZFMISC_1:87;
end;
theorem Th5:
Z c= [:X,Y:] implies proj1 Z c= X & proj2 Z c= Y
proof
assume Z c= [:X,Y:];
then
A1: proj1 Z c= proj1 [:X,Y:] & proj2 Z c= proj2 [:X,Y:] by XTUPLE_0:8,9;
proj1 [:X,Y:] c= X & proj2 [:X,Y:] c= Y by Th4;
hence thesis by A1;
end;
theorem Th6:
proj1 {[x,y]} = {x} & proj2 {[x,y]} = {y}
proof
thus proj1 {[x,y]} c= {x}
proof
let z be object;
assume z in proj1 {[x,y]};
then consider t being object such that
A1: [z,t] in {[x,y]} by XTUPLE_0:def 12;
[z,t] = [x,y] by A1,TARSKI:def 1;
then z = x by XTUPLE_0:1;
hence thesis by TARSKI:def 1;
end;
thus {x} c= proj1 {[x,y]}
proof
let z be object;
assume z in {x};
then z = x by TARSKI:def 1;
then [z,y] in {[x,y]} by TARSKI:def 1;
hence thesis by XTUPLE_0:def 12;
end;
thus proj2 {[x,y]} c= {y}
proof
let z be object;
assume z in proj2 {[x,y]};
then consider t being object such that
A2: [t,z] in {[x,y]} by XTUPLE_0:def 13;
[t,z] = [x,y] by A2,TARSKI:def 1;
then z = y by XTUPLE_0:1;
hence thesis by TARSKI:def 1;
end;
thus {y} c= proj2 {[x,y]}
proof
let z be object;
assume z in {y};
then z = y by TARSKI:def 1;
then [x,z] in {[x,y]} by TARSKI:def 1;
hence thesis by XTUPLE_0:def 13;
end;
end;
theorem
proj1 {[x,y],[z,t]} = {x,z} & proj2 {[x,y],[z,t]} = {y,t}
proof
A1: proj2 {[x,y]} = {y} & proj2 {[z,t]} = {t} by Th6;
{[x,y],[z,t]} = {[x,y]} \/ {[z,t]} by ENUMSET1:1;
then
A2: proj1 {[x,y],[z,t]} = proj1 {[x,y]} \/ proj1 {[z,t]} & proj2 {[x,y],[z,t
]} = proj2 {[x,y]} \/ proj2 {[z,t]} by XTUPLE_0:23,27;
proj1 {[x,y]} = {x} & proj1 {[z,t]} = {z} by Th6;
hence thesis by A2,A1,ENUMSET1:1;
end;
theorem Th8:
not (ex x,y being object st [x,y] in X)
implies proj1 X = {} & proj2 X = {}
proof
set x = the Element of proj2 X;
assume
A1: not (ex x,y being object st [x,y] in X);
hereby
set x = the Element of proj1 X;
assume proj1 X <> {};
then ex y being object st [x,y] in X by XTUPLE_0:def 12;
hence contradiction by A1;
end;
assume proj2 X <> {};
then ex y being object st [y,x] in X by XTUPLE_0:def 13;
hence thesis by A1;
end;
theorem
proj1 X = {} or proj2 X = {} implies
not ex x,y being object st [x,y] in X by
XTUPLE_0:def 12,def 13;
theorem
proj1 X = {} iff proj2 X = {}
proof
proj1 X = {} or proj2 X = {} implies
not ex x,y being object st [x,y] in X by
XTUPLE_0:def 12,def 13;
hence thesis by Th8;
end;
theorem Th11:
proj1 dom f = proj2 dom ~f & proj2 dom f = proj1 dom ~f
proof
thus proj1 dom f c= proj2 dom ~f
proof
let x be object;
assume x in proj1 dom f;
then consider y being object such that
A1: [x,y] in dom f by XTUPLE_0:def 12;
[y,x] in dom ~f by A1,FUNCT_4:42;
hence thesis by XTUPLE_0:def 13;
end;
thus proj2 dom ~f c= proj1 dom f
proof
let y be object;
assume y in proj2 dom ~f;
then consider x being object such that
A2: [x,y] in dom ~f by XTUPLE_0:def 13;
[y,x] in dom f by A2,FUNCT_4:42;
hence thesis by XTUPLE_0:def 12;
end;
thus proj2 dom f c= proj1 dom ~f
proof
let y be object;
assume y in proj2 dom f;
then consider x being object such that
A3: [x,y] in dom f by XTUPLE_0:def 13;
[y,x] in dom ~f by A3,FUNCT_4:42;
hence thesis by XTUPLE_0:def 12;
end;
thus proj1 dom ~f c= proj2 dom f
proof
let x be object;
assume x in proj1 dom ~f;
then consider y being object such that
A4: [x,y] in dom ~f by XTUPLE_0:def 12;
[y,x] in dom f by A4,FUNCT_4:42;
hence thesis by XTUPLE_0:def 13;
end;
end;
definition
let f;
func curry f -> Function means
:Def1:
dom it = proj1 dom f & for x being object st x in
proj1 dom f ex g st it.x = g & dom g = proj2 (dom f /\ [:{x},proj2 dom f:]) &
for y st y in dom g holds g.y = f.(x,y);
existence
proof
defpred F[object,Function] means
dom $2 = proj2 (dom f /\ [:{$1},proj2 dom f
:]) & for y st y in dom $2 holds $2.y = f.($1,y);
defpred P[object,object] means ex g st $2 = g & F[ $1,g];
A1: for x,y,z being object st x in proj1 dom f & P[x,y] & P[x,z] holds y = z
proof
let x,y,z be object such that
x in proj1 dom f;
given g1 being Function such that
A2: y = g1 and
A3: F[x,g1];
given g2 being Function such that
A4: z = g2 and
A5: F[x,g2];
now
let t be object;
assume
A6: t in proj2 (dom f /\ [:{x},proj2 dom f:]);
then g1.t = f.(x,t) by A3;
hence g1.t = g2.t by A5,A6;
end;
hence thesis by A2,A3,A4,A5,FUNCT_1:2;
end;
A7: for x being object st x in proj1 dom f ex y being object st P[x,y]
proof
let x being object such that
x in proj1 dom f;
deffunc F(object) = f.[x,$1];
consider g such that
A8: dom g = proj2 (dom f /\ [:{x},proj2 dom f:]) &
for y being object st y in
proj2 (dom f /\ [:{x},proj2 dom f:]) holds g.y = F(y) from FUNCT_1:sch 3;
reconsider y = g as set;
take A=y,B=g;
thus thesis by A8;
end;
ex g being Function st dom g = proj1 dom f &
for x being object st x in proj1 dom
f holds P[x,g.x] from FUNCT_1:sch 2(A1,A7);
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function such that
A9: dom f1 = proj1 dom f and
A10: for x being object st x in proj1 dom f
ex g st f1.x = g & dom g = proj2 (dom f
/\ [:{x},proj2 dom f:]) & for y st y in dom g holds g.y = f.(x,y) and
A11: dom f2 = proj1 dom f and
A12: for x being object st x in proj1 dom f
ex g st f2.x = g & dom g = proj2 (dom f
/\ [:{x},proj2 dom f:]) & for y st y in dom g holds g.y = f.(x,y);
now
let x be object;
assume
A13: x in proj1 dom f;
then consider g1 being Function such that
A14: f1.x = g1 and
A15: dom g1 = proj2 (dom f /\ [:{x},proj2 dom f:]) and
A16: for y st y in dom g1 holds g1.y = f.(x,y) by A10;
consider g2 being Function such that
A17: f2.x = g2 and
A18: dom g2 = proj2 (dom f /\ [:{x},proj2 dom f:]) and
A19: for y st y in dom g2 holds g2.y = f.(x,y) by A12,A13;
now
let y be object;
assume
A20: y in proj2 (dom f /\ [:{x},proj2 dom f:]);
then g1.y = f.(x,y) by A15,A16;
hence g1.y = g2.y by A18,A19,A20;
end;
hence f1.x = f2.x by A14,A15,A17,A18,FUNCT_1:2;
end;
hence thesis by A9,A11;
end;
func uncurry f -> Function means
: Def2:
(for t being object holds t in dom it iff ex x,g
,y st t = [x,y] & x in dom f & g = f.x & y in dom g) & for x,g st x in dom it &
g = f.x`1 holds it.x = g.x`2;
existence
proof
defpred Q[object,object] means ex g st g = f.$1`1 & $2 = g.$1`2;
deffunc F(Function) = dom $1;
defpred P[object] means f.$1 is Function;
consider X such that
A21: for x being object holds x in X iff x in dom f & P[ x ]
from XBOOLE_0:sch 1;
defpred P[object] means for g1 st g1 = f.$1`1 holds $1`2 in dom g1;
consider g such that
A22: dom g = f.:X & for g1 st g1 in f.:X holds g.g1 = F(g1) from
LambdaFS;
consider Y such that
A23: for x being object holds x in Y iff x in [:X,union rng g:] & P[ x ]
from XBOOLE_0:sch 1;
A24: for x being object st x in Y ex y being object st Q[x,y]
proof
let x be object;
assume x in Y;
then x in [:X,union rng g:] by A23;
then x`1 in X by MCART_1:10;
then reconsider h = f.x`1 as Function by A21;
take h.x`2,h;
thus thesis;
end;
A25: for x,x1,x2 being object st x in Y & Q[x,x1] & Q[x,x2] holds x1 = x2;
consider F being Function such that
A26: dom F = Y &
for x being object st x in Y holds Q[x,F.x] from FUNCT_1:sch 2(A25
,A24);
take F;
thus for t being object holds
t in dom F iff ex x,g,y st t = [x,y] & x in dom f & g = f
.x & y in dom g
proof
let t be object;
thus t in dom F implies ex x,g,y st t = [x,y] & x in dom f & g = f.x & y
in dom g
proof
assume
A27: t in dom F;
take x = t`1;
t in [:X,union rng g:] by A23,A26,A27;
then
A28: x in X by MCART_1:10;
then reconsider h = f.x as Function by A21;
take h, t`2;
thus thesis by A21,A23,A26,A27,A28,MCART_1:21;
end;
given x be object, h be Function, y be object such that
A29: t = [x,y] and
A30: x in dom f and
A31: h = f.x and
A32: y in dom h;
A33: x in X by A21,A30,A31;
then h in f.:X by A30,A31,FUNCT_1:def 6;
then g.h = dom h & g.h in rng g by A22,FUNCT_1:def 3;
then dom h c= union rng g by ZFMISC_1:74;
then
A34: t in [:X,union rng g:] by A29,A32,A33,ZFMISC_1:87;
for g1 st g1 = f.t`1 holds t`2 in dom g1 by A29,A31,A32;
hence thesis by A23,A26,A34;
end;
let x;
let h be Function;
assume that
A35: x in dom F and
A36: h = f.x`1;
ex g st g = f.x`1 & F.x = g.x`2 by A26,A35;
hence thesis by A36;
end;
uniqueness
proof
defpred P[object] means
ex x,g,y st $1 = [x,y] & x in dom f & g = f.x & y in
dom g;
let f1,f2;
assume that
A37: for t being object holds t in dom f1 iff P[t] and
A38: for x,g st x in dom f1 & g = f.x`1 holds f1.x = g.x`2 and
A39: for t being object holds t in dom f2 iff P[t] and
A40: for x,g st x in dom f2 & g = f.x`1 holds f2.x = g.x`2;
A41: dom f1 = dom f2 from XBOOLE_0:sch 2(A37,A39);
now
let x be object;
assume
A42: x in dom f1;
then consider z,g,y such that
A43: x = [z,y] and
z in dom f and
A44: g = f.z and
y in dom g by A37;
A45: z = x`1 & y = x`2 by A43;
then f1.x = g.y by A38,A42,A44;
hence f1.x = f2.x by A40,A41,A42,A44,A45;
end;
hence thesis by A41;
end;
end;
definition
let f;
func curry' f -> Function equals
curry ~f;
correctness;
func uncurry' f -> Function equals
~(uncurry f);
correctness;
end;
::$CT
registration let f;
cluster curry f -> Function-yielding;
coherence
proof let x be object;
assume x in dom curry f;
then
A1: x in proj1 dom f by Def1;
ex g st (curry f).x = g & dom g = proj2 (dom f /\ [:{x},proj2 dom f:]) &
for y st y in dom g holds g.y = f.(x,y) by A1,Def1;
hence thesis;
end;
end;
theorem Th12:
for x,y being object holds
[x,y] in dom f implies x in dom curry f
proof let x,y be object;
assume [x,y] in dom f;
then
x in proj1 dom f by XTUPLE_0:def 12;
hence x in dom curry f by Def1;
end;
theorem Th13:
for x,y being object holds
[x,y] in dom f & g = (curry f).x implies y in dom g & g.y = f.(x ,y)
proof let x,y be object;
assume that
A1: [x,y] in dom f and
A2: g = (curry f).x;
x in proj1 dom f by A1,XTUPLE_0:def 12;
then
A3: ex h st (curry f).x = h & dom h = proj2 (dom f /\ [:{x},proj2 dom f :])
& for y st y in dom h holds h.y = f.(x,y) by Def1;
y in proj2 dom f by A1,XTUPLE_0:def 13;
then [x,y] in [:{x},proj2 dom f:] by ZFMISC_1:105;
then [x,y] in dom f /\ [:{x},proj2 dom f:] by A1,XBOOLE_0:def 4;
hence y in dom g by A2,A3,XTUPLE_0:def 13;
hence thesis by A2,A3;
end;
registration let f;
cluster curry' f -> Function-yielding;
coherence;
end;
theorem
for x,y being object holds
[x,y] in dom f implies y in dom curry' f
proof let x,y be object;
assume [x,y] in dom f;
then [y,x] in dom ~f by FUNCT_4:42;
then y in dom curry' f by Th12;
hence thesis;
end;
theorem Th15:
for x,y being object holds
[x,y] in dom f & g = (curry' f).y implies x in dom g & g.x = f.(x,y)
proof let x,y be object;
assume [x,y] in dom f;
then
A1: [y,x] in dom ~f by FUNCT_4:42;
assume
A2: g = (curry' f).y;
then g.x = (~f).(y,x) by A1,Th13;
hence thesis by A1,A2,Th13,FUNCT_4:43;
end;
theorem
dom curry' f = proj2 dom f
proof
dom curry ~f = proj1 dom ~f by Def1;
hence thesis by Th11;
end;
theorem Th17:
[:X,Y:] <> {} & dom f = [:X,Y:] implies dom curry f = X & dom curry' f = Y
proof
assume that
A1: [:X,Y:] <> {} and
A2: dom f = [:X,Y:];
dom curry f = proj1 dom f by Def1;
hence dom curry f = X by A1,A2,Th3;
thus dom curry' f = proj1 dom ~f by Def1
.= proj1 [:Y,X:] by A2,FUNCT_4:46
.= Y by A1,Th3;
end;
theorem Th18:
dom f c= [:X,Y:] implies dom curry f c= X & dom curry' f c= Y
proof
assume
A1: dom f c= [:X,Y:];
dom curry f = proj1 dom f by Def1;
hence dom curry f c= X by A1,Th5;
A2: dom curry' f = proj1 dom ~f by Def1;
dom ~f c= [:Y,X:] by A1,FUNCT_4:45;
hence thesis by A2,Th5;
end;
theorem Th19:
rng f c= Funcs(X,Y) implies dom uncurry f = [:dom f,X:] & dom
uncurry' f = [:X,dom f:]
proof
defpred P[object] means
ex x,g,y st $1 = [x,y] & x in dom f & g = f.x & y in dom g;
assume
A1: rng f c= Funcs(X,Y);
A2: for t being object holds t in [:dom f,X:] iff P[t]
proof let t be object;
thus t in [:dom f,X:] implies ex x,g,y st t = [x,y] & x in dom f & g = f.x
& y in dom g
proof
assume
A3: t in [:dom f,X:];
then t`1 in dom f by MCART_1:10;
then f.t`1 in rng f by FUNCT_1:def 3;
then consider g such that
A4: f.t`1 = g & dom g = X and
rng g c= Y by A1,FUNCT_2:def 2;
take t`1, g, t`2;
thus thesis by A3,A4,MCART_1:10,21;
end;
given x,g,y such that
A5: t = [x,y] and
A6: x in dom f and
A7: g = f.x and
A8: y in dom g;
g in rng f by A6,A7,FUNCT_1:def 3;
then ex g1 st g = g1 & dom g1 = X & rng g1 c= Y by A1,FUNCT_2:def 2;
hence thesis by A5,A6,A8,ZFMISC_1:87;
end;
A9: for t being object holds t in dom uncurry f iff P[t] by Def2;
thus dom uncurry f = [:dom f,X:] from XBOOLE_0:sch 2(A9,A2);
hence thesis by FUNCT_4:46;
end;
theorem
not (ex x,y being object st [x,y] in dom f)
implies curry f = {} & curry' f = {}
proof
assume
A1: not ex x,y being object st [x,y] in dom f;
then proj1 dom f = {} by Th8;
then dom curry f = {} by Def1;
hence curry f = {};
now
let x,y be object;
assume [x,y] in dom ~f;
then [y,x] in dom f by FUNCT_4:42;
hence contradiction by A1;
end;
then proj1 dom ~f = {} by Th8;
then dom curry ~f = {} by Def1;
hence thesis;
end;
theorem
not (ex x st x in dom f & f.x is Function) implies uncurry f = {} &
uncurry' f = {}
proof
assume
A1: not (ex x st x in dom f & f.x is Function);
A2: now
set t = the Element of dom uncurry f;
assume dom uncurry f <> {};
then ex x,g,y st t = [x,y] & x in dom f & g = f.x & y in dom g by Def2;
hence contradiction by A1;
end;
hence uncurry f = {};
thus thesis by A2,Th1,RELAT_1:41;
end;
theorem Th22:
[:X,Y:] <> {} & dom f = [:X,Y:] & x in X implies ex g st (curry
f).x = g & dom g = Y & rng g c= rng f & for y st y in Y holds g.y = f.(x,y)
proof
assume that
A1: [:X,Y:] <> {} and
A2: dom f = [:X,Y:] and
A3: x in X;
{x} c= X by A3,ZFMISC_1:31;
then
A4: [:{x},Y:] /\ dom f = [:{x},Y:] by A2,ZFMISC_1:101;
x in proj1 dom f by A1,A2,A3,Th3;
then consider g such that
A5: (curry f).x = g and
A6: dom g = proj2 (dom f /\ [:{x},proj2 dom f:]) & for y st y in dom g
holds g.y = f.(x,y) by Def1;
take g;
A7: proj2 [:{x},Y:] = Y by Th3;
A8: proj2 dom f = Y by A2,A3,Th3;
rng g c= rng f
proof
let z be object;
assume z in rng g;
then consider y being object such that
A9: y in dom g & z = g.y by FUNCT_1:def 3;
[x,y] in dom f & z = f.(x,y) by A2,A3,A6,A8,A4,A7,A9,ZFMISC_1:87;
hence thesis by FUNCT_1:def 3;
end;
hence thesis by A5,A6,A8,A4,A7;
end;
theorem Th23:
x in dom curry f implies (curry f).x is Function
proof
assume
A1: x in dom curry f;
dom curry f = proj1 dom f by Def1;
then
ex g st (curry f).x = g & dom g = proj2 (dom f /\ [:{x},proj2 dom f:] )
& for y st y in dom g holds g.y = f.(x,y) by A1,Def1;
hence thesis;
end;
theorem Th24:
x in dom curry f & g = (curry f).x implies dom g = proj2 (dom f
/\ [:{x},proj2 dom f:]) & dom g c= proj2 dom f & rng g c= rng f & for y st y in
dom g holds g.y = f.(x,y) & [x,y] in dom f
proof
assume that
A1: x in dom curry f and
A2: g = (curry f).x;
dom curry f = proj1 dom f by Def1;
then consider h such that
A3: (curry f).x = h and
A4: dom h = proj2 (dom f /\ [:{x},proj2 dom f:]) and
A5: for y st y in dom h holds h.y = f.(x,y) by A1,Def1;
thus dom g = proj2 (dom f /\ [:{x},proj2 dom f:]) by A2,A3,A4;
dom f /\ [:{x},proj2 dom f:] c= dom f by XBOOLE_1:17;
hence dom g c= proj2 dom f by A2,A3,A4,XTUPLE_0:9;
thus rng g c= rng f
proof
let y be object;
assume y in rng g;
then consider z being object such that
A6: z in dom g and
A7: y = g.z by FUNCT_1:def 3;
consider t being object such that
A8: [t,z] in dom f /\ [:{x},proj2 dom f:] by A2,A3,A4,A6,XTUPLE_0:def 13;
[t,z] in dom f & [t,z] in [:{x},proj2 dom f:] by A8,XBOOLE_0:def 4;
then
A9: [x,z] in dom f by ZFMISC_1:105;
h.z = f.(x,z) by A2,A3,A5,A6;
hence thesis by A2,A3,A7,A9,FUNCT_1:def 3;
end;
let y;
assume
A10: y in dom g;
then consider t being object such that
A11: [t,y] in dom f /\ [:{x},proj2 dom f:] by A2,A3,A4,XTUPLE_0:def 13;
[t,y] in dom f & [t,y] in [:{x},proj2 dom f:] by A11,XBOOLE_0:def 4;
hence thesis by A2,A3,A5,A10,ZFMISC_1:105;
end;
theorem Th25:
[:X,Y:] <> {} & dom f = [:X,Y:] & y in Y implies ex g st (curry'
f).y = g & dom g = X & rng g c= rng f & for x st x in X holds g.x = f.(x,y)
proof
assume that
A1: [:X,Y:] <> {} and
A2: dom f = [:X,Y:] and
A3: y in Y;
A4: dom ~f = [:Y,X:] by A2,FUNCT_4:46;
X <> {} by A1,ZFMISC_1:90;
then consider g such that
A5: (curry ~f).y = g & dom g = X & rng g c= rng ~f and
A6: for x st x in X holds g.x = (~f).(y,x) by A3,A4,Th22;
take g;
rng ~f c= rng f by FUNCT_4:41;
hence (curry' f).y = g & dom g = X & rng g c= rng f by A5;
let x;
assume
A7: x in X;
then
A8: g.x = (~f).(y,x) by A6;
[y,x] in dom ~f by A3,A4,A7,ZFMISC_1:87;
hence thesis by A8,FUNCT_4:43;
end;
theorem
x in dom curry' f implies (curry' f).x is Function by Th23;
theorem
x in dom curry' f & g = (curry' f).x implies dom g = proj1 (dom f /\
[:proj1 dom f,{x}:]) & dom g c= proj1 dom f & rng g c= rng f & for y st y in
dom g holds g.y = f.(y,x) & [y,x] in dom f
proof
A1: rng ~f c= rng f by FUNCT_4:41;
assume
A2: x in dom curry' f & g = (curry' f).x;
then dom g = proj2 (dom ~f /\ [:{x},proj2 dom ~f:]) by Th24;
then
A3: dom g = proj2 (dom ~f /\ [:{x},proj1 dom f:]) by Th11;
thus
A4: dom g c= proj1 (dom f /\ [:proj1 dom f,{x}:])
proof
let z be object;
assume z in dom g;
then consider y being object such that
A5: [y,z] in dom ~f /\ [:{x},proj1 dom f:] by A3,XTUPLE_0:def 13;
[y,z] in [:{x},proj1 dom f:] by A5,XBOOLE_0:def 4;
then
A6: [z,y] in [:proj1 dom f,{x}:] by ZFMISC_1:88;
[y,z] in dom ~f by A5,XBOOLE_0:def 4;
then [z,y] in dom f by FUNCT_4:42;
then [z,y] in dom f /\ [:proj1 dom f,{x}:] by A6,XBOOLE_0:def 4;
hence thesis by XTUPLE_0:def 12;
end;
thus proj1 (dom f /\ [:proj1 dom f,{x}:]) c= dom g
proof
let z be object;
assume z in proj1 (dom f /\ [:proj1 dom f,{x}:]);
then consider y being object such that
A7: [z,y] in dom f /\ [:proj1 dom f,{x}:] by XTUPLE_0:def 12;
[z,y] in [:proj1 dom f,{x}:] by A7,XBOOLE_0:def 4;
then
A8: [y,z] in [:{x},proj1 dom f:] by ZFMISC_1:88;
[z,y] in dom f by A7,XBOOLE_0:def 4;
then [y,z] in dom ~f by FUNCT_4:42;
then [y,z] in dom ~f /\ [:{x},proj1 dom f:] by A8,XBOOLE_0:def 4;
hence thesis by A3,XTUPLE_0:def 13;
end;
dom g c= proj2 dom ~f & rng g c= rng ~f by A2,Th24;
hence dom g c= proj1 dom f & rng g c= rng f by A1,Th11;
let y;
assume
A9: y in dom g;
then consider z being object such that
A10: [y,z] in dom f /\ [:proj1 dom f,{x}:] by A4,XTUPLE_0:def 12;
[y,z] in [:proj1 dom f,{x}:] by A10,XBOOLE_0:def 4;
then
A11: z = x by ZFMISC_1:106;
[y,z] in dom f by A10,XBOOLE_0:def 4;
then [z,y] in dom ~f by FUNCT_4:42;
then (~f).(x,y) = f.(y,x) by A11,FUNCT_4:43;
hence thesis by A2,A9,A10,A11,Th24,XBOOLE_0:def 4;
end;
theorem Th28:
dom f = [:X,Y:] implies rng curry f c= Funcs(Y,rng f) & rng
curry' f c= Funcs(X,rng f)
proof
assume
A1: dom f = [:X,Y:];
A2: now
assume
A3: [:X,Y:] <> {};
then
A4: dom curry f = X by A1,Th17;
thus rng curry f c= Funcs(Y,rng f)
proof
let z be object;
assume z in rng curry f;
then consider x being object such that
A5: x in dom curry f and
A6: z = (curry f).x by FUNCT_1:def 3;
ex g st (curry f).x = g & dom g = Y & rng g c= rng f & for y st y
in Y holds g.y = f.(x,y) by A1,A3,A4,A5,Th22;
hence thesis by A6,FUNCT_2:def 2;
end;
A7: dom curry' f = Y by A1,A3,Th17;
thus rng curry' f c= Funcs(X,rng f)
proof
let z be object;
assume z in rng curry' f;
then consider y being object such that
A8: y in dom curry' f and
A9: z = (curry' f).y by FUNCT_1:def 3;
ex g st (curry' f).y = g & dom g = X & rng g c= rng f & for x st x
in X holds g.x = f.(x,y) by A1,A3,A7,A8,Th25;
hence thesis by A9,FUNCT_2:def 2;
end;
end;
now
assume
A10: dom f = {};
then X = {} or Y = {} by A1;
then
A11: [:Y,X:] = {} by ZFMISC_1:90;
{} = dom curry f by A10,Def1,Th2;
then
A12: rng curry f = {} by RELAT_1:42;
dom ~f = [:Y,X:] & dom curry ~f = proj1 dom ~f by A1,Def1,FUNCT_4:46;
then rng curry' f = {} by A11,Th2,RELAT_1:42;
hence thesis by A12;
end;
hence thesis by A1,A2;
end;
theorem
rng curry f c= PFuncs(proj2 dom f,rng f) & rng curry' f c= PFuncs(
proj1 dom f,rng f)
proof
A1: rng ~f c= rng f by FUNCT_4:41;
thus rng curry f c= PFuncs(proj2 dom f,rng f)
proof
let t be object;
assume t in rng curry f;
then consider z being object such that
A2: z in dom curry f and
A3: t = (curry f).z by FUNCT_1:def 3;
dom curry f = proj1 dom f by Def1;
then consider g such that
A4: (curry f).z = g and
dom g = proj2 (dom f /\ [:{z},proj2 dom f:]) and
for y st y in dom g holds g.y = f.(z,y) by A2,Def1;
dom g c= proj2 dom f & rng g c= rng f by A2,A4,Th24;
hence thesis by A3,A4,PARTFUN1:def 3;
end;
let t be object;
assume t in rng curry' f;
then consider z being object such that
A5: z in dom curry' f and
A6: t = (curry' f).z by FUNCT_1:def 3;
dom curry ~f = proj1 dom ~f by Def1;
then consider g such that
A7: (curry ~f).z = g and
dom g = proj2 (dom ~f /\ [:{z},proj2 dom ~f:]) and
for y st y in dom g holds g.y = (~f).(z,y) by A5,Def1;
rng g c= rng ~f by A5,A7,Th24;
then
A8: rng g c= rng f by A1;
dom g c= proj2 dom ~f by A5,A7,Th24;
then dom g c= proj1 dom f by Th11;
hence thesis by A6,A7,A8,PARTFUN1:def 3;
end;
theorem Th30:
rng f c= PFuncs(X,Y) implies dom uncurry f c= [:dom f,X:] & dom
uncurry' f c= [:X,dom f:]
proof
assume
A1: rng f c= PFuncs(X,Y);
thus
A2: dom uncurry f c= [:dom f,X:]
proof
let x be object;
assume x in dom uncurry f;
then consider y,g,z such that
A3: x = [y,z] and
A4: y in dom f and
A5: g = f.y and
A6: z in dom g by Def2;
g in rng f by A4,A5,FUNCT_1:def 3;
then g is PartFunc of X,Y by A1,PARTFUN1:46;
then dom g c= X by RELAT_1:def 18;
hence thesis by A3,A4,A6,ZFMISC_1:87;
end;
let x be object;
assume x in dom uncurry' f;
then ex y,z being object st x = [z,y] & [y,z] in dom uncurry f
by FUNCT_4:def 2;
hence thesis by A2,ZFMISC_1:88;
end;
theorem Th31:
x in dom f & g = f.x & y in dom g implies [x,y] in dom uncurry f
& (uncurry f).(x,y) = g.y & g.y in rng uncurry f
proof
assume that
A1: x in dom f and
A2: g = f.x and
A3: y in dom g;
thus
A4: [x,y] in dom uncurry f by A1,A2,A3,Def2;
[x,y]`1 = x & [x,y]`2 = y;
hence (uncurry f).(x,y) = g.y by A2,A4,Def2;
hence thesis by A4,FUNCT_1:def 3;
end;
theorem
x in dom f & g = f.x & y in dom g implies [y,x] in dom uncurry' f & (
uncurry' f).(y,x) = g.y & g.y in rng uncurry' f
proof
assume
A1: x in dom f & g = f.x & y in dom g;
then [x,y] in dom uncurry f by Th31;
hence
A2: [y,x] in dom uncurry' f by FUNCT_4:42;
(uncurry f).(x,y) = g.y by A1,Th31;
hence (uncurry' f).(y,x) = g.y by A2,FUNCT_4:43;
hence thesis by A2,FUNCT_1:def 3;
end;
theorem Th33:
rng f c= PFuncs(X,Y) implies rng uncurry f c= Y & rng uncurry' f c= Y
proof
assume
A1: rng f c= PFuncs(X,Y);
thus
A2: rng uncurry f c= Y
proof
let x be object;
assume x in rng uncurry f;
then consider y being object such that
A3: y in dom uncurry f and
A4: x = (uncurry f).y by FUNCT_1:def 3;
consider z,g,t such that
A5: y = [z,t] and
A6: z in dom f & g = f.z and
A7: t in dom g by A3,Def2;
g in rng f by A6,FUNCT_1:def 3;
then
A8: ex g1 st g = g1 & dom g1 c= X & rng g1 c= Y by A1,PARTFUN1:def 3;
(uncurry f).(z,t) = g.t & g.t in rng g by A6,A7,Th31,FUNCT_1:def 3;
hence thesis by A4,A5,A8;
end;
rng uncurry' f c= rng uncurry f by FUNCT_4:41;
hence thesis by A2;
end;
theorem Th34:
rng f c= Funcs(X,Y) implies rng uncurry f c= Y & rng uncurry' f c= Y
proof
A1: Funcs(X,Y) c= PFuncs(X,Y) by FUNCT_2:72;
assume rng f c= Funcs(X,Y);
then rng f c= PFuncs(X,Y) by A1;
hence thesis by Th33;
end;
theorem Th35:
curry {} = {} & curry' {} = {}
by Def1,Th1;
theorem Th36:
uncurry {} = {} & uncurry' {} = {}
proof
A1: now
set t = the Element of dom uncurry {};
assume dom uncurry {} <> {};
then ex x,g,y st t = [x,y] & x in dom {} & g = {} .x & y in dom g by Def2;
hence contradiction;
end;
hence uncurry {} = {};
thus thesis by A1,Th1,RELAT_1:41;
end;
theorem Th37:
dom f1 = [:X,Y:] & dom f2 = [:X,Y:] & curry f1 = curry f2 implies f1 = f2
proof
assume that
A1: dom f1 = [:X,Y:] and
A2: dom f2 = [:X,Y:] and
A3: curry f1 = curry f2;
A4: now
assume [:X,Y:] <> {};
now
let z be object;
assume
A5: z in [:X,Y:];
then consider g1 being Function such that
A6: (curry f1).z`1 = g1 and
dom g1 = Y and
rng g1 c= rng f1 and
A7: for y st y in Y holds g1.y = f1.(z`1,y) by A1,Th22,MCART_1:10;
A8: z = [z`1,z`2] by A5,MCART_1:21;
A9: z`2 in Y by A5,MCART_1:10;
then
A10: f1.(z`1,z`2) = g1.z`2 by A7;
ex g2 being Function st (curry f2).z`1 = g2 & dom g2 = Y & rng g2 c=
rng f2 & for y st y in Y holds g2.y = f2.(z`1,y) by A2,A5,Th22,MCART_1:10;
then f2.(z`1,z`2) = g1.z`2 by A3,A9,A6;
hence f1.z = f2.z by A8,A10;
end;
hence thesis by A1,A2;
end;
[:X,Y:] = {} implies f1 = {} & f2 = {} by A1,A2;
hence thesis by A4;
end;
theorem Th38:
dom f1 = [:X,Y:] & dom f2 = [:X,Y:] & curry' f1 = curry' f2 implies f1 = f2
proof
assume that
A1: dom f1 = [:X,Y:] and
A2: dom f2 = [:X,Y:] and
A3: curry' f1 = curry' f2;
dom ~f1 = [:Y,X:] & dom ~f2 = [:Y,X:] by A1,A2,FUNCT_4:46;
then
A4: ~f1 = ~f2 by A3,Th37;
~~f1 = f1 by A1,FUNCT_4:52;
hence thesis by A2,A4,FUNCT_4:52;
end;
theorem Th39:
rng f1 c= Funcs(X,Y) & rng f2 c= Funcs(X,Y) & X <> {} & uncurry
f1 = uncurry f2 implies f1 = f2
proof
assume that
A1: rng f1 c= Funcs(X,Y) and
A2: rng f2 c= Funcs(X,Y) and
A3: X <> {} and
A4: uncurry f1 = uncurry f2;
A5: dom uncurry f1 = [:dom f1,X:] & dom uncurry f2 = [:dom f2,X:] by A1,A2,Th19
;
then dom f1 = {} implies dom f1 = dom f2 by A3,A4;
then
A6: dom f1 = dom f2 by A3,A4,A5,ZFMISC_1:110;
now
let x be object;
assume
A7: x in dom f1;
then f1.x in rng f1 by FUNCT_1:def 3;
then consider g1 such that
A8: f1.x = g1 and
A9: dom g1 = X and
rng g1 c= Y by A1,FUNCT_2:def 2;
f2.x in rng f2 by A6,A7,FUNCT_1:def 3;
then consider g2 such that
A10: f2.x = g2 and
A11: dom g2 = X and
rng g2 c= Y by A2,FUNCT_2:def 2;
now
let y be object;
A12: [x,y]`1 = x & [x,y]`2 = y;
assume
A13: y in X;
then
A14: [x,y] in dom uncurry f2 by A4,A7,A8,A9,Def2;
[x,y] in dom uncurry f1 by A7,A8,A9,A13,Def2;
then (uncurry f1).[x,y] = g1.y by A8,A12,Def2;
hence g1.y = g2.y by A4,A10,A14,A12,Def2;
end;
hence f1.x = f2.x by A8,A9,A10,A11,FUNCT_1:2;
end;
hence thesis by A6;
end;
theorem
rng f1 c= Funcs(X,Y) & rng f2 c= Funcs(X,Y) & X <> {} & uncurry' f1 =
uncurry' f2 implies f1 = f2
proof
assume that
A1: rng f1 c= Funcs(X,Y) and
A2: rng f2 c= Funcs(X,Y) and
A3: X <> {} & uncurry' f1 = uncurry' f2;
dom uncurry f1 = [:dom f1,X:] by A1,Th19;
then
A4: uncurry f1 = ~~(uncurry f1) by FUNCT_4:52;
dom uncurry f2 = [:dom f2,X:] by A2,Th19;
hence thesis by A1,A2,A3,A4,Th39,FUNCT_4:52;
end;
theorem Th41:
rng f c= Funcs(X,Y) & X <> {} implies curry uncurry f = f &
curry' uncurry' f = f
proof
assume that
A1: rng f c= Funcs(X,Y) and
A2: X <> {};
A3: dom uncurry f = [:dom f,X:] by A1,Th19;
A4: now
A5: now
let x be object;
assume
A6: x in dom f;
then consider h such that
A7: (curry uncurry f).x = h & dom h = X & rng h c= rng uncurry f and
A8: y in X implies h.y = (uncurry f).(x,y) by A2,A3,Th22;
f.x in rng f by A6,FUNCT_1:def 3;
then consider g such that
A9: f.x = g & dom g = X and
rng g c= Y by A1,FUNCT_2:def 2;
now
let y be object;
assume
A10: y in X;
then (uncurry f).(x,y) = g.y by A6,A9,Th31;
hence g.y = h.y by A8,A10;
end;
hence f.x = (curry uncurry f).x by A9,A7,FUNCT_1:2;
end;
assume dom f <> {};
then dom curry uncurry f = dom f by A2,A3,Th17;
hence curry uncurry f = f by A5;
end;
A11: now
assume dom f = {};
then dom uncurry f = {} & f = {} by A3;
hence curry uncurry f = f by Th35,RELAT_1:41;
end;
hence curry uncurry f = f by A4;
thus thesis by A3,A11,A4,FUNCT_4:52;
end;
theorem
dom f = [:X,Y:] implies uncurry curry f = f & uncurry' curry' f = f
proof
assume
A1: dom f = [:X,Y:];
A2: now
A3: rng curry' f c= Funcs(X,rng f) by A1,Th28;
assume
A4: dom f <> {};
then X <> {} by A1;
then
A5: curry' uncurry' curry' f = curry' f by A3,Th41;
dom curry' f = Y by A1,A4,Th17;
then
A6: dom uncurry' curry' f = [:X,Y:] by A3,Th19;
A7: rng curry f c= Funcs(Y,rng f) by A1,Th28;
Y <> {} by A1,A4;
then
A8: curry uncurry curry f = curry f by A7,Th41;
dom curry f = X by A1,A4,Th17;
then dom uncurry curry f = [:X,Y:] by A7,Th19;
hence thesis by A1,A8,A5,A6,Th37,Th38;
end;
now
assume dom f = {};
then f = {};
hence thesis by Th35,Th36;
end;
hence thesis by A2;
end;
theorem Th43:
dom f c= [:X,Y:] implies uncurry curry f = f & uncurry' curry' f = f
proof
assume
A1: dom f c= [:X,Y:];
A2: now
let X,Y,f such that
A3: dom f c= [:X,Y:];
A4: dom uncurry curry f = dom f
proof
thus dom uncurry curry f c= dom f
proof
let x be object;
assume x in dom uncurry curry f;
then
ex y,g,z st x = [y,z] & y in dom curry f & g = (curry f).y & z in
dom g by Def2;
hence thesis by Th24;
end;
let x be object;
assume
A5: x in dom f;
then
A6: x = [x`1,x`2] by A3,MCART_1:21;
then x`1 in dom curry f by A5,Th12;
then reconsider g = (curry f).x`1 as Function by FUNCOP_1:def 6;
x`2 in dom g & x`1 in dom curry f by A5,A6,Th12,Th13;
hence thesis by A6,Th31;
end;
now
let x be object;
assume
A7: x in dom f;
then
A8: x = [x`1,x`2] by A3,MCART_1:21;
then x`1 in dom curry f by A7,Th12;
then reconsider g = (curry f).x`1 as Function by FUNCOP_1:def 6;
(uncurry curry f).x = g.x`2 by A4,A7,Def2;
then f.(x`1,x`2) = (uncurry curry f).(x`1,x`2) by A7,A8,Th13;
hence f.x = (uncurry curry f).x by A8;
end;
hence uncurry curry f = f by A4;
end;
hence uncurry curry f = f by A1;
dom ~f c= [:Y,X:] by A1,FUNCT_4:45;
then uncurry curry ~f = ~f by A2;
hence thesis by A1,FUNCT_4:52;
end;
theorem Th44:
rng f c= PFuncs(X,Y) & not {} in rng f implies curry uncurry f =
f & curry' uncurry' f = f
proof
assume that
A1: rng f c= PFuncs(X,Y) and
A2: not {} in rng f;
A3: dom curry uncurry f = dom f
proof
dom uncurry f c= [:dom f,X:] by A1,Th30;
hence dom curry uncurry f c= dom f by Th18;
let x be object;
assume
A4: x in dom f;
then f.x in rng f by FUNCT_1:def 3;
then consider g such that
A5: f.x = g and
dom g c= X and
rng g c= Y by A1,PARTFUN1:def 3;
set y = the Element of dom g;
g <> {} by A2,A4,A5,FUNCT_1:def 3;
then
A6: [x,y] in dom uncurry f by A4,A5,Th31;
dom curry uncurry f = proj1 dom uncurry f by Def1;
hence thesis by A6,XTUPLE_0:def 12;
end;
now
let x be object;
assume
A7: x in dom f;
then reconsider h = (curry uncurry f).x as Function by A3,Th23;
f.x in rng f by A7,FUNCT_1:def 3;
then consider g such that
A8: f.x = g and
dom g c= X and
rng g c= Y by A1,PARTFUN1:def 3;
A9: dom h = proj2 (dom uncurry f /\ [:{x},proj2 dom uncurry f:]) by A3,A7,Th24;
A10: dom h = dom g
proof
thus dom h c= dom g
proof
let z be object;
assume z in dom h;
then consider t being object such that
A11: [t,z] in dom uncurry f /\ [:{x},proj2 dom uncurry f:] by A9,
XTUPLE_0:def 13;
[t,z] in [:{x},proj2 dom uncurry f:] by A11,XBOOLE_0:def 4;
then
A12: t = x by ZFMISC_1:105;
[t,z] in dom uncurry f by A11,XBOOLE_0:def 4;
then consider x1,g1,x2 such that
A13: [t,z] = [x1,x2] and
x1 in dom f and
A14: g1 = f.x1 & x2 in dom g1 by Def2;
t = x1 by A13,XTUPLE_0:1;
hence thesis by A8,A13,A14,A12,XTUPLE_0:1;
end;
let y be object;
assume y in dom g;
then [x,y] in dom uncurry f by A7,A8,Th31;
hence thesis by Th13;
end;
now
let y be object;
assume
A15: y in dom h;
hence h.y = (uncurry f).(x,y) by A3,A7,Th24
.= g.y by A7,A8,A10,A15,Th31;
end;
hence f.x = (curry uncurry f).x by A8,A10,FUNCT_1:2;
end;
hence
A16: curry uncurry f = f by A3;
dom uncurry f c= [:dom f,X:] by A1,Th30;
hence thesis by A16,FUNCT_4:52;
end;
theorem
dom f1 c= [:X,Y:] & dom f2 c= [:X,Y:] & curry f1 = curry f2 implies f1 = f2
proof
assume that
A1: dom f1 c= [:X,Y:] and
A2: dom f2 c= [:X,Y:];
uncurry curry f1 = f1 by A1,Th43;
hence thesis by A2,Th43;
end;
theorem
dom f1 c= [:X,Y:] & dom f2 c= [:X,Y:] & curry' f1 = curry' f2 implies f1 = f2
proof
assume that
A1: dom f1 c= [:X,Y:] and
A2: dom f2 c= [:X,Y:];
uncurry' curry' f1 = f1 by A1,Th43;
hence thesis by A2,Th43;
end;
theorem
rng f1 c= PFuncs(X,Y) & rng f2 c= PFuncs(X,Y) & not {} in rng f1 & not
{} in rng f2 & uncurry f1 = uncurry f2 implies f1 = f2
proof
assume that
A1: rng f1 c= PFuncs(X,Y) and
A2: rng f2 c= PFuncs(X,Y) and
A3: not {} in rng f1 and
A4: not {} in rng f2;
curry uncurry f1 = f1 by A1,A3,Th44;
hence thesis by A2,A4,Th44;
end;
theorem
rng f1 c= PFuncs(X,Y) & rng f2 c= PFuncs(X,Y) & not {} in rng f1 & not
{} in rng f2 & uncurry' f1 = uncurry' f2 implies f1 = f2
proof
assume that
A1: rng f1 c= PFuncs(X,Y) and
A2: rng f2 c= PFuncs(X,Y) and
A3: not {} in rng f1 and
A4: not {} in rng f2;
curry' uncurry' f1 = f1 by A1,A3,Th44;
hence thesis by A2,A4,Th44;
end;
theorem Th49:
X c= Y implies Funcs(Z,X) c= Funcs(Z,Y)
proof
assume
A1: X c= Y;
let x be object;
assume x in Funcs(Z,X);
then consider f such that
A2: x = f & dom f = Z and
A3: rng f c= X by FUNCT_2:def 2;
rng f c= Y by A1,A3;
hence thesis by A2,FUNCT_2:def 2;
end;
theorem Th50:
Funcs({},X) = {{}}
proof
thus Funcs({},X) c= {{}}
proof
let x be object;
assume x in Funcs({},X);
then ex f st x = f & dom f = {} & rng f c= X by FUNCT_2:def 2;
then x = {};
hence thesis by TARSKI:def 1;
end;
let x be object;
A1: {} c= X;
assume x in {{}};
then
A2: x = {} by TARSKI:def 1;
dom {} = {} & rng {} = {};
hence thesis by A2,A1,FUNCT_2:def 2;
end;
theorem
for x being object holds
X,Funcs({x},X) are_equipotent & card X = card Funcs({x},X)
proof let x be object;
deffunc F(object) = {x} --> $1;
consider f such that
A1: dom f = X &
for y being object st y in X holds f.y = F(y) from FUNCT_1:sch 3;
A2: x in {x} by TARSKI:def 1;
thus X,Funcs({x},X) are_equipotent
proof
take f;
thus f is one-to-one
proof
let y,z be object;
assume y in dom f & z in dom f;
then
A3: f.y = {x} --> y & f.z = {x} --> z by A1;
({x} --> y).x = y by A2,FUNCOP_1:7;
hence thesis by A2,A3,FUNCOP_1:7;
end;
thus dom f = X by A1;
thus rng f c= Funcs({x},X)
proof
let y be object;
assume y in rng f;
then consider z being object such that
A4: z in dom f & y = f.z by FUNCT_1:def 3;
A5: dom({x} --> z) = {x} & rng({x} --> z) = {z} by FUNCOP_1:8,13;
y = {x} --> z & {z} c= X by A1,A4,ZFMISC_1:31;
hence thesis by A5,FUNCT_2:def 2;
end;
let y be object;
assume y in Funcs({x},X);
then consider g such that
A6: y = g and
A7: dom g = {x} and
A8: rng g c= X by FUNCT_2:def 2;
A9: g.x in {g.x} by TARSKI:def 1;
A10: rng g = {g.x} by A7,FUNCT_1:4;
then g = {x} --> (g.x) by A7,FUNCOP_1:9;
then f.(g.x) = g by A1,A8,A10,A9;
hence thesis by A1,A6,A8,A10,A9,FUNCT_1:def 3;
end;
hence thesis by CARD_1:5;
end;
theorem Th52:
Funcs(X,{x}) = {X --> x}
proof
thus Funcs(X,{x}) c= {X --> x}
proof
let y be object;
assume y in Funcs(X,{x});
then consider f such that
A1: y = f and
A2: dom f = X and
A3: rng f c= {x} by FUNCT_2:def 2;
A4: now
set z = the Element of X;
A5: X <> {} implies z in X;
assume for z holds not z in X;
hence f = X --> x by A2,A5;
end;
now
given z such that
A6: z in X;
f.z in rng f by A2,A6,FUNCT_1:def 3;
then f.z = x & {f.z} c= rng f by A3,TARSKI:def 1;
then rng f = {x} by A3;
hence f = X --> x by A2,FUNCOP_1:9;
end;
hence thesis by A1,A4,TARSKI:def 1;
end;
let y be object;
assume y in {X --> x};
then
A7: y = X --> x by TARSKI:def 1;
dom(X --> x) = X & rng(X --> x) c= {x} by FUNCOP_1:13;
hence thesis by A7,FUNCT_2:def 2;
end;
theorem Th53:
X1,Y1 are_equipotent & X2,Y2 are_equipotent implies Funcs(X1,X2)
,Funcs(Y1,Y2) are_equipotent & card Funcs(X1,X2) = card Funcs(Y1,Y2)
proof
assume that
A1: X1,Y1 are_equipotent and
A2: X2,Y2 are_equipotent;
consider f1 such that
A3: f1 is one-to-one and
A4: dom f1 = Y1 and
A5: rng f1 = X1 by A1,WELLORD2:def 4;
consider f2 such that
A6: f2 is one-to-one and
A7: dom f2 = X2 and
A8: rng f2 = Y2 by A2;
Funcs(X1,X2),Funcs(Y1,Y2) are_equipotent
proof
A9: rng(f1") = Y1 by A3,A4,FUNCT_1:33;
deffunc F(Function) = f2*($1*f1);
consider F being Function such that
A10: dom F = Funcs(X1,X2) & for g st g in Funcs(X1,X2) holds F.g = F(g
) from LambdaFS;
take F;
thus F is one-to-one
proof
let x,y be object;
assume that
A11: x in dom F and
A12: y in dom F and
A13: F.x = F.y;
consider g1 being Function such that
A14: x = g1 and
A15: dom g1 = X1 and
A16: rng g1 c= X2 by A10,A11,FUNCT_2:def 2;
A17: F.x = f2*(g1*f1) by A10,A11,A14;
A18: rng(g1*f1) c= X2 & dom(g1*f1) = Y1 by A4,A5,A15,A16,RELAT_1:27,28;
consider g2 being Function such that
A19: y = g2 and
A20: dom g2 = X1 and
A21: rng g2 c= X2 by A10,A12,FUNCT_2:def 2;
A22: rng(g2*f1) c= X2 & dom(g2*f1) = Y1 by A4,A5,A20,A21,RELAT_1:27,28;
F.x = f2*(g2*f1) by A10,A12,A13,A19;
then
A23: g1*f1 = g2*f1 by A6,A7,A17,A18,A22,FUNCT_1:27;
now
let z be object;
assume z in X1;
then consider z9 being object such that
A24: z9 in Y1 & f1.z9 = z by A4,A5,FUNCT_1:def 3;
thus g1.z = (g1*f1).z9 by A4,A24,FUNCT_1:13
.= g2.z by A4,A23,A24,FUNCT_1:13;
end;
hence thesis by A14,A15,A19,A20,FUNCT_1:2;
end;
thus dom F = Funcs(X1,X2) by A10;
thus rng F c= Funcs(Y1,Y2)
proof
let x be object;
assume x in rng F;
then consider y being object such that
A25: y in dom F and
A26: x = F.y by FUNCT_1:def 3;
consider g such that
A27: y = g and
A28: dom g = X1 & rng g c= X2 by A10,A25,FUNCT_2:def 2;
dom(g*f1) = Y1 & rng(g*f1) c= X2 by A4,A5,A28,RELAT_1:27,28;
then
A29: dom(f2*(g*f1)) = Y1 by A7,RELAT_1:27;
A30: rng(f2*(g*f1)) c= Y2 by A8,RELAT_1:26;
x = f2*(g*f1) by A10,A25,A26,A27;
hence thesis by A29,A30,FUNCT_2:def 2;
end;
let x be object;
assume x in Funcs(Y1,Y2);
then consider g such that
A31: x = g and
A32: dom g = Y1 and
A33: rng g c= Y2 by FUNCT_2:def 2;
A34: f2*((f2"*g*(f1"))*f1) = f2*(f2"*g*(f1"*f1)) by RELAT_1:36
.= f2*(f2"*g)*(f1"*f1) by RELAT_1:36
.= f2*(f2")*g*(f1"*f1) by RELAT_1:36
.= (id Y2)*g*(f1"*f1) by A6,A8,FUNCT_1:39
.= (id Y2)*g*(id Y1) by A3,A4,FUNCT_1:39
.= g*(id Y1) by A33,RELAT_1:53
.= x by A31,A32,RELAT_1:52;
dom(f2") = Y2 by A6,A8,FUNCT_1:33;
then
A35: dom(f2"*g) = Y1 by A32,A33,RELAT_1:27;
rng(f2") = X2 by A6,A7,FUNCT_1:33;
then rng(f2"*g) c= X2 by RELAT_1:26;
then
A36: rng(f2"*g*(f1")) c= X2 by A9,A35,RELAT_1:28;
dom(f1") = X1 by A3,A5,FUNCT_1:33;
then dom(f2"*g*(f1")) = X1 by A9,A35,RELAT_1:27;
then
A37: f2"*g*(f1") in dom F by A10,A36,FUNCT_2:def 2;
then F.(f2"*g*(f1")) = f2*((f2"*g*(f1"))*f1) by A10;
hence thesis by A37,A34,FUNCT_1:def 3;
end;
hence thesis by CARD_1:5;
end;
theorem
card X1 = card Y1 & card X2 = card Y2 implies card Funcs(X1,X2) = card
Funcs(Y1,Y2)
proof
assume card X1 = card Y1 & card X2 = card Y2;
then X1,Y1 are_equipotent & X2,Y2 are_equipotent by CARD_1:5;
hence thesis by Th53;
end;
theorem
X1 misses X2 implies Funcs(X1 \/ X2,X),[:Funcs(X1,X),Funcs(X2,X):]
are_equipotent & card Funcs(X1 \/ X2,X) = card [:Funcs(X1,X),Funcs(X2,X):]
proof
deffunc F(Function) = [ $1|X1,$1|X2];
consider f such that
A1: dom f = Funcs(X1 \/ X2,X) & for g st g in Funcs(X1 \/ X2,X) holds f.
g = F(g) from LambdaFS;
assume
A2: X1 misses X2;
thus Funcs(X1 \/ X2,X),[:Funcs(X1,X),Funcs(X2,X):] are_equipotent
proof
take f;
thus f is one-to-one
proof
let x,y be object;
assume that
A3: x in dom f and
A4: y in dom f;
consider g2 being Function such that
A5: y = g2 and
A6: dom g2 = X1 \/ X2 and
rng g2 c= X by A1,A4,FUNCT_2:def 2;
A7: f.y = [g2|X1,g2|X2] by A1,A4,A5;
assume
A8: f.x = f.y;
consider g1 being Function such that
A9: x = g1 and
A10: dom g1 = X1 \/ X2 and
rng g1 c= X by A1,A3,FUNCT_2:def 2;
A11: f.x = [g1|X1,g1|X2] by A1,A3,A9;
now
let x be object;
assume x in X1 \/ X2;
then x in X1 or x in X2 by XBOOLE_0:def 3;
then
g1.x = g1|X1.x & g2.x = g2|X1.x or g1.x = g1|X2.x & g2.x = g2|X2.
x by FUNCT_1:49;
hence g1.x = g2.x by A11,A7,A8,XTUPLE_0:1;
end;
hence thesis by A9,A10,A5,A6,FUNCT_1:2;
end;
thus dom f = Funcs(X1 \/ X2,X) by A1;
thus rng f c= [:Funcs(X1,X),Funcs(X2,X):]
proof
let x be object;
assume x in rng f;
then consider y being object such that
A12: y in dom f and
A13: x = f.y by FUNCT_1:def 3;
consider g such that
A14: y = g and
A15: dom g = X1 \/ X2 and
A16: rng g c= X by A1,A12,FUNCT_2:def 2;
rng(g|X2) c= rng g by RELAT_1:70;
then
A17: rng(g|X2) c= X by A16;
rng(g|X1) c= rng g by RELAT_1:70;
then
A18: rng(g|X1) c= X by A16;
dom(g|X2) = X2 by A15,RELAT_1:62,XBOOLE_1:7;
then
A19: g|X2 in Funcs(X2,X) by A17,FUNCT_2:def 2;
dom(g|X1) = X1 by A15,RELAT_1:62,XBOOLE_1:7;
then g|X1 in Funcs(X1,X) by A18,FUNCT_2:def 2;
then [g|X1,g|X2] in [:Funcs(X1,X),Funcs(X2,X):] by A19,ZFMISC_1:87;
hence thesis by A1,A12,A13,A14;
end;
let x be object;
assume
A20: x in [:Funcs(X1,X),Funcs(X2,X):];
then
A21: x = [x`1,x`2] by MCART_1:21;
x`1 in Funcs(X1,X) by A20,MCART_1:10;
then consider g1 being Function such that
A22: x`1 = g1 and
A23: dom g1 = X1 and
A24: rng g1 c= X by FUNCT_2:def 2;
x`2 in Funcs(X2,X) by A20,MCART_1:10;
then consider g2 being Function such that
A25: x`2 = g2 and
A26: dom g2 = X2 and
A27: rng g2 c= X by FUNCT_2:def 2;
rng(g1+*g2) c= rng g1 \/ rng g2 & rng g1 \/ rng g2 c= X \/ X by A24,A27,
FUNCT_4:17,XBOOLE_1:13;
then
A28: rng(g1+*g2) c= X;
dom(g1+*g2) = X1 \/ X2 by A23,A26,FUNCT_4:def 1;
then
A29: g1+*g2 in dom f by A1,A28,FUNCT_2:def 2;
then f.(g1+*g2) = [(g1+*g2)|X1,(g1+*g2)|X2] by A1
.= [(g1+*g2)|X1,g2] by A26,FUNCT_4:23
.= x by A2,A21,A22,A23,A25,A26,FUNCT_4:33;
hence thesis by A29,FUNCT_1:def 3;
end;
hence thesis by CARD_1:5;
end;
theorem
Funcs([:X,Y:],Z),Funcs(X,Funcs(Y,Z)) are_equipotent & card Funcs([:X,Y
:],Z) = card Funcs(X,Funcs(Y,Z))
proof
deffunc F(Function) = curry $1;
consider f such that
A1: dom f = Funcs([:X,Y:],Z) & for g st g in Funcs([:X,Y:],Z) holds f.g
= F(g) from LambdaFS;
A2: now
assume
A3: [:X,Y:] <> {};
thus Funcs([:X,Y:],Z),Funcs(X,Funcs(Y,Z)) are_equipotent
proof
take f;
thus f is one-to-one
proof
let x1,x2 be object;
assume that
A4: x1 in dom f and
A5: x2 in dom f and
A6: f.x1 = f.x2;
consider g2 such that
A7: x2 = g2 and
A8: dom g2 = [:X,Y:] and
rng g2 c= Z by A1,A5,FUNCT_2:def 2;
A9: f.x2 = curry g2 by A1,A5,A7;
consider g1 such that
A10: x1 = g1 and
A11: dom g1 = [:X,Y:] and
rng g1 c= Z by A1,A4,FUNCT_2:def 2;
f.x1 = curry g1 by A1,A4,A10;
hence thesis by A6,A10,A11,A7,A8,A9,Th37;
end;
thus dom f = Funcs([:X,Y:],Z) by A1;
thus rng f c= Funcs(X,Funcs(Y,Z))
proof
let y be object;
assume y in rng f;
then consider x being object such that
A12: x in dom f and
A13: y = f.x by FUNCT_1:def 3;
consider g such that
A14: x = g and
A15: dom g = [:X,Y:] and
A16: rng g c= Z by A1,A12,FUNCT_2:def 2;
A17: dom curry g = X by A3,A15,Th17;
rng curry g c= Funcs(Y,rng g) & Funcs(Y,rng g) c= Funcs(Y,Z) by A15,A16
,Th28,Th49;
then
A18: rng curry g c= Funcs(Y,Z);
y = curry g by A1,A12,A13,A14;
hence thesis by A17,A18,FUNCT_2:def 2;
end;
let y be object;
assume y in Funcs(X,Funcs(Y,Z));
then consider g such that
A19: y = g and
A20: dom g = X and
A21: rng g c= Funcs(Y,Z) by FUNCT_2:def 2;
dom uncurry g = [:X,Y:] & rng uncurry g c= Z by A20,A21,Th19,Th34;
then
A22: uncurry g in Funcs([:X,Y:],Z) by FUNCT_2:def 2;
Y <> {} by A3,ZFMISC_1:90;
then curry uncurry g = g by A21,Th41;
then f.(uncurry g) = y by A1,A19,A22;
hence thesis by A1,A22,FUNCT_1:def 3;
end;
hence card Funcs([:X,Y:],Z) = card Funcs(X,Funcs(Y,Z)) by CARD_1:5;
end;
now
assume
A23: [:X,Y:] = {};
then
A24: Funcs([:X,Y:],Z) = {{}} by Th50;
A25: now
assume Y = {};
then Funcs(Y,Z) = {{}} by Th50;
then Funcs(X,Funcs(Y,Z)) = {X --> {}} by Th52;
hence Funcs([:X,Y:],Z),Funcs(X,Funcs(Y,Z)) are_equipotent by A24,
CARD_1:28;
end;
X = {} or Y = {} by A23;
hence Funcs([:X,Y:],Z),Funcs(X,Funcs(Y,Z)) are_equipotent by A24,A25,Th50;
X = {} implies Funcs(X,Funcs(Y,Z)) = {{}} by Th50;
hence card Funcs([:X,Y:],Z) = card Funcs(X,Funcs(Y,Z)) by A23,A25,Th50,
CARD_1:5;
end;
hence thesis by A2;
end;
theorem
Funcs(Z,[:X,Y:]),[:Funcs(Z,X),Funcs(Z,Y):] are_equipotent & card Funcs
(Z,[:X,Y:]) = card [:Funcs(Z,X),Funcs(Z,Y):]
proof
deffunc F(Function) = [pr1(X,Y)*$1,pr2(X,Y)*$1];
consider f such that
A1: dom f = Funcs(Z,[:X,Y:]) & for g st g in Funcs(Z,[:X,Y:]) holds f.g
= F(g) from LambdaFS;
thus Funcs(Z,[:X,Y:]),[:Funcs(Z,X),Funcs(Z,Y):] are_equipotent
proof
take f;
thus f is one-to-one
proof
let x1,x2 be object;
assume that
A2: x1 in dom f and
A3: x2 in dom f and
A4: f.x1 = f.x2;
consider g1 such that
A5: x1 = g1 and
A6: dom g1 = Z and
A7: rng g1 c= [:X,Y:] by A1,A2,FUNCT_2:def 2;
consider g2 such that
A8: x2 = g2 and
A9: dom g2 = Z and
A10: rng g2 c= [:X,Y:] by A1,A3,FUNCT_2:def 2;
[pr1(X,Y)*g1,pr2(X,Y)*g1] = f.x1 by A1,A2,A5
.= [pr1(X,Y)*g2,pr2(X,Y)*g2] by A1,A3,A4,A8;
then
A11: pr1(X,Y)*g1 = pr1(X,Y)*g2 & pr2(X,Y)*g1 = pr2(X,Y)*g2 by XTUPLE_0:1;
now
let x be object;
assume
A12: x in Z;
then
A13: (pr2(X,Y)*g1).x = pr2(X,Y).(g1.x) by A6,FUNCT_1:13;
A14: g2.x in rng g2 by A9,A12,FUNCT_1:def 3;
then
A15: g2.x = [(g2.x)`1,(g2.x)`2] by A10,MCART_1:21;
A16: g1.x in rng g1 by A6,A12,FUNCT_1:def 3;
then
A17: g1.x = [(g1.x)`1,(g1.x)`2] by A7,MCART_1:21;
(g2.x)`1 in X & (g2.x)`2 in Y by A10,A14,MCART_1:10;
then
A18: pr1(X,Y).((g2.x)`1,(g2.x)`2) = (g2.x)`1 & pr2(X,Y).((g2.x)`1,(g2.
x)`2) = (g2 .x)`2 by FUNCT_3:def 4,def 5;
(g1.x)`1 in X & (g1.x)`2 in Y by A7,A16,MCART_1:10;
then
A19: pr1(X,Y).((g1.x)`1,(g1.x)`2) = (g1.x)`1 & pr2(X,Y).((g1.x)`1,(g1.
x)`2) = (g1 .x)`2 by FUNCT_3:def 4,def 5;
(pr1(X,Y)*g1).x = pr1(X,Y).(g1.x) & (pr1(X,Y)*g2).x = pr1(X,Y).(
g2.x) by A6,A9,A12,FUNCT_1:13;
hence g1.x = g2.x by A9,A11,A12,A13,A17,A15,A19,A18,FUNCT_1:13;
end;
hence thesis by A5,A6,A8,A9,FUNCT_1:2;
end;
thus dom f = Funcs(Z,[:X,Y:]) by A1;
thus rng f c= [:Funcs(Z,X),Funcs(Z,Y):]
proof
let x be object;
assume x in rng f;
then consider y being object such that
A20: y in dom f and
A21: x = f.y by FUNCT_1:def 3;
consider g such that
A22: y = g and
A23: dom g = Z & rng g c= [:X,Y:] by A1,A20,FUNCT_2:def 2;
A24: rng(pr1(X,Y)*g) c= X;
A25: rng(pr2(X,Y)*g) c= Y;
dom pr2(X,Y) = [:X,Y:] by FUNCT_3:def 5;
then dom(pr2(X,Y)*g) = Z by A23,RELAT_1:27;
then
A26: pr2(X,Y)*g in Funcs(Z,Y) by A25,FUNCT_2:def 2;
dom pr1(X,Y) = [:X,Y:] by FUNCT_3:def 4;
then dom(pr1(X,Y)*g) = Z by A23,RELAT_1:27;
then
A27: pr1(X,Y)*g in Funcs(Z,X) by A24,FUNCT_2:def 2;
x = [pr1(X,Y)*g,pr2(X,Y)*g] by A1,A20,A21,A22;
hence thesis by A27,A26,ZFMISC_1:87;
end;
let x be object;
assume
A28: x in [:Funcs(Z,X),Funcs(Z,Y):];
then
A29: x = [x`1,x`2] by MCART_1:21;
x`2 in Funcs(Z,Y) by A28,MCART_1:10;
then consider g2 such that
A30: x`2 = g2 and
A31: dom g2 = Z and
A32: rng g2 c= Y by FUNCT_2:def 2;
x`1 in Funcs(Z,X) by A28,MCART_1:10;
then consider g1 such that
A33: x`1 = g1 and
A34: dom g1 = Z and
A35: rng g1 c= X by FUNCT_2:def 2;
rng <:g1,g2:> c= [:rng g1,rng g2:] & [:rng g1,rng g2:] c= [:X,Y:] by A35
,A32,FUNCT_3:51,ZFMISC_1:96;
then
A36: rng <:g1,g2:> c= [:X,Y:];
dom <:g1,g2:> = Z /\ Z by A34,A31,FUNCT_3:def 7;
then
A37: <:g1,g2:> in Funcs(Z,[:X,Y:]) by A36,FUNCT_2:def 2;
pr1(X,Y)*<:g1,g2:> = g1 & pr2(X,Y)*<:g1,g2:> = g2 by A34,A35,A31,A32,
FUNCT_3:52;
then f.<:g1,g2:> = [g1,g2] by A1,A37;
hence thesis by A1,A29,A33,A30,A37,FUNCT_1:def 3;
end;
hence thesis by CARD_1:5;
end;
theorem
x <> y implies Funcs(X,{x,y}),bool X are_equipotent & card Funcs(X,{x,
y}) = card bool X
proof
deffunc F(Function) = $1"{x};
consider f such that
A1: dom f = Funcs(X,{x,y}) & for g st g in Funcs(X,{x,y}) holds f.g = F(
g) from LambdaFS;
assume
A2: x <> y;
thus Funcs(X,{x,y}),bool X are_equipotent
proof
deffunc F(object) = x;
take f;
thus f is one-to-one
proof
let x1,x2 be object;
assume that
A3: x1 in dom f and
A4: x2 in dom f and
A5: f.x1 = f.x2;
consider g2 being Function such that
A6: x2 = g2 and
A7: dom g2 = X and
A8: rng g2 c= {x,y} by A1,A4,FUNCT_2:def 2;
A9: f.x2 = g2"{x} by A1,A4,A6;
consider g1 being Function such that
A10: x1 = g1 and
A11: dom g1 = X and
A12: rng g1 c= {x,y} by A1,A3,FUNCT_2:def 2;
A13: f.x1 = g1"{x} by A1,A3,A10;
now
let z be object such that
A14: z in X;
A15: now
assume
A16: not g1.z in {x};
then
A17: g1.z <> x by TARSKI:def 1;
not z in g2"{x} by A5,A13,A9,A16,FUNCT_1:def 7;
then not g2.z in {x} by A7,A14,FUNCT_1:def 7;
then
A18: g2.z <> x by TARSKI:def 1;
g1.z in rng g1 by A11,A14,FUNCT_1:def 3;
then
A19: g1.z = y by A12,A17,TARSKI:def 2;
g2.z in rng g2 by A7,A14,FUNCT_1:def 3;
hence g1.z = g2.z by A8,A18,A19,TARSKI:def 2;
end;
now
assume
A20: g1.z in {x};
then z in g2"{x} by A5,A11,A13,A9,A14,FUNCT_1:def 7;
then g2.z in {x} by FUNCT_1:def 7;
then g2.z = x by TARSKI:def 1;
hence g1.z = g2.z by A20,TARSKI:def 1;
end;
hence g1.z = g2.z by A15;
end;
hence thesis by A10,A11,A6,A7,FUNCT_1:2;
end;
thus dom f = Funcs(X,{x,y}) by A1;
thus rng f c= bool X
proof
let z be object;
assume z in rng f;
then consider t being object such that
A21: t in dom f and
A22: z = f.t by FUNCT_1:def 3;
consider g such that
A23: t = g and
A24: dom g = X and
rng g c= {x,y} by A1,A21,FUNCT_2:def 2;
A25: g"{x} c= X by A24,RELAT_1:132;
z = g"{x} by A1,A21,A22,A23;
hence thesis by A25;
end;
deffunc G(object) = y;
let z be object;
reconsider zz=z as set by TARSKI:1;
defpred P[object] means $1 in zz;
consider g such that
A26: dom g = X &
for t being object st t in X holds (P[t] implies g.t = F(t)) & (
not P[t] implies g.t = G(t)) from PARTFUN1:sch 1;
assume
A27: z in bool X;
A28: g"{x} = zz
proof
thus g"{x} c= zz
proof
let t be object;
assume
A29: t in g"{x};
then g.t in {x} by FUNCT_1:def 7;
then
A30: g.t = x by TARSKI:def 1;
t in dom g by A29,FUNCT_1:def 7;
hence thesis by A2,A26,A30;
end;
let t be object;
assume
A31: t in zz;
then g.t = x by A27,A26;
then g.t in {x} by TARSKI:def 1;
hence thesis by A27,A26,A31,FUNCT_1:def 7;
end;
rng g c= {x,y}
proof
let t be object;
assume t in rng g;
then ex v being object st v in dom g & t = g.v by FUNCT_1:def 3;
then t = x or t = y by A26;
hence thesis by TARSKI:def 2;
end;
then
A32: g in Funcs(X,{x,y}) by A26,FUNCT_2:def 2;
then f.g = g"{x} by A1;
hence thesis by A1,A32,A28,FUNCT_1:def 3;
end;
hence thesis by CARD_1:5;
end;
theorem
x <> y implies Funcs({x,y},X),[:X,X:] are_equipotent & card Funcs({x,y
},X) = card [:X,X:]
proof
deffunc F(Function) = [ $1.x,$1.y];
consider f such that
A1: dom f = Funcs({x,y},X) & for g st g in Funcs({x,y},X) holds f.g = F(
g) from LambdaFS;
assume
A2: x <> y;
thus Funcs({x,y},X),[:X,X:] are_equipotent
proof
defpred P[object] means $1 = x;
take f;
thus f is one-to-one
proof
let x1,x2 be object;
assume that
A3: x1 in dom f and
A4: x2 in dom f and
A5: f.x1 = f.x2;
consider g2 such that
A6: x2 = g2 and
A7: dom g2 = {x,y} and
rng g2 c= X by A1,A4,FUNCT_2:def 2;
consider g1 such that
A8: x1 = g1 and
A9: dom g1 = {x,y} and
rng g1 c= X by A1,A3,FUNCT_2:def 2;
A10: [g1.x,g1.y] = f.x1 by A1,A3,A8
.= [g2.x,g2.y] by A1,A4,A5,A6;
now
let z be object;
assume z in {x,y};
then z = x or z = y by TARSKI:def 2;
hence g1.z = g2.z by A10,XTUPLE_0:1;
end;
hence thesis by A8,A9,A6,A7,FUNCT_1:2;
end;
thus dom f = Funcs({x,y},X) by A1;
thus rng f c= [:X,X:]
proof
let z be object;
assume z in rng f;
then consider t being object such that
A11: t in dom f and
A12: z = f.t by FUNCT_1:def 3;
consider g such that
A13: t = g and
A14: dom g = {x,y} and
A15: rng g c= X by A1,A11,FUNCT_2:def 2;
x in {x,y} by TARSKI:def 2;
then
A16: g.x in rng g by A14,FUNCT_1:def 3;
y in {x,y} by TARSKI:def 2;
then
A17: g.y in rng g by A14,FUNCT_1:def 3;
z = [g.x,g.y] by A1,A11,A12,A13;
hence thesis by A15,A16,A17,ZFMISC_1:87;
end;
let z be object;
deffunc F(object) = z`1;
deffunc G(object) = z`2;
consider g such that
A18: dom g = {x,y} &
for t being object st t in {x,y} holds (P[t] implies g.t = F(t
)) & (not P[t] implies g.t = G(t)) from PARTFUN1:sch 1;
x in {x,y} by TARSKI:def 2;
then
A19: g.x = z`1 by A18;
y in {x,y} by TARSKI:def 2;
then
A20: g.y = z`2 by A2,A18;
assume
A21: z in [:X,X:];
then
A22: z = [z`1,z`2] by MCART_1:21;
A23: z`1 in X & z`2 in X by A21,MCART_1:10;
rng g c= X
proof
let t be object;
assume t in rng g;
then ex a being object st a in dom g & t = g.a by FUNCT_1:def 3;
hence thesis by A23,A18;
end;
then
A24: g in Funcs({x,y},X) by A18,FUNCT_2:def 2;
then f.g = [g.x,g.y] by A1;
hence thesis by A1,A22,A24,A19,A20,FUNCT_1:def 3;
end;
hence thesis by CARD_1:5;
end;
begin :: Addenda
:: from VECTSP_2, MIDSP_1, 2007.11.26, A.T.
notation
synonym op0 for 0;
end;
definition
redefine func op0 -> Element of {0}; :: redefines op0 (FUNCT_5, synonym) → 0 (ORDINAL1, definition)
coherence by TARSKI:def 1;
end;
definition
func op1 -> set equals
0 .--> 0;
coherence;
func op2 -> set equals
(0,0) :-> 0;
coherence;
end;
definition
redefine func op1 -> UnOp of {0}; :: redefines op1 (FUNCT_5, definition)
coherence;
redefine func op2 -> BinOp of {0}; :: redefines op2 (FUNCT_5, definition)
coherence;
end;
:: from CAT_2, 2011.11.25, A.T.
reserve C,D,E for non empty set;
reserve c for Element of C,
d for Element of D;
definition
let D,X,E;
let F be FUNCTION_DOMAIN of X,E;
let f be Function of D,F;
let d be Element of D;
redefine func f.d -> Element of F; :: redefines . (FUNCT_1, definition)
coherence
proof
thus f.d is Element of F;
end;
end;
reserve f for Function of [:C,D:],E;
theorem Th60:
curry f is Function of C,Funcs(D,E)
proof
A1: dom f = [:C,D:] by FUNCT_2:def 1;
A2: rng curry f c= Funcs(D,E)
proof
A3: rng curry f c= Funcs(D,rng f) by A1,Th28;
let x be object;
assume x in rng curry f;
then consider g being Function such that
A4: x = g and
A5: dom g = D and
A6: rng g c= rng f by A3,FUNCT_2:def 2;
rng g c= E by A6,XBOOLE_1:1;
then g is Function of D,E by A5,FUNCT_2:def 1,RELSET_1:4;
hence thesis by A4,FUNCT_2:8;
end;
dom curry f = C by A1,Th17;
hence thesis by A2,FUNCT_2:def 1,RELSET_1:4;
end;
theorem Th61:
curry' f is Function of D,Funcs(C,E)
proof
A1: dom f = [:C,D:] by FUNCT_2:def 1;
A2: rng curry' f c= Funcs(C,E)
proof
A3: rng curry' f c= Funcs(C,rng f) by A1,Th28;
let x be object;
assume x in rng curry' f;
then consider g being Function such that
A4: x = g and
A5: dom g = C and
A6: rng g c= rng f by A3,FUNCT_2:def 2;
rng g c= E by A6,XBOOLE_1:1;
then g is Function of C,E by A5,FUNCT_2:def 1,RELSET_1:4;
hence thesis by A4,FUNCT_2:8;
end;
dom curry' f = D by A1,Th17;
hence thesis by A2,FUNCT_2:def 1,RELSET_1:4;
end;
definition
let C,D,E,f;
redefine func curry f -> Function of C,Funcs(D,E); :: redefines curry (FUNCT_5, definition)
coherence by Th60;
redefine func curry' f -> Function of D,Funcs(C,E); :: redefines curry' (FUNCT_5, definition)
coherence by Th61;
end;
theorem
f.(c,d) = ((curry f).c).d
proof
[c,d] in [:C,D:];
then [c,d] in dom f by FUNCT_2:def 1;
hence thesis by Th13;
end;
theorem
f.(c,d) = ((curry' f).d).c
proof
[c,d] in [:C,D:];
then [c,d] in dom f by FUNCT_2:def 1;
hence thesis by Th15;
end;
:: from ISOCAT_2, 2011.11.25, A.T.
definition
let A,B,C be non empty set;
let f be Function of A, Funcs(B,C);
redefine func uncurry f -> Function of [:A,B:],C; :: redefines uncurry (FUNCT_5, definition)
coherence
proof
A1: rng f c= Funcs(B,C);
then
A2: rng uncurry f c= C by Th34;
dom uncurry f = [:dom f,B:] by A1,Th19
.= [:A,B:] by FUNCT_2:def 1;
hence thesis by A2,FUNCT_2:def 1,RELSET_1:4;
end;
end;
theorem
for A,B,C being non empty set, f being Function of A,Funcs(B,C)
holds curry uncurry f = f
proof
let A,B,C be non empty set, f be Function of A,Funcs(B,C);
rng f c= Funcs(B,C);
hence thesis by Th41;
end;
theorem
for A,B,C being non empty set, f being Function of A, Funcs(B,C)
for a being Element of A, b being Element of B
holds (uncurry f).(a,b) = f.a.b
proof
let A,B,C be non empty set, f be Function of A, Funcs(B,C);
let a be Element of A, b be Element of B;
dom f = A & dom(f.a) = B by FUNCT_2:def 1;
hence thesis by Th31;
end;