A1: [:I[01],I[01]:] is SubSpace of [:R^1,R^1:] by BORSUK_3:21;
the carrier of [:I[01],I[01]:] = [:(R^1 [.0,1.]),(R^1 [.0,1.]):] by BORSUK_1:def 2, BORSUK_1:40;
hence [:R^1,R^1:] | [:(R^1 [.0,1.]),(R^1 [.0,1.]):] = [:I[01],I[01]:] by A1, TSEP_1:5, PRE_TOPC:8; :: thesis: verum