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