let a, b, x, y, z be set ; :: thesis: for c being complex number
for f being Function st dom f = {a,b,c} & f . a = x & f . b = y & f . c = z holds
f = (a,b,c) --> (x,y,z)
let c be complex number ; :: thesis: for f being Function st dom f = {a,b,c} & f . a = x & f . b = y & f . c = z holds
f = (a,b,c) --> (x,y,z)
let f be Function; :: thesis: ( dom f = {a,b,c} & f . a = x & f . b = y & f . c = z implies f = (a,b,c) --> (x,y,z) )
assume that
A1: dom f = {a,b,c} and
A2: ( f . a = x & f . b = y & f . c = z ) ; :: thesis: f = (a,b,c) --> (x,y,z)
set g = (a,b,c) --> (x,y,z);
thus dom f = dom ((a,b,c) --> (x,y,z)) by A1, BVFUNC14:11; :: according to FUNCT_1:def 11 :: thesis: for b₁ being set holds
( not b₁ in dom f or f . b₁ = ((a,b,c) --> (x,y,z)) . b₁ )
let k be set ; :: thesis: ( not k in dom f or f . k = ((a,b,c) --> (x,y,z)) . k )
assume k in dom f ; :: thesis: f . k = ((a,b,c) --> (x,y,z)) . k
then A3: ( k = a or k = b or k = c ) by A1, ENUMSET1:def 1;

per cases ( a,b,c are_mutually_different or not a,b,c are_mutually_different ) ;

suppose a,b,c are_mutually_different ; :: thesis: f . k = ((a,b,c) --> (x,y,z)) . k

hence f . k = ((a,b,c) --> (x,y,z)) . k by A2, A3, Th28; :: thesis: verum

end;

suppose A4: not a,b,c are_mutually_different ; :: thesis: f . k = ((a,b,c) --> (x,y,z)) . k

per cases ( ( a = b & a <> c ) or a = c or ( b = c & a <> c ) ) by A4, ZFMISC_1:def 5;

suppose A5: ( a = b & a <> c ) ; :: thesis: f . k = ((a,b,c) --> (x,y,z)) . k

then (a,b,c) --> (x,y,z) = (a,c) --> (y,z) by FUNCT_4:81;
hence f . k = ((a,b,c) --> (x,y,z)) . k by A5, A2, A3, FUNCT_4:63; :: thesis: verum

end;

suppose A6: a = c ; :: thesis: f . k = ((a,b,c) --> (x,y,z)) . k

per cases ( a <> b or a = b ) ;

suppose A7: a <> b ; :: thesis: f . k = ((a,b,c) --> (x,y,z)) . k

then (a,b,c) --> (x,y,z) = (a,b) --> (z,y) by A6, Th25;
hence f . k = ((a,b,c) --> (x,y,z)) . k by A6, A2, A3, A7, FUNCT_4:63; :: thesis: verum

end;

suppose a = b ; :: thesis: f . k = ((a,b,c) --> (x,y,z)) . k

hence f . k = ((a,b,c) --> (x,y,z)) . k by A6, A2, A3, FUNCOP_1:72; :: thesis: verum

end;

end;

end;

suppose A8: ( b = c & a <> c ) ; :: thesis: f . k = ((a,b,c) --> (x,y,z)) . k

then (a,b,c) --> (x,y,z) = (a,b) --> (x,z) by Th26;
hence f . k = ((a,b,c) --> (x,y,z)) . k by A8, A2, A3, FUNCT_4:63; :: thesis: verum

end;

end;

end;

end;