let x0, x1, x2 be Real; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( [!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; :: thesis: verum