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

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

end;