let x0, x1 be Real; :: thesis: for f1, f2 being Function of REAL,REAL holds [!(f1 + f2),x0,x1!] = [!f1,x0,x1!] + [!f2,x0,x1!]
let f1, f2 be Function of REAL,REAL; :: thesis: [!(f1 + f2),x0,x1!] = [!f1,x0,x1!] + [!f2,x0,x1!]
reconsider xx0 = x0, xx1 = x1 as Element of REAL by XREAL_0:def 1;
[!(f1 + f2),x0,x1!] = (((f1 . xx0) + (f2 . xx0)) - ((f1 + f2) . xx1)) / (xx0 - xx1) by VALUED_1:1
.= (((f1 . x0) + (f2 . x0)) - ((f1 . x1) + (f2 . x1))) / (x0 - x1) by VALUED_1:1
.= (((f1 . x0) - (f1 . x1)) + ((f2 . x0) - (f2 . x1))) / (x0 - x1)
.= [!f1,x0,x1!] + [!f2,x0,x1!] by XCMPLX_1:62 ;
hence [!(f1 + f2),x0,x1!] = [!f1,x0,x1!] + [!f2,x0,x1!] ; :: thesis: verum