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 set such that
A1: x in dom f and
A2: y = f . x and
A3: for z being set st z in dom f & z <> x holds
f . z <> y by FINSEQ_4:9;
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 A1, A2, PARTFUN1:def 8; :: 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 A4: ( z in dom f & z <> x ) ; :: thesis: f /. z <> y
then f . z <> y by A3;
hence f /. z <> y by A4, PARTFUN1:def 8; :: thesis: verum

end;

given x being set such that A5: x in dom f and
A6: y = f /. x and
A7: for z being set st z in dom f & z <> x holds
f /. z <> y ; :: thesis: f just_once_values y
A8: y = f . x by A5, A6, PARTFUN1:def 8;
for z being set st z in dom f & z <> x holds
f . z <> y

proof

let z be set ; :: thesis: ( z in dom f & z <> x implies f . z <> y )
assume A9: ( z in dom f & z <> x ) ; :: thesis: f . z <> y
then f /. z <> y by A7;
hence f . z <> y by A9, PARTFUN1:def 8; :: thesis: verum

end;

hence f just_once_values y by A5, A8, FINSEQ_4:9; :: thesis: verum