let a, b be set ; :: 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} by Th19;
then 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:8;
hence a in dom f by ZFMISC_1:37; :: thesis: f . a = b
thus f . a = (a .--> b) . a by A2, A3, GRFUNC_1:8
.= b by Th87 ; :: thesis: verum

end;

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

A6: now

let x be set ; :: 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 A1, TARSKI:def 1;
hence (a .--> b) . x = f . x by A5, Th87; :: thesis: verum

end;

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