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

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