let x, y, z, a, b, c be set ; :: thesis: ( a <> b & b <> c & c <> a implies ex f being Function st
( f . a = x & f . b = y & f . c = z ) )
assume Z1: ( a <> b & b <> c & c <> a ) ; :: thesis: ex f being Function st
( f . a = x & f . b = y & f . c = z )
set fa = a .--> x;
set fb = b .--> y;
set fc = c .--> z;
take f = ((a .--> x) +* (b .--> y)) +* (c .--> z); :: thesis: ( f . a = x & f . b = y & f . c = z )
( dom (c .--> z) = {c} & dom (b .--> y) = {b} & dom (a .--> x) = {a} ) by FUNCOP_1:19;
then Z2: ( a nin dom (c .--> z) & a nin dom (b .--> y) & b nin dom (c .--> z) & b in dom (b .--> y) & c in dom (c .--> z) ) by Z1, TARSKI:def 1;
thus f . a = ((a .--> x) +* (b .--> y)) . a by Z2, FUNCT_4:12
.= (a .--> x) . a by Z2, FUNCT_4:12
.= x by FUNCOP_1:87 ; :: thesis: ( f . b = y & f . c = z )
thus f . b = ((a .--> x) +* (b .--> y)) . b by Z2, FUNCT_4:12
.= (b .--> y) . b by Z2, FUNCT_4:14
.= y by FUNCOP_1:87 ; :: thesis: f . c = z
thus f . c = (c .--> z) . c by Z2, FUNCT_4:14
.= z by FUNCOP_1:87 ; :: thesis: verum