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 A20: 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 A21: 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 by A1, Lm2;
let s be Point of (Closed-Interval-TSpace 0 ,1); :: thesis: F1 . s = F2 . s
reconsider r = s as Real by Lm2;
thus F1 . s = ((1 - r) * r1) + (r * r2) by A20
.= F2 . s by A21 ; :: thesis: verum

end;

hence F1 = F2 by FUNCT_2:113; :: thesis: verum