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