environ
vocabularies HIDDEN, NUMBERS, NAT_1, XBOOLE_0, FINSEQ_1, ORDINAL4, PARTFUN1, XXREAL_0, ARYTM_3, MATRIX_1, ZFMISC_1, SUBSET_1, PRE_TOPC, EUCLID, REAL_1, CARD_1, ARYTM_1, RELAT_1, SUPINF_2, RLTOPSP1, METRIC_1, RELAT_2, CONVEX1, RCOMP_1, CONNSP_1, TARSKI, PCOMPS_1, SPPOL_1, MCART_1, GOBOARD1, TREES_1, PSCOMP_1, TOPREAL1, SPRECT_1, SPPOL_2, JORDAN3, FUNCT_1, RFINSEQ, GROUP_2, GOBOARD5, GOBOARD9, TOPREAL4, JORDAN5D, GOBOARD2, SPRECT_2, COMPLEX1, ORDINAL2, TOPS_1, JORDAN5C, FINSEQ_5;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, NAT_D, CARD_1, RFINSEQ, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_4, FINSEQ_5, MATRIX_0, MATRIX_1, SEQM_3, SEQ_4, FINSEQ_6, STRUCT_0, METRIC_1, PRE_TOPC, TOPS_1, COMPTS_1, CONNSP_1, PCOMPS_1, RLVECT_1, RLTOPSP1, EUCLID, TOPREAL1, TOPREAL4, PSCOMP_1, GOBOARD1, GOBOARD2, SPPOL_1, SPPOL_2, GOBOARD5, GOBOARD9, JORDAN3, JORDAN5C, JORDAN5D, SPRECT_1, SPRECT_2, XXREAL_0;
definitions TARSKI, SPRECT_2, JORDAN1, TOPREAL4, XBOOLE_0, SEQM_3;
theorems FINSEQ_4, TARSKI, FINSEQ_3, FINSEQ_1, SPRECT_2, GOBOARD7, PSCOMP_1, SPRECT_1, TOPREAL3, SPPOL_2, NAT_1, SPPOL_1, EUCLID, ZFMISC_1, TOPREAL1, GOBOARD5, JORDAN5D, FINSEQ_5, FINSEQ_6, JORDAN4, JORDAN3, TOPREAL5, GOBRD11, GOBOARD9, TOPMETR, GOBOARD6, JORDAN1, CONNSP_1, SUBSET_1, GOBRD12, JORDAN5C, JORDAN6, GOBOARD1, ENUMSET1, CARD_2, GOBOARD2, NAT_2, ABSVALUE, GOBOARD8, PARTFUN2, FUNCT_1, XBOOLE_0, XBOOLE_1, FINSEQ_2, XREAL_1, XXREAL_0, PARTFUN1, MATRIX_0, NAT_D, PRE_TOPC, RLTOPSP1, SEQM_3, SEQ_4, XTUPLE_0, RVSUM_1, RLVECT_1;
schemes DOMAIN_1;
registrations RELSET_1, XREAL_0, FINSEQ_1, STRUCT_0, EUCLID, GOBOARD2, SPPOL_2, SPRECT_1, SPRECT_2, VALUED_0, CARD_1, FUNCT_1, SEQ_4, SPPOL_1, TOPS_1, JORDAN1, RVSUM_1, NAT_1, ORDINAL1;
constructors HIDDEN, REAL_1, FINSEQ_4, RFINSEQ, NAT_D, TOPS_1, CONNSP_1, TOPS_2, COMPTS_1, MATRIX_1, TOPMETR, TOPREAL2, TOPREAL4, GOBOARD2, SPPOL_1, PSCOMP_1, GOBOARD9, JORDAN3, JORDAN5C, SPRECT_1, SPRECT_2, JORDAN5D, GOBOARD1, PCOMPS_1, BINARITH, FUNCSDOM, CONVEX1, SEQ_4, RVSUM_1, VALUED_0;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities RLTOPSP1, XBOOLE_0, PSCOMP_1;
expansions TARSKI, SPRECT_2, JORDAN1, XBOOLE_0;
theorem Th2:
for
a,
b,
c,
d being
set holds
Indices ((a,b) ][ (c,d)) = {[1,1],[1,2],[2,1],[2,2]}