let M be non empty set ; :: thesis: for L being continuous complete LATTICE holds Omega (M -TOP_prod (M => (Sigma L))) = Sigma (M -POS_prod (M => L))
let L be continuous complete LATTICE; :: thesis: Omega (M -TOP_prod (M => (Sigma L))) = Sigma (M -POS_prod (M => L))
A1: RelStr(# the carrier of (Sigma L), the InternalRel of (Sigma L) #) = RelStr(# the carrier of L, the InternalRel of L #) by YELLOW_9:def 4;
reconsider S = Sigma L as injective T_0-TopSpace ;
Omega (Sigma L) = Sigma L by WAYBEL25:15;
then RelStr(# the carrier of (Omega (M -TOP_prod (M => (Sigma L)))), the InternalRel of (Omega (M -TOP_prod (M => (Sigma L)))) #) = M -POS_prod (M => (Sigma L)) by WAYBEL25:14
.= (Sigma L) |^ M by YELLOW_1:def 5
.= L |^ M by A1, WAYBEL27:15 ;
then Sigma (L |^ M) = Sigma (Omega (M -TOP_prod (M => S))) by Th16
.= Omega (M -TOP_prod (M => (Sigma L))) by Th15 ;
hence Omega (M -TOP_prod (M => (Sigma L))) = Sigma (M -POS_prod (M => L)) by YELLOW_1:def 5; :: thesis: verum