theorem Th13: :: DECOMP_1:13

for T being TopSpace holds (PSO T) /\ (D(alpha,ps) T) = T ^alpha