let x0, x1, x2, k be Real; :: thesis: for f being Function of REAL,REAL st ( for x being Real holds f . x = k / x ) & x0 <> 0 & x1 <> 0 & x2 <> 0 & x0,x1,x2 are_mutually_distinct holds
[!f,x0,x1,x2!] = k / ((x0 * x1) * x2)
let f be Function of REAL,REAL; :: thesis: ( ( for x being Real holds f . x = k / x ) & x0 <> 0 & x1 <> 0 & x2 <> 0 & x0,x1,x2 are_mutually_distinct implies [!f,x0,x1,x2!] = k / ((x0 * x1) * x2) )
assume that
A1: for x being Real holds f . x = k / x and
A2: x0 <> 0 and
A3: x1 <> 0 and
A4: x2 <> 0 ; :: thesis: ( not x0,x1,x2 are_mutually_distinct or [!f,x0,x1,x2!] = k / ((x0 * x1) * x2) )
assume A5: x0,x1,x2 are_mutually_distinct ; :: thesis: [!f,x0,x1,x2!] = k / ((x0 * x1) * x2)
then A6: x1 <> x2 by ZFMISC_1:def 5;
A7: x0 - x2 <> 0 by A5, ZFMISC_1:def 5;
x0 <> x1 by A5, ZFMISC_1:def 5;
then [!f,x0,x1,x2!] = ((- (k / (x0 * x1))) - [!f,x1,x2!]) / (x0 - x2) by A1, A2, A3, Th34
.= ((- (k / (x0 * x1))) - (- (k / (x1 * x2)))) / (x0 - x2) by A1, A3, A4, A6, Th34
.= ((- (k / (x0 * x1))) + (k / (x1 * x2))) / (x0 - x2)
.= ((- ((k * x2) / ((x0 * x1) * x2))) + (k / (x1 * x2))) / (x0 - x2) by A4, XCMPLX_1:91
.= ((- ((k * x2) / ((x0 * x1) * x2))) + ((k * x0) / (x0 * (x1 * x2)))) / (x0 - x2) by A2, XCMPLX_1:91
.= (- (((k * x2) / ((x0 * x1) * x2)) - ((k * x0) / ((x0 * x1) * x2)))) / (x0 - x2)
.= (- (((k * x2) - (k * x0)) / ((x0 * x1) * x2))) / (x0 - x2) by XCMPLX_1:120
.= ((- (k * (x2 - x0))) / ((x0 * x1) * x2)) / (x0 - x2) by XCMPLX_1:187
.= (k * (x0 - x2)) / (((x0 * x1) * x2) * (x0 - x2)) by XCMPLX_1:78 ;
hence [!f,x0,x1,x2!] = k / ((x0 * x1) * x2) by A7, XCMPLX_1:91; :: thesis: verum