let x, y be object ; :: thesis: for f being Function st f = {[x,y]} holds
f . x = y
let f be Function; :: thesis: ( f = {[x,y]} implies f . x = y )
assume f = {[x,y]} ; :: thesis: f . x = y
then [x,y] in f by TARSKI:def 1;
hence f . x = y by FUNCT_1:1; :: thesis: verum