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

hence ex b_{1} being Path of a,a st b_{1} is constant
; :: thesis: verum

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

then
IT is constant
by FUNCT_1:def 10;
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;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

hence ex b