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 #):];
A1: 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 2
.= the carrier of [:X,Y:] by BORSUK_1:def 2 ;
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 2
.= { (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 A1, BORSUK_1:def 2 ;
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 A1; :: thesis: verum