let M be non empty set ; :: thesis: for T being non empty TopSpace
for x, y being Point of (product (M --> T)) holds
( x in Cl {y} iff for i being Element of M holds x . i in Cl {(y . i)} )
let T be non empty TopSpace; :: thesis: for x, y being Point of (product (M --> T)) holds
( x in Cl {y} iff for i being Element of M holds x . i in Cl {(y . i)} )
let x, y be Point of (product (M --> T)); :: thesis: ( x in Cl {y} iff for i being Element of M holds x . i in Cl {(y . i)} )
reconsider J = M --> T as non-Empty TopStruct-yielding ManySortedSet of M ;
reconsider x9 = x, y9 = y as Point of (product J) ;
thus ( x in Cl {y} implies for i being Element of M holds x . i in Cl {(y . i)} ) :: thesis: ( ( for i being Element of M holds x . i in Cl {(y . i)} ) implies x in Cl {y} )
proof
assume A1: x in Cl {y} ; :: thesis: for i being Element of M holds x . i in Cl {(y . i)}
let i be Element of M; :: thesis: x . i in Cl {(y . i)}
x9 . i in Cl {(y9 . i)} by A1, Th29;
hence x . i in Cl {(y . i)} ; :: thesis: verum
end;
assume for i being Element of M holds x . i in Cl {(y . i)} ; :: thesis: x in Cl {y}
then for i being Element of M holds x9 . i in Cl {(y9 . i)} ;
hence x in Cl {y} by Th29; :: thesis: verum