let F1, F2 be Function of (Closed-Interval-TSpace a,b),(Closed-Interval-TSpace 0 ,1); :: thesis: ( ( for s being Point of (Closed-Interval-TSpace a,b) holds F1 . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) ) & ( for s being Point of (Closed-Interval-TSpace a,b) holds F2 . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) ) implies F1 = F2 )
assume A20: for s being Point of (Closed-Interval-TSpace a,b) holds F1 . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) ; :: thesis: ( ex s being Point of (Closed-Interval-TSpace a,b) st not F2 . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) or F1 = F2 )
assume A21: for s being Point of (Closed-Interval-TSpace a,b) holds F2 . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) ; :: thesis: F1 = F2
let s be Point of (Closed-Interval-TSpace a,b); :: according to FUNCT_2:def 9 :: thesis: F1 . s = F2 . s
reconsider r = s as Real by A1, Lm2;
reconsider r1 = t1, r2 = t2 as Real by Lm2;
thus F1 . s = (((b - r) * r1) + ((r - a) * r2)) / (b - a) by A20
.= F2 . s by A21 ; :: thesis: verum