let x0, x1, x2, x3 be Real; 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; ( ( 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
; [!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
; verum