set IT = I[01] --> a;
A1: a,a are_connected ;
( (I[01] --> a) . 0 = a & (I[01] --> a) . 1 = a ) by BORSUK_1:def 14, BORSUK_1:def 15, FUNCOP_1:7;
then I[01] --> a is Path of a,a by A1, Def2;
hence ex b₁ being Path of a,a st b₁ is continuous ; :: thesis: verum