theorem :: BORSUK_3:1

for S, T being TopSpace holds [#] [:S,T:] = [:([#] S),([#] T):] by BORSUK_1:def 2;