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;

A4: a in dom f and

A5: f . a = b ; :: thesis: a .--> b c= f

hence a .--> b c= f by A6, GRFUNC_1:2; :: thesis: verum

( 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 that 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;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

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

dom (a .--> b) c= dom f
by A4, ZFMISC_1:31;(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;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

hence a .--> b c= f by A6, GRFUNC_1:2; :: thesis: verum