let x0, x1, x2, x3 be Real; :: thesis: for f being Function of REAL,REAL st ( for x being Real holds f . x = x ^2 ) & x0,x1,x2,x3 are_mutually_distinct holds
[!f,x0,x1,x2,x3!] = 0
let f be Function of REAL,REAL; :: thesis: ( ( for x being Real holds f . x = x ^2 ) & x0,x1,x2,x3 are_mutually_distinct implies [!f,x0,x1,x2,x3!] = 0 )
assume that
A1: for x being Real holds f . x = x ^2 and
A2: x0,x1,x2,x3 are_mutually_distinct ; :: thesis: [!f,x0,x1,x2,x3!] = 0
A3: ( f . x0 = x0 ^2 & f . x1 = x1 ^2 & f . x2 = x2 ^2 & f . x3 = x3 ^2 ) by A1;
A4: ( x0 - x1 <> 0 & x1 - x2 <> 0 & x2 - x3 <> 0 & x0 - x2 <> 0 & x1 - x3 <> 0 & x0 - x3 <> 0 ) by A2, ZFMISC_1:def 6;
[!f,x0,x1,x2,x3!] = ((((((x0 - x1) * (x0 + x1)) / (x0 - x1)) - (((x1 - x2) * (x1 + x2)) / (x1 - x2))) / (x0 - x2)) - (((((x1 - x2) * (x1 + x2)) / (x1 - x2)) - (((x2 - x3) * (x2 + x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3) by A3
.= ((((x0 + x1) - (((x1 - x2) * (x1 + x2)) / (x1 - x2))) / (x0 - x2)) - (((((x1 - x2) * (x1 + x2)) / (x1 - x2)) - (((x2 - x3) * (x2 + x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3) by A4, XCMPLX_1:89
.= ((((x0 + x1) - (x1 + x2)) / (x0 - x2)) - (((((x1 - x2) * (x1 + x2)) / (x1 - x2)) - (((x2 - x3) * (x2 + x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3) by A4, XCMPLX_1:89
.= ((((x0 + x1) - (x1 + x2)) / (x0 - x2)) - (((x1 + x2) - (((x2 - x3) * (x2 + x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3) by A4, XCMPLX_1:89
.= ((((x0 + x1) - (x1 + x2)) / (x0 - x2)) - (((x1 + x2) - (x2 + x3)) / (x1 - x3))) / (x0 - x3) by A4, XCMPLX_1:89
.= (1 - ((x1 - x3) / (x1 - x3))) / (x0 - x3) by A4, XCMPLX_1:60
.= (1 - 1) / (x0 - x3) by A4, XCMPLX_1:60
.= 0 ;
hence [!f,x0,x1,x2,x3!] = 0 ; :: thesis: verum