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

proof

let s be Point of (Closed-Interval-TSpace a,b); :: 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

end;

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