environ
vocabularies HIDDEN, NAT_1, VECTSP_1, MATRIX_1, ARYTM_1, ARYTM_3, FINSEQ_1, CARD_1, XXREAL_0, TREES_1, RELAT_1, SUPINF_2, SUBSET_1, NUMBERS, RVSUM_1, FINSEQ_2, STRUCT_0, FUNCT_1, TARSKI, ALGSTR_0, ZFMISC_1, XBOOLE_0, PARTFUN1, INCSP_1, CARD_3, FVSUM_1;
notations HIDDEN, TARSKI, XBOOLE_0, FINSEQ_2, SUBSET_1, ORDINAL1, NUMBERS, NAT_1, ZFMISC_1, RELAT_1, FUNCT_1, FINSEQ_1, MATRIX_0, STRUCT_0, ALGSTR_0, BINOP_1, FINSEQOP, MATRIX_3, MATRIX_1, VECTSP_1, FVSUM_1, FUNCT_3, XXREAL_0;
definitions ;
theorems FINSEQ_1, FUNCT_1, FUNCT_2, NAT_1, ZFMISC_1, XBOOLE_0, RLVECT_1, MATRIX_3, VECTSP_1, FVSUM_1, FINSEQ_2, FUNCOP_1, FINSEQOP, FUNCT_3, CARD_2, CARD_1, MATRIX_0, ORDINAL1;
schemes ;
registrations XBOOLE_0, FUNCT_1, RELSET_1, XREAL_0, STRUCT_0, ORDINAL1, FINSEQ_2, CARD_1;
constructors HIDDEN, BINOP_1, FUNCT_3, NAT_1, FVSUM_1, MATRIX_3, RELSET_1, MATRIX_1;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities BINOP_1, MATRIX_0, MATRIX_3, ALGSTR_0;
expansions ;
theorem Th9:
for
n,
m being
Nat for
K being
Field holds
- (0. (K,n,m)) = 0. (
K,
n,
m)
theorem
for
K being
Field for
M1,
M2,
M3 being
Matrix of
K st
- M1 = - M2 holds
M1 = M2