let a, c, x, w, b, d, y, z be set ; ( a,c,x,w are_mutually_different 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_different
; (a,c,x,w) --> (b,d,y,z) = {[a,b],[c,d],[x,y],[w,z]}
then A2:
a <> c
by ZFMISC_1:def 6;
A3:
a <> x
by A1, ZFMISC_1:def 6;
A4:
a <> w
by A1, ZFMISC_1:def 6;
A5:
c <> x
by A1, ZFMISC_1:def 6;
A6:
c <> w
by A1, ZFMISC_1:def 6;
A7:
x <> w
by A1, ZFMISC_1:def 6;
set m = (a,c) --> (b,d);
set n = (x,w) --> (y,z);
A8:
dom ((a,c) --> (b,d)) = {a,c}
by FUNCT_4:65;
A9:
dom ((x,w) --> (y,z)) = {x,w}
by FUNCT_4:65;
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, FUNCT_4:32, ZFMISC_1:57
.=
{[a,b],[c,d]} \/ ((x,w) --> (y,z))
by A2, FUNCT_4:71
.=
{[a,b],[c,d]} \/ {[x,y],[w,z]}
by A7, FUNCT_4:71
.=
{[a,b],[c,d],[x,y],[w,z]}
by ENUMSET1:45
;
hence
(a,c,x,w) --> (b,d,y,z) = {[a,b],[c,d],[x,y],[w,z]}
; verum