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

proof

assume A1: 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 A2: ex B being finite set st
( B = f " {y} & card B = 1 ) by Def2;
y in rng f by A1, Th7;
then consider x1 being set such that
A3: x1 in dom f and
A4: f . x1 = y by FUNCT_1:def 5;
f . x1 in {y} by A4, TARSKI:def 1;
then A5: x1 in f " {y} by A3, FUNCT_1:def 13;
take x1 ; :: thesis: ( x1 in dom f & y = f . x1 & ( for z being set 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 set st z in dom f & z <> x1 holds
f . z <> y
let z be set ; :: 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
f . z in {y} by A8, TARSKI:def 1;
then z in f " {y} by A6, FUNCT_1:def 13;
then {z,x1} c= f " {y} by A5, ZFMISC_1:38;
then card {z,x1} <= 1 by A2, NAT_1:44;
then 2 <= 1 by A7, CARD_2:76;
hence contradiction ; :: thesis: verum

end;

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

proof

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

proof

let x1 be set ; :: 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 A13: x1 = x by TARSKI:def 1;
f . x in {y} by A10, TARSKI:def 1;
hence x1 in f " {y} by A9, A13, FUNCT_1:def 13; :: thesis: verum

end;

let x1 be set ; :: according to TARSKI:def 3 :: thesis: ( not x1 in f " {y} or x1 in {x} )
assume A14: x1 in f " {y} ; :: thesis: x1 in {x}
then f . x1 in {y} by FUNCT_1:def 13;
then A15: f . x1 = y by TARSKI:def 1;
x1 in dom f by A14, FUNCT_1:def 13;
then x1 = x by A11, A15;
hence x1 in {x} by TARSKI:def 1; :: thesis: verum

end;

then reconsider B = f " {y} as finite set ;
card B = 1 by A12, CARD_1:50;
hence f just_once_values y by Def2; :: thesis: verum