let a, b, c, d be set ; :: 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;
A2: ( dom ({a} --> b) = {a} & dom ({c} --> d) = {c} ) by FUNCOP_1:13;
( {a} --> b = {[a,b]} & {c} --> d = {[c,d]} ) by ZFMISC_1:29;
hence (a,c) --> (b,d) = {[a,b]} \/ {[c,d]} by A1, A2, Th32, ZFMISC_1:11
.= {[a,b],[c,d]} by ENUMSET1:1 ;
:: thesis: verum