let f be Function; 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 ; ( 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 ) ) )
( 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
;
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
;
( 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;
for z being object st z in dom f & z <> x1 holds
f . z <> y
let z be
object ;
( 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
;
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
;
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
; f just_once_values y
A13:
{x} = f " {y}
card (Coim (f,y)) = 1
by A13, CARD_1:30;
hence
f just_once_values y
; verum