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: ( {a} --> b = {[a,b]} & {c} --> d = {[c,d]} ) by ZFMISC_1:35;
( dom ({a} --> b) = {a} & dom ({c} --> d) = {c} ) by FUNCOP_1:19;
hence a,c --> b,d = {[a,b]} \/ {[c,d]} by A1, A2, Th32, ZFMISC_1:17
.= {[a,b],[c,d]} by ENUMSET1:41 ;
:: thesis: verum