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
A28: 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
A29: 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
A30: 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 A31: x in dom A ; :: thesis: A . x = B . x
then reconsider y = x as Point of I[01] ;
x in the carrier of I[01] by A31;
then x in { r where r is Real : ( 0 <= r & r <= 1 ) } by BORSUK_1:40, RCOMP_1:def 1;
then consider r9 being Real such that
A32: r9 = x and
0 <= r9 and
r9 <= 1 ;

per cases ( r9 <= 1 / 2 or 1 / 2 < r9 ) ;

suppose A33: r9 <= 1 / 2 ; :: thesis: A . x = B . x

then A . y = P . (2 * r9) by A28, A32
.= B . y by A29, A32, A33 ;
hence A . x = B . x ; :: thesis: verum

end;

suppose A34: 1 / 2 < r9 ; :: thesis: A . x = B . x

then A . y = Q . ((2 * r9) - 1) by A28, A32
.= B . y by A29, A32, A34 ;
hence A . x = B . x ; :: thesis: verum

end;

end;

end;

dom B = the carrier of I[01] by FUNCT_2:def 1;
then dom A = dom B by FUNCT_2:def 1;
hence A = B by A30, FUNCT_1:2; :: thesis: verum