let x be object ; :: thesis: for f being Function st x in dom f holds
x .--> (f . x) c= f
let f be Function; :: thesis: ( x in dom f implies x .--> (f . x) c= f )
assume x in dom f ; :: thesis: x .--> (f . x) c= f
then {[x,(f . x)]} c= f by ZFMISC_1:31, FUNCT_1:1;
hence x .--> (f . x) c= f by ZFMISC_1:29; :: thesis: verum