theorem Th12: :: DECOMP_1:12

for T being TopSpace holds (SO T) /\ (D(alpha,s) T) = T ^alpha