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 indom A holds A . x = B . x