let a, b, c, d be object ; ( a <> c implies (a,c) --> (b,d) = {[a,b],[c,d]} )
assume A1:
a <> c
; (a,c) --> (b,d) = {[a,b],[c,d]}
set f = {a} --> b;
set g = {c} --> d;
( {a} --> b = {[a,b]} & {c} --> d = {[c,d]} )
by ZFMISC_1:29;
hence (a,c) --> (b,d) =
{[a,b]} \/ {[c,d]}
by A1, Th31, ZFMISC_1:11
.=
{[a,b],[c,d]}
by ENUMSET1:1
;
verum