let A, B be Path of a,c; :: thesis: ( ( for t being Point of I[01] holds
( ( t <= 1 / 2 implies A . t = P . (2 * t) ) & ( 1 / 2 <= t implies A . t = Q . ((2 * t) - 1) ) ) ) & ( for t being Point of I[01] holds
( ( t <= 1 / 2 implies B . t = P . (2 * t) ) & ( 1 / 2 <= t implies B . t = Q . ((2 * t) - 1) ) ) ) implies A = B )
assume that
A33: for t being Point of I[01] holds
( ( t <= 1 / 2 implies A . t = P . (2 * t) ) & ( 1 / 2 <= t implies A . t = Q . ((2 * t) - 1) ) ) and
A34: for t being Point of I[01] holds
( ( t <= 1 / 2 implies B . t = P . (2 * t) ) & ( 1 / 2 <= t implies B . t = Q . ((2 * t) - 1) ) ) ; :: thesis: A = B
A35: dom B = the carrier of I[01] by FUNCT_2:def 1;
A = B

proof

A36: dom A = dom B by A35, FUNCT_2:def 1;
for x being set st x in dom A holds
A . x = B . x

proof

let x be set ; :: thesis: ( x in dom A implies A . x = B . x )
assume A37: x in dom A ; :: thesis: A . x = B . x
then A38: x in the carrier of I[01] ;
reconsider y = x as Point of I[01] by A37;
x in { r where r is Real : ( 0 <= r & r <= 1 ) } by A38, BORSUK_1:83, RCOMP_1:def 1;
then consider r' being Real such that
A39: ( r' = x & 0 <= r' & r' <= 1 ) ;

per cases ( r' <= 1 / 2 or 1 / 2 < r' ) ;

suppose A40: r' <= 1 / 2 ; :: thesis: A . x = B . x

then A . y = P . (2 * r') by A33, A39
.= B . y by A34, A39, A40 ;
hence A . x = B . x ; :: thesis: verum

end;

suppose A41: 1 / 2 < r' ; :: thesis: A . x = B . x

then A . y = Q . ((2 * r') - 1) by A33, A39
.= B . y by A34, A39, A41 ;
hence A . x = B . x ; :: thesis: verum

end;

end;

end;

hence A = B by A36, FUNCT_1:9; :: thesis: verum

end;

hence A = B ; :: thesis: verum