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 )

A1: now :: thesis: for y being object st y in dom (x .--> (f . x)) holds
(x .--> (f . x)) . y = f . y

let y be object ; :: 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:75;
hence (x .--> (f . x)) . y = f . y by FUNCOP_1:72; :: thesis: verum

end;

assume A2: x in dom f ; :: thesis: x .--> (f . x) c= f
dom (x .--> (f . x)) c= dom f by A2, FUNCOP_1:75;
hence x .--> (f . x) c= f by A1, GRFUNC_1:2; :: thesis: verum