let X be set ; :: thesis: for x, y being object
for f being Function of X,{y} st x in X holds
f . x = y
let x, y be object ; :: thesis: for f being Function of X,{y} st x in X holds
f . x = y
let f be Function of X,{y}; :: thesis: ( x in X implies f . x = y )
( x in X implies f . x in {y} ) by Th5;
hence ( x in X implies f . x = y ) by TARSKI:def 1; :: thesis: verum