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
A6: the carrier of T1 = product (Carrier J) and
A7: product_prebasis J is prebasis of T1 and
A8: the carrier of T2 = product (Carrier J) and
A9: product_prebasis J is prebasis of T2 ; :: thesis: T1 = T2
now :: thesis: not {} in rng (Carrier J)
assume {} in rng (Carrier J) ; :: thesis: contradiction
then consider i being object such that
A10: i in dom (Carrier J) and
A11: {} = (Carrier J) . i by FUNCT_1:def 3;
consider R being 1-sorted such that
A12: R = J . i and
A13: {} = the carrier of R by A10, A11, PRALG_1:def 15;
dom J = I by PARTFUN1:def 2;
then R in rng J by A10, A12, FUNCT_1:def 3;
then reconsider R = R as non empty 1-sorted by WAYBEL_3:def 7;
the carrier of R = {} by A13;
hence contradiction ; :: thesis: verum
end;
then product (Carrier J) <> {} by CARD_3:26;
then reconsider t1 = T1, t2 = T2 as non empty TopSpace by A6, A8;
t1 = t2 by A6, A7, A8, A9, CANTOR_1:17;
hence T1 = T2 ; :: thesis: verum