let f be Function; :: thesis: for y being object holds
( f just_once_values y iff 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 ) ) )
let y be object ; :: thesis: ( f just_once_values y iff 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 ) ) )
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: ( 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 ) ) implies f just_once_values y )

proof

assume A1: f just_once_values y ; :: thesis: 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 ) )
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: ( x1 in dom f & y = f . x1 & ( for z being object st z in dom f & z <> x1 holds
f . z <> y ) )
thus ( x1 in dom f & y = f . x1 ) by A3, A4; :: thesis: for z being object st z in dom f & z <> x1 holds
f . z <> y
let z be object ; :: thesis: ( z in dom f & z <> x1 implies f . z <> y )
assume that
A6: z in dom f and
A7: z <> x1 and
A8: f . z = y ; :: thesis: contradiction
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: verum

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: f just_once_values y
A13: {x} = f " {y}

proof

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

proof

let x1 be object ; :: according to TARSKI:def 3 :: thesis: ( not x1 in {x} or x1 in f " {y} )
assume x1 in {x} ; :: thesis: x1 in f " {y}
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: verum

end;

let x1 be object ; :: according to TARSKI:def 3 :: thesis: ( not x1 in f " {y} or x1 in {x} )
assume A15: x1 in f " {y} ; :: thesis: x1 in {x}
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: verum

end;

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