let R, Q be Path of b,a; :: thesis: ( ( for t being Point of I[01] holds R . t = P . (1 - t) ) & ( for t being Point of I[01] holds Q . t = P . (1 - t) ) implies R = Q )
assume that
A9: for t being Point of I[01] holds R . t = P . (1 - t) and
A10: for t being Point of I[01] holds Q . t = P . (1 - t) ; :: thesis: R = Q
A11: for x being object st x in the carrier of I[01] holds
R . x = Q . x
proof
let x be object ; :: 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 x9 = x as Point of I[01] ;
R . x9 = P . (1 - x9) by A9
.= Q . x9 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:2; :: thesis: verum