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