let x0, x1, x2 be Real; for f being Function of REAL,REAL st x0,x1,x2 are_mutually_distinct holds
( [!f,x0,x1,x2!] = [!f,x2,x0,x1!] & [!f,x0,x1,x2!] = [!f,x1,x0,x2!] )
let f be Function of REAL,REAL; ( x0,x1,x2 are_mutually_distinct implies ( [!f,x0,x1,x2!] = [!f,x2,x0,x1!] & [!f,x0,x1,x2!] = [!f,x1,x0,x2!] ) )
assume A1:
x0,x1,x2 are_mutually_distinct
; ( [!f,x0,x1,x2!] = [!f,x2,x0,x1!] & [!f,x0,x1,x2!] = [!f,x1,x0,x2!] )
then A2:
x1 <> x2
by ZFMISC_1:def 5;
( x0 <> x1 & x0 <> x2 )
by A1, ZFMISC_1:def 5;
then A3:
x2,x0,x1 are_mutually_distinct
by A2, ZFMISC_1:def 5;
then
[!f,x0,x1,x2!] = [!f,x2,x0,x1!]
by Th34;
hence
( [!f,x0,x1,x2!] = [!f,x2,x0,x1!] & [!f,x0,x1,x2!] = [!f,x1,x0,x2!] )
by A3, Th34; verum