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 that
A1: a in dom f and
A2: c in dom f and
A3: ( f . a = b & f . c = d ) ; :: thesis: (a,c) --> (b,d) c= f
per cases ( a <> c or a = c ) ;
suppose A4: a <> c ; :: thesis: (a,c) --> (b,d) c= f
( [a,b] in f & [c,d] in f ) by A1, A2, A3, FUNCT_1:1;
then {[a,b],[c,d]} c= f by ZFMISC_1:32;
hence (a,c) --> (b,d) c= f by A4, Th67; :: thesis: verum
end;
suppose a = c ; :: thesis: (a,c) --> (b,d) c= f
hence (a,c) --> (b,d) c= f by A1, A3, Th85; :: thesis: verum
end;
end;