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

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