let a, b, c, d be object ; :: thesis: ( a <> c implies (a,c) --> (b,d) = {[a,b],[c,d]} )
assume A1: a <> c ; :: thesis: (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 ;
:: thesis: verum