let x, X, y be set ; :: thesis: for f being Function st x in X & y in dom f holds
(X --> f) .. x,y = f . y
let f be Function; :: thesis: ( x in X & y in dom f implies (X --> f) .. x,y = f . y )
( dom (X --> f) = X & ( x in X implies (X --> f) . x = f ) ) by FUNCOP_1:13, FUNCOP_1:19;
hence ( x in X & y in dom f implies (X --> f) .. x,y = f . y ) by FUNCT_5:45; :: thesis: verum