let S, T be TopSpace; :: thesis: TopStruct(# the carrier of [:S,T:], the topology of [:S,T:] #) = [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):]
A1: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by BORSUK_1:def 2
.= the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] by BORSUK_1:def 2 ;
for C1 being Subset of [:S,T:]
for C2 being Subset of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] st C1 = C2 holds
( C1 is open iff C2 is open )

proof

let C1 be Subset of [:S,T:]; :: thesis: for C2 being Subset of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] st C1 = C2 holds
( C1 is open iff C2 is open )
let C2 be Subset of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):]; :: thesis: ( C1 = C2 implies ( C1 is open iff C2 is open ) )
assume A2: C1 = C2 ; :: thesis: ( C1 is open iff C2 is open )

hereby :: thesis: ( C2 is open implies C1 is open )

assume C1 is open ; :: thesis: C2 is open
then consider A being Subset-Family of [:S,T:] such that
A3: C1 = union A and
A4: for e being set st e in A holds
ex X1 being Subset of S ex Y1 being Subset of T st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by BORSUK_1:5;
reconsider AA = A as Subset-Family of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] by A1;
for e being set st e in AA holds
ex X1 being Subset of TopStruct(# the carrier of S, the topology of S #) ex Y1 being Subset of TopStruct(# the carrier of T, the topology of T #) st
( e = [:X1,Y1:] & X1 is open & Y1 is open )

proof

let e be set ; :: thesis: ( e in AA implies ex X1 being Subset of TopStruct(# the carrier of S, the topology of S #) ex Y1 being Subset of TopStruct(# the carrier of T, the topology of T #) st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) )
assume e in AA ; :: thesis: ex X1 being Subset of TopStruct(# the carrier of S, the topology of S #) ex Y1 being Subset of TopStruct(# the carrier of T, the topology of T #) st
( e = [:X1,Y1:] & X1 is open & Y1 is open )
then consider X1 being Subset of S, Y1 being Subset of T such that
A5: ( e = [:X1,Y1:] & X1 is open & Y1 is open ) by A4;
reconsider Y2 = Y1 as Subset of TopStruct(# the carrier of T, the topology of T #) ;
reconsider X2 = X1 as Subset of TopStruct(# the carrier of S, the topology of S #) ;
take X2 ; :: thesis: ex Y1 being Subset of TopStruct(# the carrier of T, the topology of T #) st
( e = [:X2,Y1:] & X2 is open & Y1 is open )
take Y2 ; :: thesis: ( e = [:X2,Y2:] & X2 is open & Y2 is open )
thus ( e = [:X2,Y2:] & X2 is open & Y2 is open ) by A5, TOPS_3:76; :: thesis: verum

end;

hence C2 is open by A2, A3, BORSUK_1:5; :: thesis: verum

end;

assume C2 is open ; :: thesis: C1 is open
then consider A being Subset-Family of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] such that
A6: C2 = union A and
A7: for e being set st e in A holds
ex X1 being Subset of TopStruct(# the carrier of S, the topology of S #) ex Y1 being Subset of TopStruct(# the carrier of T, the topology of T #) st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by BORSUK_1:5;
reconsider AA = A as Subset-Family of [:S,T:] by A1;
for e being set st e in AA holds
ex X1 being Subset of S ex Y1 being Subset of T st
( e = [:X1,Y1:] & X1 is open & Y1 is open )

proof

let e be set ; :: thesis: ( e in AA implies ex X1 being Subset of S ex Y1 being Subset of T st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) )
assume e in AA ; :: thesis: ex X1 being Subset of S ex Y1 being Subset of T st
( e = [:X1,Y1:] & X1 is open & Y1 is open )
then consider X1 being Subset of TopStruct(# the carrier of S, the topology of S #), Y1 being Subset of TopStruct(# the carrier of T, the topology of T #) such that
A8: ( e = [:X1,Y1:] & X1 is open & Y1 is open ) by A7;
reconsider Y2 = Y1 as Subset of T ;
reconsider X2 = X1 as Subset of S ;
take X2 ; :: thesis: ex Y1 being Subset of T st
( e = [:X2,Y1:] & X2 is open & Y1 is open )
take Y2 ; :: thesis: ( e = [:X2,Y2:] & X2 is open & Y2 is open )
thus ( e = [:X2,Y2:] & X2 is open & Y2 is open ) by A8, TOPS_3:76; :: thesis: verum

end;

hence C1 is open by A2, A6, BORSUK_1:5; :: thesis: verum

end;

hence TopStruct(# the carrier of [:S,T:], the topology of [:S,T:] #) = [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] by A1, TOPS_3:72; :: thesis: verum