let x0, x1, x2, x3 be Real; for f being Function of REAL,REAL st x0,x1,x2,x3 are_mutually_distinct holds
( [!f,x0,x1,x2,x3!] = [!f,x1,x2,x3,x0!] & [!f,x0,x1,x2,x3!] = [!f,x3,x2,x1,x0!] )
let f be Function of REAL,REAL; ( x0,x1,x2,x3 are_mutually_distinct implies ( [!f,x0,x1,x2,x3!] = [!f,x1,x2,x3,x0!] & [!f,x0,x1,x2,x3!] = [!f,x3,x2,x1,x0!] ) )
set x10 = x1 - x0;
set x20 = x2 - x0;
set x30 = x3 - x0;
set x12 = x1 - x2;
set x13 = x1 - x3;
set x23 = x2 - x3;
assume A1:
x0,x1,x2,x3 are_mutually_distinct
; ( [!f,x0,x1,x2,x3!] = [!f,x1,x2,x3,x0!] & [!f,x0,x1,x2,x3!] = [!f,x3,x2,x1,x0!] )
then A2:
x2 - x3 <> 0
by ZFMISC_1:def 6;
A3:
x3 - x0 <> 0
by A1, ZFMISC_1:def 6;
A4:
x1 - x3 <> 0
by A1, ZFMISC_1:def 6;
A5:
x1 - x0 <> 0
by A1, ZFMISC_1:def 6;
A6:
x2 - x0 <> 0
by A1, ZFMISC_1:def 6;
A7:
x1 - x2 <> 0
by A1, ZFMISC_1:def 6;
A8: [!f,x0,x1,x2,x3!] =
((((((f . x0) - (f . x1)) / (- (x1 - x0))) - (((f . x1) - (f . x2)) / (x1 - x2))) / (- (x2 - x0))) - (((((f . x1) - (f . x2)) / (x1 - x2)) - (((f . x2) - (f . x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3)
.=
((((- (((f . x0) - (f . x1)) / (x1 - x0))) - (((f . x1) - (f . x2)) / (x1 - x2))) / (- (x2 - x0))) - (((((f . x1) - (f . x2)) / (x1 - x2)) - (((f . x2) - (f . x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3)
by XCMPLX_1:188
.=
(((- ((((f . x0) - (f . x1)) / (x1 - x0)) + (((f . x1) - (f . x2)) / (x1 - x2)))) / (- (x2 - x0))) - (((((f . x1) - (f . x2)) / (x1 - x2)) - (((f . x2) - (f . x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3)
.=
((((((f . x0) - (f . x1)) / (x1 - x0)) + (((f . x1) - (f . x2)) / (x1 - x2))) / (x2 - x0)) - (((((f . x1) - (f . x2)) / (x1 - x2)) - (((f . x2) - (f . x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3)
by XCMPLX_1:191
.=
(((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / ((x1 - x0) * (x1 - x2))) / (x2 - x0)) - (((((f . x1) - (f . x2)) / (x1 - x2)) - (((f . x2) - (f . x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3)
by A7, A5, XCMPLX_1:116
.=
(((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / ((x1 - x0) * (x1 - x2))) / (x2 - x0)) - ((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / ((x1 - x2) * (x2 - x3))) / (x1 - x3))) / (x0 - x3)
by A2, A7, XCMPLX_1:130
.=
((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / (((x1 - x0) * (x1 - x2)) * (x2 - x0))) - ((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / ((x1 - x2) * (x2 - x3))) / (x1 - x3))) / (x0 - x3)
by XCMPLX_1:78
.=
((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / (((x1 - x0) * (x1 - x2)) * (x2 - x0))) - (((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / (((x1 - x2) * (x2 - x3)) * (x1 - x3)))) / (x0 - x3)
by XCMPLX_1:78
.=
(- ((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / (((x1 - x0) * (x1 - x2)) * (x2 - x0))) - (((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / (((x1 - x2) * (x2 - x3)) * (x1 - x3))))) / (- (x0 - x3))
by XCMPLX_1:191
.=
((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / (((x1 - x2) * (x2 - x3)) * (x1 - x3))) - (((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / (((x1 - x0) * (x1 - x2)) * (x2 - x0)))) / (x3 - x0)
.=
((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / (((x1 - x2) * (x2 - x3)) * (x1 - x3))) / (x3 - x0)) - ((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / (((x1 - x0) * (x1 - x2)) * (x2 - x0))) / (x3 - x0))
by XCMPLX_1:120
.=
(((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / ((((x1 - x2) * (x2 - x3)) * (x1 - x3)) * (x3 - x0))) - ((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / (((x1 - x0) * (x1 - x2)) * (x2 - x0))) / (x3 - x0))
by XCMPLX_1:78
.=
(((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / ((((x1 - x2) * (x2 - x3)) * (x1 - x3)) * (x3 - x0))) - (((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / ((((x1 - x0) * (x1 - x2)) * (x2 - x0)) * (x3 - x0)))
by XCMPLX_1:78
.=
((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) * (x2 - x0)) / (((((x1 - x2) * (x2 - x3)) * (x1 - x3)) * (x3 - x0)) * (x2 - x0))) - (((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / ((((x1 - x0) * (x1 - x2)) * (x2 - x0)) * (x3 - x0)))
by A6, XCMPLX_1:91
.=
(((((((f . x1) - (f . x2)) * (x2 - x3)) * (x2 - x0)) - ((((f . x2) - (f . x3)) * (x1 - x2)) * (x2 - x0))) * (x1 - x0)) / ((((((x1 - x2) * (x2 - x0)) * (x3 - x0)) * (x2 - x3)) * (x1 - x3)) * (x1 - x0))) - (((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / ((((x1 - x0) * (x1 - x2)) * (x2 - x0)) * (x3 - x0)))
by A5, XCMPLX_1:91
.=
(((((((f . x1) - (f . x2)) * (x2 - x3)) * (x2 - x0)) * (x1 - x0)) - (((((f . x2) - (f . x3)) * (x1 - x2)) * (x2 - x0)) * (x1 - x0))) / ((((((x1 - x2) * (x2 - x0)) * (x3 - x0)) * (x2 - x3)) * (x1 - x3)) * (x1 - x0))) - ((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) * ((x2 - x3) * (x1 - x3))) / (((((x1 - x2) * (x2 - x0)) * (x3 - x0)) * (x1 - x0)) * ((x2 - x3) * (x1 - x3))))
by A2, A4, XCMPLX_1:6, XCMPLX_1:91
.=
(((((((f . x1) - (f . x2)) * (x2 - x3)) * (x2 - x0)) * (x1 - x0)) - (((((f . x2) - (f . x3)) * (x1 - x2)) * (x2 - x0)) * (x1 - x0))) - ((((((f . x0) - (f . x1)) * (x1 - x2)) * (x2 - x3)) * (x1 - x3)) + (((((f . x1) - (f . x2)) * (x1 - x0)) * (x2 - x3)) * (x1 - x3)))) / ((((((x1 - x2) * (x2 - x0)) * (x3 - x0)) * (x2 - x3)) * (x1 - x3)) * (x1 - x0))
by XCMPLX_1:120
.=
((((- ((((f . x0) * (x1 - x2)) * (x2 - x3)) * (x1 - x3))) + ((((f . x1) * (x2 - x0)) * (x2 - x3)) * (x3 - x0))) - ((((f . x2) * (x1 - x3)) * (x1 - x0)) * (x3 - x0))) + ((((f . x3) * (x1 - x2)) * (x2 - x0)) * (x1 - x0))) / ((((((x1 - x2) * (x2 - x0)) * (x3 - x0)) * (x2 - x3)) * (x1 - x3)) * (x1 - x0))
;
A9: [!f,x3,x2,x1,x0!] =
((((((f . x3) - (f . x2)) / (- (x2 - x3))) - (((f . x2) - (f . x1)) / (- (x1 - x2)))) / (- (x1 - x3))) - (((((f . x2) - (f . x1)) / (- (x1 - x2))) - (((f . x1) - (f . x0)) / (x1 - x0))) / (x2 - x0))) / (x3 - x0)
.=
((((- (((f . x3) - (f . x2)) / (x2 - x3))) - (((f . x2) - (f . x1)) / (- (x1 - x2)))) / (- (x1 - x3))) - (((((f . x2) - (f . x1)) / (- (x1 - x2))) - (((f . x1) - (f . x0)) / (x1 - x0))) / (x2 - x0))) / (x3 - x0)
by XCMPLX_1:188
.=
((((- (((f . x3) - (f . x2)) / (x2 - x3))) - (- (((f . x2) - (f . x1)) / (x1 - x2)))) / (- (x1 - x3))) - (((((f . x2) - (f . x1)) / (- (x1 - x2))) - (((f . x1) - (f . x0)) / (x1 - x0))) / (x2 - x0))) / (x3 - x0)
by XCMPLX_1:188
.=
(((- ((((f . x3) - (f . x2)) / (x2 - x3)) - (((f . x2) - (f . x1)) / (x1 - x2)))) / (- (x1 - x3))) - (((((f . x2) - (f . x1)) / (- (x1 - x2))) - (((f . x1) - (f . x0)) / (x1 - x0))) / (x2 - x0))) / (x3 - x0)
.=
((((((f . x3) - (f . x2)) / (x2 - x3)) - (((f . x2) - (f . x1)) / (x1 - x2))) / (x1 - x3)) - (((((f . x2) - (f . x1)) / (- (x1 - x2))) - (((f . x1) - (f . x0)) / (x1 - x0))) / (x2 - x0))) / (x3 - x0)
by XCMPLX_1:191
.=
((((((f . x3) - (f . x2)) / (x2 - x3)) - (((f . x2) - (f . x1)) / (x1 - x2))) / (x1 - x3)) - (((- (((f . x2) - (f . x1)) / (x1 - x2))) - (((f . x1) - (f . x0)) / (x1 - x0))) / (x2 - x0))) / (x3 - x0)
by XCMPLX_1:188
.=
((((((f . x3) - (f . x2)) / (x2 - x3)) - (((f . x2) - (f . x1)) / (x1 - x2))) / (x1 - x3)) + (- ((- ((((f . x1) - (f . x0)) / (x1 - x0)) + (((f . x2) - (f . x1)) / (x1 - x2)))) / (x2 - x0)))) / (x3 - x0)
.=
((((((f . x3) - (f . x2)) / (x2 - x3)) - (((f . x2) - (f . x1)) / (x1 - x2))) / (x1 - x3)) + (((((f . x1) - (f . x0)) / (x1 - x0)) + (((f . x2) - (f . x1)) / (x1 - x2))) / (x2 - x0))) / (x3 - x0)
by XCMPLX_1:190
.=
(((((((f . x3) - (f . x2)) * (x1 - x2)) - (((f . x2) - (f . x1)) * (x2 - x3))) / ((x2 - x3) * (x1 - x2))) / (x1 - x3)) + (((((f . x1) - (f . x0)) / (x1 - x0)) + (((f . x2) - (f . x1)) / (x1 - x2))) / (x2 - x0))) / (x3 - x0)
by A2, A7, XCMPLX_1:130
.=
(((((((f . x3) - (f . x2)) * (x1 - x2)) - (((f . x2) - (f . x1)) * (x2 - x3))) / ((x2 - x3) * (x1 - x2))) / (x1 - x3)) + ((((((f . x1) - (f . x0)) * (x1 - x2)) + (((f . x2) - (f . x1)) * (x1 - x0))) / ((x1 - x0) * (x1 - x2))) / (x2 - x0))) / (x3 - x0)
by A7, A5, XCMPLX_1:116
.=
((((((f . x3) - (f . x2)) * (x1 - x2)) - (((f . x2) - (f . x1)) * (x2 - x3))) / (((x2 - x3) * (x1 - x2)) * (x1 - x3))) + ((((((f . x1) - (f . x0)) * (x1 - x2)) + (((f . x2) - (f . x1)) * (x1 - x0))) / ((x1 - x0) * (x1 - x2))) / (x2 - x0))) / (x3 - x0)
by XCMPLX_1:78
.=
((((((f . x3) - (f . x2)) * (x1 - x2)) - (((f . x2) - (f . x1)) * (x2 - x3))) / (((x2 - x3) * (x1 - x2)) * (x1 - x3))) + (((((f . x1) - (f . x0)) * (x1 - x2)) + (((f . x2) - (f . x1)) * (x1 - x0))) / (((x1 - x0) * (x1 - x2)) * (x2 - x0)))) / (x3 - x0)
by XCMPLX_1:78
.=
((((((f . x3) - (f . x2)) * (x1 - x2)) - (((f . x2) - (f . x1)) * (x2 - x3))) / (((x2 - x3) * (x1 - x2)) * (x1 - x3))) + ((((((f . x1) - (f . x0)) * (x1 - x2)) + (((f . x2) - (f . x1)) * (x1 - x0))) * (x1 - x3)) / ((((x1 - x0) * (x1 - x2)) * (x2 - x0)) * (x1 - x3)))) / (x3 - x0)
by A4, XCMPLX_1:91
.=
((((((f . x3) - (f . x2)) * (x1 - x2)) - (((f . x2) - (f . x1)) * (x2 - x3))) / (((x2 - x3) * (x1 - x2)) * (x1 - x3))) + (((((((f . x1) - (f . x0)) * (x1 - x2)) * (x1 - x3)) + ((((f . x2) - (f . x1)) * (x1 - x0)) * (x1 - x3))) * (x2 - x3)) / (((((x1 - x0) * (x1 - x2)) * (x1 - x3)) * (x2 - x0)) * (x2 - x3)))) / (x3 - x0)
by A2, XCMPLX_1:91
.=
(((((((f . x3) - (f . x2)) * (x1 - x2)) - (((f . x2) - (f . x1)) * (x2 - x3))) * (x2 - x0)) / ((((x2 - x3) * (x1 - x2)) * (x1 - x3)) * (x2 - x0))) + (((((((f . x1) - (f . x0)) * (x1 - x2)) * (x1 - x3)) * (x2 - x3)) + (((((f . x2) - (f . x1)) * (x1 - x0)) * (x1 - x3)) * (x2 - x3))) / (((((x1 - x0) * (x1 - x2)) * (x1 - x3)) * (x2 - x0)) * (x2 - x3)))) / (x3 - x0)
by A6, XCMPLX_1:91
.=
((((((((f . x3) - (f . x2)) * (x1 - x2)) * (x2 - x0)) - ((((f . x2) - (f . x1)) * (x2 - x3)) * (x2 - x0))) * (x1 - x0)) / (((((x1 - x2) * (x1 - x3)) * (x2 - x0)) * (x2 - x3)) * (x1 - x0))) + (((((((f . x1) - (f . x0)) * (x1 - x2)) * (x1 - x3)) * (x2 - x3)) + (((((f . x2) - (f . x1)) * (x1 - x0)) * (x1 - x3)) * (x2 - x3))) / (((((x1 - x0) * (x1 - x2)) * (x1 - x3)) * (x2 - x0)) * (x2 - x3)))) / (x3 - x0)
by A5, XCMPLX_1:91
.=
((((((((f . x3) - (f . x2)) * (x1 - x2)) * (x2 - x0)) * (x1 - x0)) - (((((f . x2) - (f . x1)) * (x2 - x3)) * (x2 - x0)) * (x1 - x0))) / (((((x1 - x0) * (x1 - x2)) * (x1 - x3)) * (x2 - x0)) * (x2 - x3))) / (x3 - x0)) + ((((((((f . x1) - (f . x0)) * (x1 - x2)) * (x1 - x3)) * (x2 - x3)) + (((((f . x2) - (f . x1)) * (x1 - x0)) * (x1 - x3)) * (x2 - x3))) / (((((x1 - x0) * (x1 - x2)) * (x1 - x3)) * (x2 - x0)) * (x2 - x3))) / (x3 - x0))
by XCMPLX_1:62
.=
(((((((f . x3) - (f . x2)) * (x1 - x2)) * (x2 - x0)) * (x1 - x0)) - (((((f . x2) - (f . x1)) * (x2 - x3)) * (x2 - x0)) * (x1 - x0))) / ((((((x1 - x0) * (x1 - x2)) * (x1 - x3)) * (x2 - x0)) * (x2 - x3)) * (x3 - x0))) + ((((((((f . x1) - (f . x0)) * (x1 - x2)) * (x1 - x3)) * (x2 - x3)) + (((((f . x2) - (f . x1)) * (x1 - x0)) * (x1 - x3)) * (x2 - x3))) / (((((x1 - x0) * (x1 - x2)) * (x1 - x3)) * (x2 - x0)) * (x2 - x3))) / (x3 - x0))
by XCMPLX_1:78
.=
(((((((f . x3) - (f . x2)) * (x1 - x2)) * (x2 - x0)) * (x1 - x0)) - (((((f . x2) - (f . x1)) * (x2 - x3)) * (x2 - x0)) * (x1 - x0))) / ((((((x1 - x0) * (x1 - x2)) * (x1 - x3)) * (x2 - x0)) * (x2 - x3)) * (x3 - x0))) + (((((((f . x1) - (f . x0)) * (x1 - x2)) * (x1 - x3)) * (x2 - x3)) + (((((f . x2) - (f . x1)) * (x1 - x0)) * (x1 - x3)) * (x2 - x3))) / ((((((x1 - x0) * (x1 - x2)) * (x1 - x3)) * (x2 - x0)) * (x2 - x3)) * (x3 - x0)))
by XCMPLX_1:78
.=
(((((((f . x3) - (f . x2)) * (x1 - x2)) * (x2 - x0)) * (x1 - x0)) - (((((f . x2) - (f . x1)) * (x2 - x3)) * (x2 - x0)) * (x1 - x0))) + ((((((f . x1) - (f . x0)) * (x1 - x2)) * (x1 - x3)) * (x2 - x3)) + (((((f . x2) - (f . x1)) * (x1 - x0)) * (x1 - x3)) * (x2 - x3)))) / ((((((x1 - x0) * (x1 - x2)) * (x1 - x3)) * (x2 - x0)) * (x2 - x3)) * (x3 - x0))
by XCMPLX_1:62
.=
[!f,x0,x1,x2,x3!]
by A8
;
[!f,x1,x2,x3,x0!] =
(((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / ((x1 - x2) * (x2 - x3))) / (x1 - x3)) - (((((f . x2) - (f . x3)) / (x2 - x3)) - (((f . x3) - (f . x0)) / (x3 - x0))) / (x2 - x0))) / (x1 - x0)
by A2, A7, XCMPLX_1:130
.=
(((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / ((x1 - x2) * (x2 - x3))) / (x1 - x3)) - ((((((f . x2) - (f . x3)) * (x3 - x0)) - (((f . x3) - (f . x0)) * (x2 - x3))) / ((x2 - x3) * (x3 - x0))) / (x2 - x0))) / (x1 - x0)
by A2, A3, XCMPLX_1:130
.=
((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / (((x1 - x2) * (x2 - x3)) * (x1 - x3))) - ((((((f . x2) - (f . x3)) * (x3 - x0)) - (((f . x3) - (f . x0)) * (x2 - x3))) / ((x2 - x3) * (x3 - x0))) / (x2 - x0))) / (x1 - x0)
by XCMPLX_1:78
.=
((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / (((x1 - x2) * (x2 - x3)) * (x1 - x3))) - (((((f . x2) - (f . x3)) * (x3 - x0)) - (((f . x3) - (f . x0)) * (x2 - x3))) / (((x2 - x3) * (x3 - x0)) * (x2 - x0)))) / (x1 - x0)
by XCMPLX_1:78
.=
((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / (((x1 - x2) * (x2 - x3)) * (x1 - x3))) / (x1 - x0)) - ((((((f . x2) - (f . x3)) * (x3 - x0)) - (((f . x3) - (f . x0)) * (x2 - x3))) / (((x2 - x3) * (x3 - x0)) * (x2 - x0))) / (x1 - x0))
by XCMPLX_1:120
.=
(((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / ((((x1 - x2) * (x2 - x3)) * (x1 - x3)) * (x1 - x0))) - ((((((f . x2) - (f . x3)) * (x3 - x0)) - (((f . x3) - (f . x0)) * (x2 - x3))) / (((x2 - x3) * (x3 - x0)) * (x2 - x0))) / (x1 - x0))
by XCMPLX_1:78
.=
(((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / ((((x1 - x2) * (x2 - x3)) * (x1 - x3)) * (x1 - x0))) - (((((f . x2) - (f . x3)) * (x3 - x0)) - (((f . x3) - (f . x0)) * (x2 - x3))) / ((((x2 - x3) * (x3 - x0)) * (x2 - x0)) * (x1 - x0)))
by XCMPLX_1:78
.=
((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) * (x3 - x0)) / (((((x1 - x2) * (x2 - x3)) * (x1 - x3)) * (x1 - x0)) * (x3 - x0))) - (((((f . x2) - (f . x3)) * (x3 - x0)) - (((f . x3) - (f . x0)) * (x2 - x3))) / ((((x2 - x3) * (x3 - x0)) * (x2 - x0)) * (x1 - x0)))
by A3, XCMPLX_1:91
.=
(((((((f . x1) - (f . x2)) * (x2 - x3)) * (x3 - x0)) - ((((f . x2) - (f . x3)) * (x1 - x2)) * (x3 - x0))) * (x2 - x0)) / ((((((x1 - x2) * (x2 - x3)) * (x1 - x3)) * (x1 - x0)) * (x3 - x0)) * (x2 - x0))) - (((((f . x2) - (f . x3)) * (x3 - x0)) - (((f . x3) - (f . x0)) * (x2 - x3))) / ((((x2 - x3) * (x3 - x0)) * (x2 - x0)) * (x1 - x0)))
by A6, XCMPLX_1:91
.=
(((((((f . x1) - (f . x2)) * (x2 - x3)) * (x3 - x0)) * (x2 - x0)) - (((((f . x2) - (f . x3)) * (x1 - x2)) * (x3 - x0)) * (x2 - x0))) / ((((((x1 - x2) * (x2 - x3)) * (x1 - x3)) * (x1 - x0)) * (x3 - x0)) * (x2 - x0))) - ((((((f . x2) - (f . x3)) * (x3 - x0)) - (((f . x3) - (f . x0)) * (x2 - x3))) * (x1 - x3)) / (((((x1 - x0) * (x3 - x0)) * (x2 - x0)) * (x2 - x3)) * (x1 - x3)))
by A4, XCMPLX_1:91
.=
(((((((f . x1) - (f . x2)) * (x2 - x3)) * (x3 - x0)) * (x2 - x0)) - (((((f . x2) - (f . x3)) * (x1 - x2)) * (x3 - x0)) * (x2 - x0))) / ((((((x1 - x2) * (x2 - x3)) * (x1 - x3)) * (x1 - x0)) * (x3 - x0)) * (x2 - x0))) - (((((((f . x2) - (f . x3)) * (x3 - x0)) * (x1 - x3)) - ((((f . x3) - (f . x0)) * (x2 - x3)) * (x1 - x3))) * (x1 - x2)) / ((((((x2 - x3) * (x1 - x3)) * (x1 - x0)) * (x3 - x0)) * (x2 - x0)) * (x1 - x2)))
by A7, XCMPLX_1:91
.=
(((((((f . x1) - (f . x2)) * (x2 - x3)) * (x3 - x0)) * (x2 - x0)) - (((((f . x2) - (f . x3)) * (x1 - x2)) * (x3 - x0)) * (x2 - x0))) - ((((((f . x2) - (f . x3)) * (x3 - x0)) * (x1 - x3)) * (x1 - x2)) - (((((f . x3) - (f . x0)) * (x2 - x3)) * (x1 - x3)) * (x1 - x2)))) / ((((((x1 - x2) * (x2 - x3)) * (x1 - x3)) * (x1 - x0)) * (x3 - x0)) * (x2 - x0))
by XCMPLX_1:120
.=
[!f,x0,x1,x2,x3!]
by A8
;
hence
( [!f,x0,x1,x2,x3!] = [!f,x1,x2,x3,x0!] & [!f,x0,x1,x2,x3!] = [!f,x3,x2,x1,x0!] )
by A9; verum