let X be non empty TopSpace; :: thesis: for M being non empty set holds oContMaps X,(M -TOP_prod (M --> Sierpinski_Space )),M -POS_prod (M --> (oContMaps X,Sierpinski_Space )) are_isomorphic
let M be non empty set ; :: thesis: oContMaps X,(M -TOP_prod (M --> Sierpinski_Space )),M -POS_prod (M --> (oContMaps X,Sierpinski_Space )) are_isomorphic
consider F being Function of (oContMaps X,(M -TOP_prod (M --> Sierpinski_Space ))),(M -POS_prod (M --> (oContMaps X,Sierpinski_Space ))) such that
A1: F is isomorphic and
for f being continuous Function of X,(M -TOP_prod (M --> Sierpinski_Space )) holds F . f = commute f by Th35;
take F ; :: according to WAYBEL_1:def 8 :: thesis: F is isomorphic
thus F is isomorphic by A1; :: thesis: verum