let f be Function; :: thesis:
let y be object ; :: thesis:
thus ( f just_once_values y implies ex x being object st
( x in dom f & y = f . x & ( for z being object st z in dom f & z <> x holds
f . z <> y ) ) ) :: thesis:

assume A1: f just_once_values y ; :: thesis:
then A2: card (Coim (f,y)) = 1 ;
y in rng f by A1, Th5;
then consider x1 being object such that
A3: x1 in dom f and
A4: f . x1 = y by FUNCT_1:def 3;
f . x1 in {y} by A4, TARSKI:def 1;
then A5: x1 in f " {y} by A3, FUNCT_1:def 7;
take x1 ; :: thesis:
thus ( x1 in dom f & y = f . x1 ) by A3, A4; :: thesis:
let z be object ; :: thesis:
assume that
A6: z in dom f and
A7: z <> x1 and
A8: f . z = y ; :: thesis:
A9: f " {y} is finite by A2;
f . z in {y} by A8, TARSKI:def 1;
then z in f " {y} by A6, FUNCT_1:def 7;
then {z,x1} c= f " {y} by A5, ZFMISC_1:32;
then card {z,x1} <= 1 by A9, A2, NAT_1:43;
then 2 <= 1 by A7, CARD_2:57;
hence contradiction ; :: thesis:

end;

given x being object such that A10: x in dom f and
A11: y = f . x and
A12: for z being object st z in dom f & z <> x holds
f . z <> y ; :: thesis:
A13: {x} = f " {y}

thus {x} c= f " {y} :: according to XBOOLE_0:def 10 :: thesis:

let x1 be object ; :: according to TARSKI:def 3 :: thesis:
assume x1 in {x} ; :: thesis:
then A14: x1 = x by TARSKI:def 1;
f . x in {y} by A11, TARSKI:def 1;
hence x1 in f " {y} by A10, A14, FUNCT_1:def 7; :: thesis:

end;

let x1 be object ; :: according to TARSKI:def 3 :: thesis:
assume A15: x1 in f " {y} ; :: thesis:
then f . x1 in {y} by FUNCT_1:def 7;
then A16: f . x1 = y by TARSKI:def 1;
x1 in dom f by A15, FUNCT_1:def 7;
then x1 = x by A12, A16;
hence x1 in {x} by TARSKI:def 1; :: thesis:

end;

card (Coim (f,y)) = 1 by A13, CARD_1:30;
hence f just_once_values y ; :: thesis: