let a, b, c, d be set ; :: thesis: for f being Function st a in dom f & c in dom f & f . a = b & f . c = d holds
a,c --> b,d c= f
let f be Function; :: thesis: ( a in dom f & c in dom f & f . a = b & f . c = d implies a,c --> b,d c= f )
assume A1: ( a in dom f & c in dom f & f . a = b & f . c = d ) ; :: thesis: a,c --> b,d c= f

per cases ( a <> c or a = c ) ;

suppose A2: a <> c ; :: thesis: a,c --> b,d c= f

( [a,b] in f & [c,d] in f ) by A1, FUNCT_1:8;
then {[a,b],[c,d]} c= f by ZFMISC_1:38;
hence a,c --> b,d c= f by A2, Th71; :: thesis: verum

end;

suppose a = c ; :: thesis: a,c --> b,d c= f

hence a,c --> b,d c= f by A1, Th90; :: thesis: verum

end;

end;