thus ExtendInt r is continuous ; :: according to BORSUK_2:def 4 :: thesis: ( (ExtendInt r) . 0 = R^1 0 & (ExtendInt r) . 1 = R^1 r )
thus (ExtendInt r) . 0 = r * 0 by Def1, BORSUK_1:def 14
.= R^1 0 by TOPREALB:def 2 ; :: thesis: (ExtendInt r) . 1 = R^1 r
thus (ExtendInt r) . 1 = r * 1 by Def1, BORSUK_1:def 15
.= R^1 r by TOPREALB:def 2 ; :: thesis: verum