set IT = I[01] --> a;
A1: ( (I[01] --> a) . 0 = a & (I[01] --> a) . 1 = a ) by BORSUK_1:def 17, BORSUK_1:def 18, FUNCOP_1:13;
a,a are_connected ;
then reconsider IT = I[01] --> a as Path of a,a by A1, Def2;
for n1, n2 being set st n1 in dom IT & n2 in dom IT holds
IT . n1 = IT . n2

proof

let n1, n2 be set ; :: thesis: ( n1 in dom IT & n2 in dom IT implies IT . n1 = IT . n2 )
assume A2: ( n1 in dom IT & n2 in dom IT ) ; :: thesis: IT . n1 = IT . n2
then IT . n1 = a by FUNCOP_1:13
.= IT . n2 by A2, FUNCOP_1:13 ;
hence IT . n1 = IT . n2 ; :: thesis: verum

end;

then IT is constant by FUNCT_1:def 16;
hence ex b₁ being Path of a,a st b₁ is constant ; :: thesis: verum