let a, b, c, x, y, z be object ; :: 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, Th128; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom f or f . b₁ = ((a,b,c) --> (x,y,z)) . b₁ )
let k be object ; :: 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_distinct or ( a = b & a <> c ) or a = c or ( b = c & a <> c ) ) ;

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

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

end;

suppose A4: ( 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 Th81;
hence f . k = ((a,b,c) --> (x,y,z)) . k by A4, A2, A3, Th63; :: thesis: verum

end;

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

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

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

then (a,b,c) --> (x,y,z) = (a,b) --> (z,y) by A5, Th132;
hence f . k = ((a,b,c) --> (x,y,z)) . k by A5, A2, A3, A6, Th63; :: 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 A5, A2, A3, FUNCOP_1:72; :: thesis: verum

end;

end;

end;

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

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

end;

end;