let x, y, z, a, b, c be set ; ( a <> b & b <> c & c <> a implies ex f being Function st
( f . a = x & f . b = y & f . c = z ) )
assume that
A1:
a <> b
and
A2:
b <> c
and
A3:
c <> a
; ex f being Function st
( f . a = x & f . b = y & f . c = z )
set fb = b .--> y;
A5:
a nin dom (b .--> y)
by A1, TARSKI:def 1;
A6:
b in dom (b .--> y)
by TARSKI:def 1;
set fc = c .--> z;
set fa = a .--> x;
take f = ((a .--> x) +* (b .--> y)) +* (c .--> z); ( f . a = x & f . b = y & f . c = z )
a nin dom (c .--> z)
by A3, TARSKI:def 1;
hence f . a =
((a .--> x) +* (b .--> y)) . a
by FUNCT_4:11
.=
(a .--> x) . a
by A5, FUNCT_4:11
.=
x
by FUNCOP_1:72
;
( f . b = y & f . c = z )
b nin dom (c .--> z)
by A2, TARSKI:def 1;
hence f . b =
((a .--> x) +* (b .--> y)) . b
by FUNCT_4:11
.=
(b .--> y) . b
by A6, FUNCT_4:13
.=
y
by FUNCOP_1:72
;
f . c = z
c in dom (c .--> z)
by TARSKI:def 1;
hence f . c =
(c .--> z) . c
by FUNCT_4:13
.=
z
by FUNCOP_1:72
;
verum