assume f just_once_values y ; :: thesis:
then consider x being object such that
A1: x in dom f and
A2: y = f . x and
A3: for z being object st z in dom f & z <> x holds
f . z <> y by FINSEQ_4:7;
reconsider x = x as set by TARSKI:1;
take x = x; :: thesis:
thus x in dom f by A1; :: thesis:
thus y = f /. x by A1, A2, PARTFUN1:def 6; :: thesis:
let z be set ; :: thesis:
assume that
A4: z in dom f and
A5: z <> x ; :: thesis:
f . z <> y by A3, A4, A5;
hence f /. z <> y by A4, PARTFUN1:def 6; :: thesis:

end;

given x being set such that A6: x in dom f and
A7: y = f /. x and
A8: for z being set st z in dom f & z <> x holds
f /. z <> y ; :: thesis:
A9: for z being object st z in dom f & z <> x holds
f . z <> y

end;