let M be non empty set ; :: thesis: for i being Element of M
for T being non empty TopSpace
for x being Point of (product (M --> T)) holds pi ((Cl {x}),i) = Cl {(x . i)}
let i be Element of M; :: thesis: for T being non empty TopSpace
for x being Point of (product (M --> T)) holds pi ((Cl {x}),i) = Cl {(x . i)}
let T be non empty TopSpace; :: thesis: for x being Point of (product (M --> T)) holds pi ((Cl {x}),i) = Cl {(x . i)}
let x be Point of (product (M --> T)); :: thesis: pi ((Cl {x}),i) = Cl {(x . i)}
(M --> T) . i = T ;
hence pi ((Cl {x}),i) = Cl {(x . i)} by Th31; :: thesis: verum