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 A18: 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 A19: 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 8 :: thesis: F1 . s = F2 . s
reconsider r = s as Real ;
reconsider r1 = t1, r2 = t2 as Real ;
thus F1 . s = (((b - r) * r1) + ((r - a) * r2)) / (b - a) by A18
.= F2 . s by A19 ; :: thesis: verum