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 . x0) / ((x0 - x1) * (x0 - x2))) + ((f . x1) / ((x1 - x0) * (x1 - x2)))) + ((f . x2) / ((x2 - x0) * (x2 - x1)))
let f be Function of REAL,REAL; ( 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
; [!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; verum