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

proof

let n1, n2 be object ; :: thesis: ( n1 in dom IT & n2 in dom IT implies IT . n1 = IT . n2 )
assume that
A2: n1 in dom IT and
A3: n2 in dom IT ; :: thesis: IT . n1 = IT . n2
IT . n1 = a by A2, FUNCOP_1:7
.= IT . n2 by A3, FUNCOP_1:7 ;
hence IT . n1 = IT . n2 ; :: thesis: verum

end;

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