let X, Y be TopSpace; 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; verum