let x0, x1, x2 be Real; :: thesis: for f being Function of REAL ,REAL st x0,x1,x2 are_mutually_different 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_different implies ( [!f,x0,x1,x2!] = [!f,x2,x0,x1!] & [!f,x0,x1,x2!] = [!f,x1,x0,x2!] ) )
assume x0,x1,x2 are_mutually_different ; :: thesis: ( [!f,x0,x1,x2!] = [!f,x2,x0,x1!] & [!f,x0,x1,x2!] = [!f,x1,x0,x2!] )
then ( x0 <> x1 & x0 <> x2 & x1 <> x2 ) by ZFMISC_1:def 5;
then A1: x2,x0,x1 are_mutually_different by 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 A1, Th34; :: thesis: verum