let a, b be set ; :: thesis: for f being Function st a in dom f & f . a = b holds
a .--> b c= f
let f be Function; :: thesis: ( a in dom f & f . a = b implies a .--> b c= f )
assume ( a in dom f & f . a = b ) ; :: thesis: a .--> b c= f
then [a,b] in f by FUNCT_1:1;
then {[a,b]} c= f by ZFMISC_1:31;
hence a .--> b c= f by ZFMISC_1:29; :: thesis: verum