let X, Y be TopSpace; :: thesis: for Z being Subset of [:Y,X:]
for V being Subset of X st Z = [:([#] Y),V:] holds
TopStruct(# the carrier of [:Y,(X | V):], the topology of [:Y,(X | V):] #) = TopStruct(# the carrier of ([:Y,X:] | Z), the topology of ([:Y,X:] | Z) #)
let Z be Subset of [:Y,X:]; :: thesis: for V being Subset of X st Z = [:([#] Y),V:] holds
TopStruct(# the carrier of [:Y,(X | V):], the topology of [:Y,(X | V):] #) = TopStruct(# the carrier of ([:Y,X:] | Z), the topology of ([:Y,X:] | Z) #)
let V be Subset of X; :: thesis: ( Z = [:([#] Y),V:] implies TopStruct(# the carrier of [:Y,(X | V):], the topology of [:Y,(X | V):] #) = TopStruct(# the carrier of ([:Y,X:] | Z), the topology of ([:Y,X:] | Z) #) )
reconsider A = [:Y,(X | V):] as SubSpace of [:Y,X:] by Th15;
assume A1: Z = [:([#] Y),V:] ; :: thesis: TopStruct(# the carrier of [:Y,(X | V):], the topology of [:Y,(X | V):] #) = TopStruct(# the carrier of ([:Y,X:] | Z), the topology of ([:Y,X:] | Z) #)
the carrier of A = [: the carrier of Y, the carrier of (X | V):] by BORSUK_1:def 2
.= Z by A1, PRE_TOPC:8
.= the carrier of ([:Y,X:] | Z) by PRE_TOPC:8 ;
then ( A is SubSpace of [:Y,X:] | Z & [:Y,X:] | Z is SubSpace of A ) by TOPMETR:3;
hence TopStruct(# the carrier of [:Y,(X | V):], the topology of [:Y,(X | V):] #) = TopStruct(# the carrier of ([:Y,X:] | Z), the topology of ([:Y,X:] | Z) #) by TSEP_1:6; :: thesis: verum