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) / ((x0 - x1) * (x0 - x2))) + ((f . x1) / ((x1 - x0) * (x1 - x2)))) + ((f . x2) / ((x2 - x0) * (x2 - x1)))
let f be Function of REAL,REAL; :: thesis: ( x0,x1,x2 are_mutually_distinct implies [!f,x0,x1,x2!] = (((f . x0) / ((x0 - x1) * (x0 - x2))) + ((f . x1) / ((x1 - x0) * (x1 - x2)))) + ((f . x2) / ((x2 - x0) * (x2 - x1))) )
assume A1: x0,x1,x2 are_mutually_distinct ; :: thesis: [!f,x0,x1,x2!] = (((f . x0) / ((x0 - x1) * (x0 - x2))) + ((f . x1) / ((x1 - x0) * (x1 - x2)))) + ((f . x2) / ((x2 - x0) * (x2 - x1)))
then A2: x1 - x2 <> 0 by ZFMISC_1:def 5;
A3: x0 - x1 <> 0 by A1, ZFMISC_1:def 5;
A4: x0 - x2 <> 0 by A1, ZFMISC_1:def 5;
[!f,x0,x1,x2!] = ((((f . x0) - (f . x1)) / (x0 - x1)) / (x0 - x2)) - ((((f . x1) - (f . x2)) / (x1 - x2)) / (x0 - x2)) by XCMPLX_1:120
.= (((f . x0) - (f . x1)) / ((x0 - x1) * (x0 - x2))) - ((((f . x1) - (f . x2)) / (x1 - x2)) / (x0 - x2)) by XCMPLX_1:78
.= (((f . x0) - (f . x1)) / ((x0 - x1) * (x0 - x2))) - (((f . x1) - (f . x2)) / ((x1 - x2) * (x0 - x2))) by XCMPLX_1:78
.= (((f . x0) / ((x0 - x1) * (x0 - x2))) - ((f . x1) / ((x0 - x1) * (x0 - x2)))) - (((f . x1) - (f . x2)) / ((x1 - x2) * (x0 - x2))) by XCMPLX_1:120
.= (((f . x0) / ((x0 - x1) * (x0 - x2))) - ((f . x1) / ((x0 - x1) * (x0 - x2)))) - (((f . x1) / ((x1 - x2) * (x0 - x2))) - ((f . x2) / ((x1 - x2) * (x0 - x2)))) by XCMPLX_1:120
.= (((f . x0) / ((x0 - x1) * (x0 - x2))) - (((f . x1) / ((x0 - x1) * (x0 - x2))) + ((f . x1) / ((x1 - x2) * (x0 - x2))))) + ((f . x2) / ((x1 - x2) * (x0 - x2)))
.= (((f . x0) / ((x0 - x1) * (x0 - x2))) - ((((f . x1) * (x1 - x2)) / (((x0 - x1) * (x0 - x2)) * (x1 - x2))) + ((f . x1) / ((x1 - x2) * (x0 - x2))))) + ((f . x2) / ((x1 - x2) * (x0 - x2))) by A2, XCMPLX_1:91
.= (((f . x0) / ((x0 - x1) * (x0 - x2))) - ((((f . x1) * (x1 - x2)) / (((x0 - x1) * (x0 - x2)) * (x1 - x2))) + (((f . x1) * (x0 - x1)) / (((x1 - x2) * (x0 - x2)) * (x0 - x1))))) + ((f . x2) / ((x1 - x2) * (x0 - x2))) by A3, XCMPLX_1:91
.= (((f . x0) / ((x0 - x1) * (x0 - x2))) - ((((f . x1) * (x1 - x2)) + ((f . x1) * (x0 - x1))) / (((x0 - x1) * (x0 - x2)) * (x1 - x2)))) + ((f . x2) / ((x1 - x2) * (x0 - x2))) by XCMPLX_1:62
.= (((f . x0) / ((x0 - x1) * (x0 - x2))) - (((f . x1) * (x0 - x2)) / (((x0 - x1) * (x1 - x2)) * (x0 - x2)))) + ((f . x2) / ((x1 - x2) * (x0 - x2)))
.= (((f . x0) / ((x0 - x1) * (x0 - x2))) - ((f . x1) / (- ((x1 - x0) * (x1 - x2))))) + ((f . x2) / (- ((x2 - x1) * (x0 - x2)))) by A4, XCMPLX_1:91
.= (((f . x0) / ((x0 - x1) * (x0 - x2))) + (- ((f . x1) / (- ((x1 - x0) * (x1 - x2)))))) + ((f . x2) / ((- (x2 - x1)) * (- (x2 - x0)))) ;
hence [!f,x0,x1,x2!] = (((f . x0) / ((x0 - x1) * (x0 - x2))) + ((f . x1) / ((x1 - x0) * (x1 - x2)))) + ((f . x2) / ((x2 - x0) * (x2 - x1))) by XCMPLX_1:189; :: thesis: verum