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