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
A29: 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
A30: 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
A31: for x being object st x in dom A holds
A . x = B . x
proof
let x be object ; :: thesis: ( x in dom A implies A . x = B . x )
assume A32: 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 A32;
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
A33: r9 = x and
0 <= r9 and
r9 <= 1 ;
per cases ( r9 <= 1 / 2 or 1 / 2 < r9 ) ;
suppose A34: r9 <= 1 / 2 ; :: thesis: A . x = B . x
then A . y = P . (2 * r9) by A29, A33
.= B . y by A30, A33, A34 ;
hence A . x = B . x ; :: thesis: verum
end;
suppose A35: 1 / 2 < r9 ; :: thesis: A . x = B . x
then A . y = Q . ((2 * r9) - 1) by A29, A33
.= B . y by A30, A33, A35 ;
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 A31, FUNCT_1:2; :: thesis: verum