let a, c, b, d, x, y, z, w be object ; ( a,c,x,w are_mutually_distinct implies (a,c,x,w) --> (b,d,y,z) = {[a,b],[c,d],[x,y],[w,z]} )
assume A1:
a,c,x,w are_mutually_distinct
; (a,c,x,w) --> (b,d,y,z) = {[a,b],[c,d],[x,y],[w,z]}
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);
set n = (x,w) --> (y,z);
A8:
dom ((a,c) --> (b,d)) = {a,c}
by Th62;
A9:
dom ((x,w) --> (y,z)) = {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) =
((a,c) --> (b,d)) \/ ((x,w) --> (y,z))
by A8, A9, A10, Th31, ZFMISC_1:51
.=
{[a,b],[c,d]} \/ ((x,w) --> (y,z))
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
(a,c,x,w) --> (b,d,y,z) = {[a,b],[c,d],[x,y],[w,z]}
; verum