thus A1:
t,t are_connected
; :: according to BORSUK_2:def 2 :: thesis: ( inverse_loop f is continuous & (inverse_loop f) . 0 = t & (inverse_loop f) . 1 = t )

thus inverse_loop f is continuous ; :: thesis: ( (inverse_loop f) . 0 = t & (inverse_loop f) . 1 = t )

A2: t = 1_ T by Def1;

A3: (1_ T) " = 1_ T ;

( f . 0[01] = t & f . 1[01] = t ) by A1, BORSUK_2:def 2;

hence ( (inverse_loop f) . 0 = t & (inverse_loop f) . 1 = t ) by A2, A3, Th2; :: thesis: verum

thus inverse_loop f is continuous ; :: thesis: ( (inverse_loop f) . 0 = t & (inverse_loop f) . 1 = t )

A2: t = 1_ T by Def1;

A3: (1_ T) " = 1_ T ;

( f . 0[01] = t & f . 1[01] = t ) by A1, BORSUK_2:def 2;

hence ( (inverse_loop f) . 0 = t & (inverse_loop f) . 1 = t ) by A2, A3, Th2; :: thesis: verum