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 )

given x being set such that A6:
x in dom f
and ( 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 A1, A2, PARTFUN1:def 6; :: 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 A4, PARTFUN1:def 6; :: thesis: verum

end;( 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 A1, A2, PARTFUN1:def 6; :: 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 A4, PARTFUN1:def 6; :: thesis: verum

A7: y = f /. x and

A8: for z being set st z in dom f & z <> x holds

f /. z <> y ; :: thesis: f just_once_values y

A9: for z being object st z in dom f & z <> x holds

f . z <> y

proof

y = f . x
by A6, A7, PARTFUN1:def 6;
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 A10, PARTFUN1:def 6; :: thesis: verum

end;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 A10, PARTFUN1:def 6; :: thesis: verum

hence f just_once_values y by A6, A9, FINSEQ_4:7; :: thesis: verum