let F1, F2 be Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (a,b)); :: thesis: ( ( for s being Point of (Closed-Interval-TSpace (0,1)) holds F1 . s = ((1 - s) * t1) + (s * t2) ) & ( for s being Point of (Closed-Interval-TSpace (0,1)) holds F2 . s = ((1 - s) * t1) + (s * t2) ) implies F1 = F2 )
assume A18: for s being Point of (Closed-Interval-TSpace (0,1)) holds F1 . s = ((1 - s) * t1) + (s * t2) ; :: thesis: ( ex s being Point of (Closed-Interval-TSpace (0,1)) st not F2 . s = ((1 - s) * t1) + (s * t2) or F1 = F2 )
assume A19: for s being Point of (Closed-Interval-TSpace (0,1)) holds F2 . s = ((1 - s) * t1) + (s * t2) ; :: thesis: F1 = F2
for s being Point of (Closed-Interval-TSpace (0,1)) holds F1 . s = F2 . s

proof

reconsider r1 = t1, r2 = t2 as Real ;
let s be Point of (Closed-Interval-TSpace (0,1)); :: thesis: F1 . s = F2 . s
reconsider r = s as Real ;
thus F1 . s = ((1 - r) * r1) + (r * r2) by A18
.= F2 . s by A19 ; :: thesis: verum

end;

hence F1 = F2 ; :: thesis: verum