hereby :: thesis: ( ex x being set st
( x in dom f & y = f /. x & ( for z being set st z in dom f & z <> x holds
f /. z <> y ) ) implies f just_once_values y )
assume f just_once_values y ; :: thesis: ex x being set st
( x in dom f & y = f /. x & ( for z being set st z in dom f & z <> x holds
f /. z <> y ) )

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: ( x in dom f & y = f /. x & ( for z being set st z in dom f & z <> x holds
f /. z <> y ) )

thus x in dom f by A1; :: thesis: ( y = f /. x & ( for z being set st z in dom f & z <> x holds
f /. z <> y ) )

thus y = f /. x by ; :: thesis: for z being set st z in dom f & z <> x holds
f /. z <> y

let z be set ; :: thesis: ( z in dom f & z <> x implies f /. z <> y )
assume that
A4: z in dom f and
A5: z <> x ; :: thesis: f /. z <> y
f . z <> y by A3, A4, A5;
hence f /. z <> y by ; :: thesis: verum
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
proof
let z be object ; :: thesis: ( z in dom f & z <> x implies f . z <> y )
assume that
A10: z in dom f and
A11: z <> x ; :: thesis: f . z <> y
f /. z <> y by A8, A10, A11;
hence f . z <> y by ; :: thesis: verum
end;
y = f . x by ;
hence f just_once_values y by ; :: thesis: verum