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 )

A1: 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;

assume A2: x in dom f ; :: thesis: x .--> (f . x) c= f
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 A2, FUNCOP_1:90; :: thesis: verum

end;

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