let a, b be object ; :: thesis: for f being Function holds
( a .--> b c= f iff ( a in dom f & f . a = b ) )
let f be Function; :: thesis: ( a .--> b c= f iff ( a in dom f & f . a = b ) )
A1: dom (a .--> b) = {a} ;
A2: a in dom (a .--> b) by TARSKI:def 1;

hereby :: thesis: ( a in dom f & f . a = b implies a .--> b c= f )

assume A3: a .--> b c= f ; :: thesis: ( a in dom f & f . a = b )
then {a} c= dom f by A1, GRFUNC_1:2;
hence a in dom f by ZFMISC_1:31; :: thesis: f . a = b
thus f . a = (a .--> b) . a by A2, A3, GRFUNC_1:2
.= b by Th72 ; :: thesis: verum

end;

assume that
A4: a in dom f and
A5: f . a = b ; :: thesis: a .--> b c= f

A6: now :: thesis: for x being object st x in dom (a .--> b) holds
(a .--> b) . x = f . x

let x be object ; :: thesis: ( x in dom (a .--> b) implies (a .--> b) . x = f . x )
assume x in dom (a .--> b) ; :: thesis: (a .--> b) . x = f . x
then x = a by TARSKI:def 1;
hence (a .--> b) . x = f . x by A5, Th72; :: thesis: verum

end;

dom (a .--> b) c= dom f by A4, ZFMISC_1:31;
hence a .--> b c= f by A6, GRFUNC_1:2; :: thesis: verum