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 )
A1: ( x in X implies (X --> f) . x = f ) by FUNCOP_1:13;
dom (X --> f) = X by FUNCOP_1:19;
hence ( x in X & y in dom f implies (X --> f) .. (x,y) = f . y ) by A1, FUNCT_5:45; :: thesis: verum