let T1, T2 be strict TopSpace; :: thesis: ( the carrier of T1 = product (Carrier J) & product_prebasis J is prebasis of T1 & the carrier of T2 = product (Carrier J) & product_prebasis J is prebasis of T2 implies T1 = T2 )
assume that
A5: the carrier of T1 = product (Carrier J) and
A6: product_prebasis J is prebasis of T1 and
A7: the carrier of T2 = product (Carrier J) and
A8: product_prebasis J is prebasis of T2 ; :: thesis: T1 = T2

now

assume {} in rng (Carrier J) ; :: thesis: contradiction
then consider i being set such that
A9: ( i in dom (Carrier J) & {} = (Carrier J) . i ) by FUNCT_1:def 5;
A10: ( dom (Carrier J) = I & dom J = I ) by PARTFUN1:def 4;
then consider R being 1-sorted such that
A11: ( R = J . i & {} = the carrier of R ) by A9, PRALG_1:def 13;
R in rng J by A9, A10, A11, FUNCT_1:def 5;
then reconsider R = R as non empty 1-sorted by WAYBEL_3:def 7;
the carrier of R = {} by A11;
hence contradiction ; :: thesis: verum

end;

then product (Carrier J) <> {} by CARD_3:37;
then reconsider t1 = T1, t2 = T2 as non empty TopSpace by A5, A7;
t1 = t2 by A5, A6, A7, A8, CANTOR_1:19;
hence T1 = T2 ; :: thesis: verum