theorem :: DIFF_2:17

for x0, x1, x2 being 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)))