let x be set ; :: 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 A1: x in dom f ; :: thesis: x .--> (f . x) c= f
A3: dom (x .--> (f . x)) c= dom f

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in dom (x .--> (f . x)) or y in dom f )
thus ( not y in dom (x .--> (f . x)) or y in dom f ) by A1, FUNCOP_1:90; :: thesis: verum

end;

now

let y be set ; :: thesis: ( y in dom (x .--> (f . x)) implies (x .--> (f . x)) . y = f . y )
assume y in dom (x .--> (f . x)) ; :: thesis: (x .--> (f . x)) . y = f . y
then x = y by FUNCOP_1:90;
hence (x .--> (f . x)) . y = f . y by FUNCOP_1:87; :: thesis: verum

end;

hence x .--> (f . x) c= f by A3, GRFUNC_1:8; :: thesis: verum