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

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