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,x0,x2,x1!]
let f be Function of REAL,REAL; :: thesis: ( x0,x1,x2 are_mutually_distinct implies [!f,x0,x1,x2!] = [!f,x0,x2,x1!] )
assume x0,x1,x2 are_mutually_distinct ; :: thesis: [!f,x0,x1,x2!] = [!f,x0,x2,x1!]
then A1: ( x2 - x1 <> 0 & x2 - x0 <> 0 & x1 - x0 <> 0 ) by ZFMISC_1:def 5;
set x10 = x1 - x0;
set x20 = x2 - x0;
set x21 = x2 - x1;
A2: [!f,x0,x2,x1!] = ((((f . x0) - (f . x2)) / (- (x2 - x0))) - (((f . x2) - (f . x1)) / (x2 - x1))) / (- (x1 - x0))
.= ((- (((f . x0) - (f . x2)) / (x2 - x0))) - (((f . x2) - (f . x1)) / (x2 - x1))) / (- (x1 - x0)) by XCMPLX_1:188
.= (- ((((f . x0) - (f . x2)) / (x2 - x0)) + (((f . x2) - (f . x1)) / (x2 - x1)))) / (- (x1 - x0))
.= ((((f . x0) - (f . x2)) / (x2 - x0)) + (((f . x2) - (f . x1)) / (x2 - x1))) / (x1 - x0) by XCMPLX_1:191
.= (((((f . x0) - (f . x2)) * (x2 - x1)) + (((f . x2) - (f . x1)) * (x2 - x0))) / ((x2 - x0) * (x2 - x1))) / (x1 - x0) by A1, XCMPLX_1:116
.= ((((f . x0) * (x2 - x1)) - ((f . x1) * (x2 - x0))) + ((f . x2) * (x1 - x0))) / (((x2 - x0) * (x2 - x1)) * (x1 - x0)) by XCMPLX_1:78 ;
[!f,x0,x1,x2!] = ((((f . x0) - (f . x1)) / (- (x1 - x0))) - (((f . x1) - (f . x2)) / (- (x2 - x1)))) / (- (x2 - x0))
.= ((- (((f . x0) - (f . x1)) / (x1 - x0))) - (((f . x1) - (f . x2)) / (- (x2 - x1)))) / (- (x2 - x0)) by XCMPLX_1:188
.= ((- (((f . x0) - (f . x1)) / (x1 - x0))) - (- (((f . x1) - (f . x2)) / (x2 - x1)))) / (- (x2 - x0)) by XCMPLX_1:188
.= (- ((((f . x0) - (f . x1)) / (x1 - x0)) - (((f . x1) - (f . x2)) / (x2 - x1)))) / (- (x2 - x0))
.= ((((f . x0) - (f . x1)) / (x1 - x0)) - (((f . x1) - (f . x2)) / (x2 - x1))) / (x2 - x0) by XCMPLX_1:191
.= (((((f . x0) - (f . x1)) * (x2 - x1)) - (((f . x1) - (f . x2)) * (x1 - x0))) / ((x1 - x0) * (x2 - x1))) / (x2 - x0) by A1, XCMPLX_1:130
.= ((((f . x0) * (x2 - x1)) - ((f . x1) * (x2 - x0))) + ((f . x2) * (x1 - x0))) / (((x1 - x0) * (x2 - x1)) * (x2 - x0)) by XCMPLX_1:78
.= [!f,x0,x2,x1!] by A2 ;
hence [!f,x0,x1,x2!] = [!f,x0,x2,x1!] ; :: thesis: verum