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

then dom A = dom B by FUNCT_2:def 1;

hence A = B by A31, FUNCT_1:2; :: thesis: verum

( ( 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

dom B = the carrier of I[01]
by FUNCT_2:def 1;
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 ;

end;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 ;

then dom A = dom B by FUNCT_2:def 1;

hence A = B by A31, FUNCT_1:2; :: thesis: verum