let a, c, x, w, b, d, y, z be set ; :: thesis: ( 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 a,c,x,w are_mutually_different ; :: thesis: a,c,x,w --> b,d,y,z = {[a,b],[c,d],[x,y],[w,z]}
then A1: ( a <> c & a <> x & a <> w & c <> x & c <> w & x <> w ) by ZFMISC_1:def 6;
set m = a,c --> b,d;
set n = x,w --> y,z;
A2: ( dom (a,c --> b,d) = {a,c} & dom (x,w --> y,z) = {x,w} ) by FUNCT_4:65;
( not a in {x,w} & not c in {x,w} ) by A1, TARSKI:def 2;
then a,c,x,w --> b,d,y,z = (a,c --> b,d) \/ (x,w --> y,z) by A2, FUNCT_4:32, ZFMISC_1:57
.= {[a,b],[c,d]} \/ (x,w --> y,z) by A1, FUNCT_4:71
.= {[a,b],[c,d]} \/ {[x,y],[w,z]} by A1, 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]} ; :: thesis: verum