let x, y be object ; :: thesis: for X being set
for f being Function st x in X & y in dom f holds
(X --> f) .. (x,y) = f . y
let X 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:7;
dom (X --> f) = X ;
hence ( x in X & y in dom f implies (X --> f) .. (x,y) = f . y ) by A1, FUNCT_5:38; :: thesis: verum