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:35;
hence commute X,M,Sierpinski_Space is isomorphic by Def5; :: thesis: verum