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 Th34;
take F ; :: according to WAYBEL_1:def 8 :: thesis: F is isomorphic
thus F is isomorphic by A1; :: thesis: verum