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

hence R = Q by A11, FUNCT_1:2; :: thesis: verum

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

( dom R = the carrier of I[01] & the carrier of I[01] = dom Q )
by FUNCT_2:def 1;
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;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

hence R = Q by A11, FUNCT_1:2; :: thesis: verum