let X, Y be TopSpace; :: thesis: TopStruct(# the carrier of [:X,Y:],the topology of [:X,Y:] #) = [:TopStruct(# the carrier of X,the topology of X #),TopStruct(# the carrier of Y,the topology of Y #):]
set T = [:TopStruct(# the carrier of X,the topology of X #),TopStruct(# the carrier of Y,the topology of Y #):];
A: the carrier of [:TopStruct(# the carrier of X,the topology of X #),TopStruct(# the carrier of Y,the topology of Y #):] = [:the carrier of TopStruct(# the carrier of X,the topology of X #),the carrier of TopStruct(# the carrier of Y,the topology of Y #):] by BORSUK_1:def 5
.= the carrier of [:X,Y:] by BORSUK_1:def 5 ;
set tau1 = { (union A) where A is Subset-Family of [:TopStruct(# the carrier of X,the topology of X #),TopStruct(# the carrier of Y,the topology of Y #):] : A c= { [:X1,Y1:] where X1 is Subset of TopStruct(# the carrier of X,the topology of X #), Y1 is Subset of TopStruct(# the carrier of Y,the topology of Y #) : ( X1 in the topology of TopStruct(# the carrier of X,the topology of X #) & Y1 in the topology of TopStruct(# the carrier of Y,the topology of Y #) ) } } ;
set tau2 = { (union A) where A is Subset-Family of [:TopStruct(# the carrier of X,the topology of X #),TopStruct(# the carrier of Y,the topology of Y #):] : A c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) } } ;
the topology of [:TopStruct(# the carrier of X,the topology of X #),TopStruct(# the carrier of Y,the topology of Y #):] = { (union A) where A is Subset-Family of [:TopStruct(# the carrier of X,the topology of X #),TopStruct(# the carrier of Y,the topology of Y #):] : A c= { [:X1,Y1:] where X1 is Subset of TopStruct(# the carrier of X,the topology of X #), Y1 is Subset of TopStruct(# the carrier of Y,the topology of Y #) : ( X1 in the topology of TopStruct(# the carrier of X,the topology of X #) & Y1 in the topology of TopStruct(# the carrier of Y,the topology of Y #) ) } } by BORSUK_1:def 5
.= { (union A) where A is Subset-Family of [:TopStruct(# the carrier of X,the topology of X #),TopStruct(# the carrier of Y,the topology of Y #):] : A c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) } }
.= the topology of [:X,Y:] by BORSUK_1:def 5, A ;
hence TopStruct(# the carrier of [:X,Y:],the topology of [:X,Y:] #) = [:TopStruct(# the carrier of X,the topology of X #),TopStruct(# the carrier of Y,the topology of Y #):] by A; :: thesis: verum