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_{1} being Path of a,a st b_{1} is continuous
; :: thesis: verum

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