let x0, x1, x2, x3 be Real; :: thesis: for f being Function of REAL ,REAL st x0,x1,x2,x3 are_mutually_different holds
( [!f,x0,x1,x2,x3!] = [!f,x1,x0,x2,x3!] & [!f,x0,x1,x2,x3!] = [!f,x1,x2,x0,x3!] )
let f be Function of REAL ,REAL ; :: thesis: ( x0,x1,x2,x3 are_mutually_different implies ( [!f,x0,x1,x2,x3!] = [!f,x1,x0,x2,x3!] & [!f,x0,x1,x2,x3!] = [!f,x1,x2,x0,x3!] ) )
assume x0,x1,x2,x3 are_mutually_different ; :: thesis: ( [!f,x0,x1,x2,x3!] = [!f,x1,x0,x2,x3!] & [!f,x0,x1,x2,x3!] = [!f,x1,x2,x0,x3!] )
then A1: ( x2 - x3 <> 0 & x1 - x3 <> 0 & x1 - x2 <> 0 & x3 - x0 <> 0 & x2 - x0 <> 0 & x1 - x0 <> 0 ) by ZFMISC_1:def 6;
set x10 = x1 - x0;
set x20 = x2 - x0;
set x30 = x3 - x0;
set x12 = x1 - x2;
set x13 = x1 - x3;
set x23 = x2 - x3;
A2: [!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:189
.= (((- ((((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:192
.= (((((((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 A1, XCMPLX_1:117
.= (((((((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 A1, XCMPLX_1:131
.= ((((((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:79
.= ((((((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:79
.= (- ((((((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:192
.= ((((((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:121
.= (((((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:79
.= (((((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:79
.= ((((((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 A1, XCMPLX_1:92
.= (((((((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 A1, XCMPLX_1:92
.= (((((((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 A1, XCMPLX_1:6, XCMPLX_1:92
.= (((((((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:121
.= ((((- ((((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)) ;
A3: [!f,x1,x0,x2,x3!] = ((((((f . x1) - (f . x0)) / (x1 - x0)) - (- (((f . x0) - (f . x2)) / (x2 - x0)))) / (x1 - x2)) - (((((f . x0) - (f . x2)) / (- (x2 - x0))) - (((f . x2) - (f . x3)) / (x2 - x3))) / (x0 - x3))) / (x1 - x3) by XCMPLX_1:189
.= ((((((f . x1) - (f . x0)) / (x1 - x0)) + (((f . x0) - (f . x2)) / (x2 - x0))) / (x1 - x2)) - (((- (((f . x0) - (f . x2)) / (x2 - x0))) - (((f . x2) - (f . x3)) / (x2 - x3))) / (- (x3 - x0)))) / (x1 - x3) by XCMPLX_1:189
.= ((((((f . x1) - (f . x0)) / (x1 - x0)) + (((f . x0) - (f . x2)) / (x2 - x0))) / (x1 - x2)) - ((- ((((f . x0) - (f . x2)) / (x2 - x0)) + (((f . x2) - (f . x3)) / (x2 - x3)))) / (- (x3 - x0)))) / (x1 - x3)
.= ((((((f . x1) - (f . x0)) / (x1 - x0)) + (((f . x0) - (f . x2)) / (x2 - x0))) / (x1 - x2)) - (((((f . x0) - (f . x2)) / (x2 - x0)) + (((f . x2) - (f . x3)) / (x2 - x3))) / (x3 - x0))) / (x1 - x3) by XCMPLX_1:192
.= (((((((f . x1) - (f . x0)) * (x2 - x0)) + (((f . x0) - (f . x2)) * (x1 - x0))) / ((x2 - x0) * (x1 - x0))) / (x1 - x2)) - (((((f . x0) - (f . x2)) / (x2 - x0)) + (((f . x2) - (f . x3)) / (x2 - x3))) / (x3 - x0))) / (x1 - x3) by A1, XCMPLX_1:117
.= (((((((f . x1) - (f . x0)) * (x2 - x0)) + (((f . x0) - (f . x2)) * (x1 - x0))) / ((x1 - x0) * (x2 - x0))) / (x1 - x2)) - ((((((f . x0) - (f . x2)) * (x2 - x3)) + (((f . x2) - (f . x3)) * (x2 - x0))) / ((x2 - x3) * (x2 - x0))) / (x3 - x0))) / (x1 - x3) by A1, XCMPLX_1:117
.= ((((((f . x1) - (f . x0)) * (x2 - x0)) + (((f . x0) - (f . x2)) * (x1 - x0))) / (((x1 - x0) * (x2 - x0)) * (x1 - x2))) - ((((((f . x0) - (f . x2)) * (x2 - x3)) + (((f . x2) - (f . x3)) * (x2 - x0))) / ((x2 - x3) * (x2 - x0))) / (x3 - x0))) / (x1 - x3) by XCMPLX_1:79
.= ((((((f . x1) - (f . x0)) * (x2 - x0)) + (((f . x0) - (f . x2)) * (x1 - x0))) / (((x1 - x0) * (x2 - x0)) * (x1 - x2))) - (((((f . x0) - (f . x2)) * (x2 - x3)) + (((f . x2) - (f . x3)) * (x2 - x0))) / (((x2 - x3) * (x2 - x0)) * (x3 - x0)))) / (x1 - x3) by XCMPLX_1:79
.= ((((((f . x1) - (f . x0)) * (x2 - x0)) + (((f . x0) - (f . x2)) * (x1 - x0))) / (((x1 - x0) * (x2 - x0)) * (x1 - x2))) / (x1 - x3)) - ((((((f . x0) - (f . x2)) * (x2 - x3)) + (((f . x2) - (f . x3)) * (x2 - x0))) / (((x2 - x3) * (x2 - x0)) * (x3 - x0))) / (x1 - x3)) by XCMPLX_1:121
.= (((((f . x1) - (f . x0)) * (x2 - x0)) + (((f . x0) - (f . x2)) * (x1 - x0))) / ((((x1 - x0) * (x2 - x0)) * (x1 - x2)) * (x1 - x3))) - ((((((f . x0) - (f . x2)) * (x2 - x3)) + (((f . x2) - (f . x3)) * (x2 - x0))) / (((x2 - x3) * (x2 - x0)) * (x3 - x0))) / (x1 - x3)) by XCMPLX_1:79
.= (((((f . x1) - (f . x0)) * (x2 - x0)) + (((f . x0) - (f . x2)) * (x1 - x0))) / ((((x1 - x0) * (x2 - x0)) * (x1 - x2)) * (x1 - x3))) - (((((f . x0) - (f . x2)) * (x2 - x3)) + (((f . x2) - (f . x3)) * (x2 - x0))) / ((((x2 - x3) * (x2 - x0)) * (x3 - x0)) * (x1 - x3))) by XCMPLX_1:79
.= ((((((f . x1) - (f . x0)) * (x2 - x0)) + (((f . x0) - (f . x2)) * (x1 - x0))) * (x2 - x3)) / (((((x1 - x0) * (x2 - x0)) * (x1 - x2)) * (x1 - x3)) * (x2 - x3))) - (((((f . x0) - (f . x2)) * (x2 - x3)) + (((f . x2) - (f . x3)) * (x2 - x0))) / ((((x2 - x3) * (x2 - x0)) * (x3 - x0)) * (x1 - x3))) by A1, XCMPLX_1:92
.= (((((((f . x1) - (f . x0)) * (x2 - x0)) * (x2 - x3)) + ((((f . x0) - (f . x2)) * (x1 - x0)) * (x2 - x3))) * (x3 - x0)) / ((((((x1 - x0) * (x2 - x0)) * (x1 - x2)) * (x1 - x3)) * (x2 - x3)) * (x3 - x0))) - (((((f . x0) - (f . x2)) * (x2 - x3)) + (((f . x2) - (f . x3)) * (x2 - x0))) / ((((x2 - x3) * (x2 - x0)) * (x3 - x0)) * (x1 - x3))) by A1, XCMPLX_1:92
.= (((((((f . x1) - (f . x0)) * (x2 - x0)) * (x2 - x3)) * (x3 - x0)) + (((((f . x0) - (f . x2)) * (x1 - x0)) * (x2 - x3)) * (x3 - x0))) / ((((((x1 - x0) * (x2 - x0)) * (x1 - x2)) * (x1 - x3)) * (x2 - x3)) * (x3 - x0))) - ((((((f . x0) - (f . x2)) * (x2 - x3)) + (((f . x2) - (f . x3)) * (x2 - x0))) * (x1 - x0)) / (((((x2 - x3) * (x2 - x0)) * (x3 - x0)) * (x1 - x3)) * (x1 - x0))) by A1, XCMPLX_1:92
.= (((((((f . x1) - (f . x0)) * (x2 - x0)) * (x2 - x3)) * (x3 - x0)) + (((((f . x0) - (f . x2)) * (x1 - x0)) * (x2 - x3)) * (x3 - x0))) / ((((((x1 - x0) * (x2 - x0)) * (x1 - x2)) * (x1 - x3)) * (x2 - x3)) * (x3 - x0))) - (((((((f . x0) - (f . x2)) * (x2 - x3)) * (x1 - x0)) + ((((f . x2) - (f . x3)) * (x2 - x0)) * (x1 - x0))) * (x1 - x2)) / ((((((x2 - x3) * (x2 - x0)) * (x3 - x0)) * (x1 - x3)) * (x1 - x0)) * (x1 - x2))) by A1, XCMPLX_1:92
.= (((((((f . x1) - (f . x0)) * (x2 - x0)) * (x2 - x3)) * (x3 - x0)) + (((((f . x0) - (f . x2)) * (x1 - x0)) * (x2 - x3)) * (x3 - x0))) - ((((((f . x0) - (f . x2)) * (x2 - x3)) * (x1 - x0)) * (x1 - x2)) + (((((f . x2) - (f . x3)) * (x2 - x0)) * (x1 - x0)) * (x1 - x2)))) / ((((((x2 - x3) * (x2 - x0)) * (x3 - x0)) * (x1 - x3)) * (x1 - x0)) * (x1 - x2)) by XCMPLX_1:121
.= [!f,x0,x1,x2,x3!] by A2 ;
[!f,x1,x2,x0,x3!] = ((((((f . x1) - (f . x2)) / (x1 - x2)) - (((f . x2) - (f . x0)) / (x2 - x0))) / (x1 - x0)) - (((((f . x2) - (f . x0)) / (x2 - x0)) - (((f . x0) - (f . x3)) / (- (x3 - x0)))) / (x2 - x3))) / (x1 - x3)
.= ((((((f . x1) - (f . x2)) / (x1 - x2)) - (((f . x2) - (f . x0)) / (x2 - x0))) / (x1 - x0)) - (((((f . x2) - (f . x0)) / (x2 - x0)) - (- (((f . x0) - (f . x3)) / (x3 - x0)))) / (x2 - x3))) / (x1 - x3) by XCMPLX_1:189
.= (((((((f . x1) - (f . x2)) * (x2 - x0)) - (((f . x2) - (f . x0)) * (x1 - x2))) / ((x1 - x2) * (x2 - x0))) / (x1 - x0)) - (((((f . x2) - (f . x0)) / (x2 - x0)) + (((f . x0) - (f . x3)) / (x3 - x0))) / (x2 - x3))) / (x1 - x3) by A1, XCMPLX_1:131
.= (((((((f . x1) - (f . x2)) * (x2 - x0)) - (((f . x2) - (f . x0)) * (x1 - x2))) / ((x1 - x2) * (x2 - x0))) / (x1 - x0)) - ((((((f . x2) - (f . x0)) * (x3 - x0)) + (((f . x0) - (f . x3)) * (x2 - x0))) / ((x3 - x0) * (x2 - x0))) / (x2 - x3))) / (x1 - x3) by A1, XCMPLX_1:117
.= ((((((f . x1) - (f . x2)) * (x2 - x0)) - (((f . x2) - (f . x0)) * (x1 - x2))) / (((x1 - x2) * (x2 - x0)) * (x1 - x0))) - ((((((f . x2) - (f . x0)) * (x3 - x0)) + (((f . x0) - (f . x3)) * (x2 - x0))) / ((x3 - x0) * (x2 - x0))) / (x2 - x3))) / (x1 - x3) by XCMPLX_1:79
.= ((((((f . x1) - (f . x2)) * (x2 - x0)) - (((f . x2) - (f . x0)) * (x1 - x2))) / (((x1 - x2) * (x2 - x0)) * (x1 - x0))) - (((((f . x2) - (f . x0)) * (x3 - x0)) + (((f . x0) - (f . x3)) * (x2 - x0))) / (((x3 - x0) * (x2 - x0)) * (x2 - x3)))) / (x1 - x3) by XCMPLX_1:79
.= ((((((f . x1) - (f . x2)) * (x2 - x0)) - (((f . x2) - (f . x0)) * (x1 - x2))) / (((x1 - x2) * (x2 - x0)) * (x1 - x0))) / (x1 - x3)) - ((((((f . x2) - (f . x0)) * (x3 - x0)) + (((f . x0) - (f . x3)) * (x2 - x0))) / (((x3 - x0) * (x2 - x0)) * (x2 - x3))) / (x1 - x3)) by XCMPLX_1:121
.= (((((f . x1) - (f . x2)) * (x2 - x0)) - (((f . x2) - (f . x0)) * (x1 - x2))) / ((((x1 - x2) * (x2 - x0)) * (x1 - x0)) * (x1 - x3))) - ((((((f . x2) - (f . x0)) * (x3 - x0)) + (((f . x0) - (f . x3)) * (x2 - x0))) / (((x3 - x0) * (x2 - x0)) * (x2 - x3))) / (x1 - x3)) by XCMPLX_1:79
.= (((((f . x1) - (f . x2)) * (x2 - x0)) - (((f . x2) - (f . x0)) * (x1 - x2))) / ((((x1 - x2) * (x2 - x0)) * (x1 - x0)) * (x1 - x3))) - (((((f . x2) - (f . x0)) * (x3 - x0)) + (((f . x0) - (f . x3)) * (x2 - x0))) / ((((x3 - x0) * (x2 - x0)) * (x2 - x3)) * (x1 - x3))) by XCMPLX_1:79
.= ((((((f . x1) - (f . x2)) * (x2 - x0)) - (((f . x2) - (f . x0)) * (x1 - x2))) * (x3 - x0)) / (((((x1 - x2) * (x2 - x0)) * (x1 - x0)) * (x1 - x3)) * (x3 - x0))) - (((((f . x2) - (f . x0)) * (x3 - x0)) + (((f . x0) - (f . x3)) * (x2 - x0))) / ((((x3 - x0) * (x2 - x0)) * (x2 - x3)) * (x1 - x3))) by A1, XCMPLX_1:92
.= (((((((f . x1) - (f . x2)) * (x2 - x0)) * (x3 - x0)) - ((((f . x2) - (f . x0)) * (x1 - x2)) * (x3 - x0))) * (x2 - x3)) / ((((((x1 - x2) * (x2 - x0)) * (x1 - x0)) * (x1 - x3)) * (x3 - x0)) * (x2 - x3))) - (((((f . x2) - (f . x0)) * (x3 - x0)) + (((f . x0) - (f . x3)) * (x2 - x0))) / ((((x3 - x0) * (x2 - x0)) * (x2 - x3)) * (x1 - x3))) by A1, XCMPLX_1:92
.= (((((((f . x1) - (f . x2)) * (x2 - x0)) * (x3 - x0)) * (x2 - x3)) - (((((f . x2) - (f . x0)) * (x1 - x2)) * (x3 - x0)) * (x2 - x3))) / ((((((x1 - x2) * (x2 - x0)) * (x1 - x0)) * (x1 - x3)) * (x3 - x0)) * (x2 - x3))) - ((((((f . x2) - (f . x0)) * (x3 - x0)) + (((f . x0) - (f . x3)) * (x2 - x0))) * (x1 - x2)) / (((((x3 - x0) * (x2 - x0)) * (x2 - x3)) * (x1 - x3)) * (x1 - x2))) by A1, XCMPLX_1:92
.= (((((((f . x1) - (f . x2)) * (x2 - x0)) * (x3 - x0)) * (x2 - x3)) - (((((f . x2) - (f . x0)) * (x1 - x2)) * (x3 - x0)) * (x2 - x3))) / ((((((x1 - x2) * (x2 - x0)) * (x1 - x0)) * (x1 - x3)) * (x3 - x0)) * (x2 - x3))) - (((((((f . x2) - (f . x0)) * (x3 - x0)) * (x1 - x2)) + ((((f . x0) - (f . x3)) * (x2 - x0)) * (x1 - x2))) * (x1 - x0)) / ((((((x3 - x0) * (x2 - x0)) * (x2 - x3)) * (x1 - x3)) * (x1 - x2)) * (x1 - x0))) by A1, XCMPLX_1:92
.= (((((((f . x1) - (f . x2)) * (x2 - x0)) * (x3 - x0)) * (x2 - x3)) - (((((f . x2) - (f . x0)) * (x1 - x2)) * (x3 - x0)) * (x2 - x3))) - ((((((f . x2) - (f . x0)) * (x3 - x0)) * (x1 - x2)) * (x1 - x0)) + (((((f . x0) - (f . x3)) * (x2 - x0)) * (x1 - x2)) * (x1 - x0)))) / ((((((x3 - x0) * (x2 - x0)) * (x2 - x3)) * (x1 - x3)) * (x1 - x2)) * (x1 - x0)) by XCMPLX_1:121
.= [!f,x0,x1,x2,x3!] by A2 ;
hence ( [!f,x0,x1,x2,x3!] = [!f,x1,x0,x2,x3!] & [!f,x0,x1,x2,x3!] = [!f,x1,x2,x0,x3!] ) by A3; :: thesis: verum