let a, b, x, y, z be set ; for c being complex number st a,b,c are_mutually_different holds
( ((a,b,c) --> (x,y,z)) . a = x & ((a,b,c) --> (x,y,z)) . b = y & ((a,b,c) --> (x,y,z)) . c = z )
let c be complex number ; ( a,b,c are_mutually_different implies ( ((a,b,c) --> (x,y,z)) . a = x & ((a,b,c) --> (x,y,z)) . b = y & ((a,b,c) --> (x,y,z)) . c = z ) )
assume A1:
a,b,c are_mutually_different
; ( ((a,b,c) --> (x,y,z)) . a = x & ((a,b,c) --> (x,y,z)) . b = y & ((a,b,c) --> (x,y,z)) . c = z )
set f = (a,b) --> (x,y);
set g = c .--> z;
set h = (a,b,c) --> (x,y,z);
A2:
a <> b
by A1, ZFMISC_1:def 5;
a <> c
by A1, ZFMISC_1:def 5;
then A3:
not a in {c}
by TARSKI:def 1;
b <> c
by A1, ZFMISC_1:def 5;
then A4:
not b in {c}
by TARSKI:def 1;
A5:
c in {c}
by TARSKI:def 1;
A6:
dom (c .--> z) = {c}
by FUNCOP_1:13;
hence ((a,b,c) --> (x,y,z)) . a =
((a,b) --> (x,y)) . a
by A3, FUNCT_4:11
.=
x
by A2, FUNCT_4:63
;
( ((a,b,c) --> (x,y,z)) . b = y & ((a,b,c) --> (x,y,z)) . c = z )
thus ((a,b,c) --> (x,y,z)) . b =
((a,b) --> (x,y)) . b
by A4, A6, FUNCT_4:11
.=
y
by FUNCT_4:63
; ((a,b,c) --> (x,y,z)) . c = z
thus ((a,b,c) --> (x,y,z)) . c =
(c .--> z) . c
by A5, A6, FUNCT_4:13
.=
z
by FUNCOP_1:72
; verum