M -POS_prod (M => (oContMaps X,Sierpinski_Space )) = (oContMaps X,Sierpinski_Space ) |^ M by YELLOW_1:def 5;
then consider f1 being Function of (oContMaps X,(M -TOP_prod (M => Sierpinski_Space ))),((oContMaps X,Sierpinski_Space ) |^ M) such that
A1: f1 is isomorphic and
A2: for f being continuous Function of X,(M -TOP_prod (M => Sierpinski_Space )) holds f1 . f = commute f by WAYBEL26:35;
thus commute X,M,Sierpinski_Space is isomorphic by A1, A2, Def5; :: thesis: verum