theorem Th7: :: WAYBEL29:7

for X, Y, X1, Y1 being TopSpace st 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 #) holds
[:X,Y:] = [:X1,Y1:]