let X1, X2, Y1, Y2 be set ; ( 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)) ) )
assume that
A1:
X1,Y1 are_equipotent
and
A2:
X2,Y2 are_equipotent
; ( Funcs (X1,X2), Funcs (Y1,Y2) are_equipotent & card (Funcs (X1,X2)) = card (Funcs (Y1,Y2)) )
consider f1 being Function 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 being Function 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 H1(
Function)
-> set =
f2 * ($1 * f1);
consider F being
Function such that A10:
(
dom F = Funcs (
X1,
X2) & ( for
g being
Function st
g in Funcs (
X1,
X2) holds
F . g = H1(
g) ) )
from FUNCT_5:sch 1();
take
F
;
WELLORD2:def 4 ( F is one-to-one & proj1 F = Funcs (X1,X2) & proj2 F = Funcs (Y1,Y2) )
thus
F is
one-to-one
( proj1 F = Funcs (X1,X2) & proj2 F = Funcs (Y1,Y2) )proof
let x,
y be
object ;
FUNCT_1:def 4 ( not x in proj1 F or not y in proj1 F or not F . x = F . y or x = y )
assume that A11:
x in dom F
and A12:
y in dom F
and A13:
F . x = F . y
;
x = 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, RELAT_1: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, RELAT_1: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;
hence
x = y
by A14, A15, A19, A20, FUNCT_1:2;
verum
end;
thus
dom F = Funcs (
X1,
X2)
by A10;
proj2 F = Funcs (Y1,Y2)
thus
rng F c= Funcs (
Y1,
Y2)
XBOOLE_0:def 10 Funcs (Y1,Y2) c= proj2 Fproof
let x be
object ;
TARSKI:def 3 ( not x in rng F or x in Funcs (Y1,Y2) )
assume
x in rng F
;
x in Funcs (Y1,Y2)
then consider y being
object such that A25:
y in dom F
and A26:
x = F . y
by FUNCT_1:def 3;
consider g being
Function 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, RELAT_1: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
x in Funcs (
Y1,
Y2)
by A29, A30, FUNCT_2:def 2;
verum
end;
let x be
object ;
TARSKI:def 3 ( not x in Funcs (Y1,Y2) or x in proj2 F )
assume
x in Funcs (
Y1,
Y2)
;
x in proj2 F
then consider g being
Function 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
x in proj2 F
by A37, A34, FUNCT_1:def 3;
verum
end;
hence
( Funcs (X1,X2), Funcs (Y1,Y2) are_equipotent & card (Funcs (X1,X2)) = card (Funcs (Y1,Y2)) )
by CARD_1:5; verum