let R, Q be Path of b,a; :: thesis: ( ( for t being Point of holds R . t = P . (1 - t) ) & ( for t being Point of holds Q . t = P . (1 - t) ) implies R = Q )
assume that
A9: for t being Point of holds R . t = P . (1 - t) and
A10: for t being Point of holds Q . t = P . (1 - t) ; :: thesis: R = Q
A11: for x being set st x in the carrier of I[01] holds
R . x = Q . x

proof

let x be set ; :: thesis: ( x in the carrier of I[01] implies R . x = Q . x )
assume x in the carrier of I[01] ; :: thesis: R . x = Q . x
then reconsider x' = x as Point of ;
R . x' = P . (1 - x') by A9
.= Q . x' by A10 ;
hence R . x = Q . x ; :: thesis: verum

end;

( dom R = the carrier of I[01] & the carrier of I[01] = dom Q ) by FUNCT_2:def 1;
hence R = Q by A11, FUNCT_1:9; :: thesis: verum