let X, Y, X1, Y1 be TopSpace; :: thesis: ( TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of X1, the topology of X1 #) & TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of Y1, the topology of Y1 #) implies [:X,Y:] = [:X1,Y1:] )
assume A1: ( TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of X1, the topology of X1 #) & TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of Y1, the topology of Y1 #) ) ; :: thesis: [:X,Y:] = [:X1,Y1:]
set U2 = { (union A) where A is Subset-Family of [:X1,Y1:] : A c= { [:X2,Y2:] where X2 is Subset of X1, Y2 is Subset of Y1 : ( X2 in the topology of X1 & Y2 in the topology of Y1 ) } } ;
A2: the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] by BORSUK_1:def 2
.= the carrier of [:X1,Y1:] by A1, BORSUK_1:def 2 ;
then the topology of [:X,Y:] = { (union A) where A is Subset-Family of [:X1,Y1:] : A c= { [:X2,Y2:] where X2 is Subset of X1, Y2 is Subset of Y1 : ( X2 in the topology of X1 & Y2 in the topology of Y1 ) } } by A1, BORSUK_1:def 2
.= the topology of [:X1,Y1:] by BORSUK_1:def 2 ;
hence [:X,Y:] = [:X1,Y1:] by A2; :: thesis: verum