M -POS_prod (M => (oContMaps (X,Sierpinski_Space))) = (oContMaps (X,Sierpinski_Space)) |^ M by YELLOW_1:def 5;
then ex f1 being Function of (oContMaps (X,(M -TOP_prod (M => Sierpinski_Space)))),((oContMaps (X,Sierpinski_Space)) |^ M) st
( f1 is isomorphic & ( for f being continuous Function of X,(M -TOP_prod (M => Sierpinski_Space)) holds f1 . f = commute f ) ) by WAYBEL26:34;
hence commute (X,M,Sierpinski_Space) is isomorphic by Def5; :: thesis: verum