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