let M be non empty set ; :: thesis: for T being injective T_0-TopSpace holds Omega (M -TOP_prod (M => T)) = Sigma (M -POS_prod (M => (Omega T)))
let T be injective T_0-TopSpace; :: thesis: Omega (M -TOP_prod (M => T)) = Sigma (M -POS_prod (M => (Omega T)))
set L = Omega T;
RelStr(# the carrier of (Omega (M -TOP_prod (M => T))), the InternalRel of (Omega (M -TOP_prod (M => T))) #) = M -POS_prod (M => (Omega T)) by WAYBEL25:14;
then Sigma (Omega (M -TOP_prod (M => T))) = Sigma (M -POS_prod (M => (Omega T))) by Th16;
hence Omega (M -TOP_prod (M => T)) = Sigma (M -POS_prod (M => (Omega T))) by Th15; :: thesis: verum