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)
for r, r1, r2 being real number st s = r & r1 = t1 & r2 = t2 holds
F1 . s = ((1 - r) * r1) + (r * r2) ) & ( for s being Point of (Closed-Interval-TSpace 0 ,1)
for r, r1, r2 being real number st s = r & r1 = t1 & r2 = t2 holds
F2 . s = ((1 - r) * r1) + (r * r2) ) implies F1 = F2 )
assume A16: for s being Point of (Closed-Interval-TSpace 0 ,1)
for r, r1, r2 being real number st s = r & r1 = t1 & r2 = t2 holds
F1 . s = ((1 - r) * r1) + (r * r2) ; :: thesis: ( ex s being Point of (Closed-Interval-TSpace 0 ,1) ex r, r1, r2 being real number st
( s = r & r1 = t1 & r2 = t2 & not F2 . s = ((1 - r) * r1) + (r * r2) ) or F1 = F2 )
assume A17: for s being Point of (Closed-Interval-TSpace 0 ,1)
for r, r1, r2 being real number st s = r & r1 = t1 & r2 = t2 holds
F2 . s = ((1 - r) * r1) + (r * r2) ; :: thesis: F1 = F2
for s being Point of (Closed-Interval-TSpace 0 ,1) holds F1 . s = F2 . s

proof

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

end;

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