environ
vocabularies HIDDEN, NAT_1, VECTSP_1, SUBSET_1, MATRIX_1, REWRITE1, RELAT_1, MESFUNC1, ALGSTR_0, ARYTM_1, FINSEQ_1, TREES_1, ARYTM_3, SUPINF_2, XXREAL_0, CARD_1, QC_LANG1, ZFMISC_1, RELAT_2, FUNCOP_1, GROUP_1, MATRIX_6, FUNCSDOM, MATRIX_0;
notations HIDDEN, TARSKI, ZFMISC_1, ORDINAL1, NUMBERS, FINSEQ_1, RLVECT_1, GROUP_1, VECTSP_1, MATRIX_0, STRUCT_0, MATRIX_1, MATRIX_3, MATRIX_4, XXREAL_0;
definitions ;
theorems ZFMISC_1, RLVECT_1, MATRIX_0, MATRIX_4, MATRIX_3, VECTSP_1, NAT_1, CARD_2, XXREAL_0, MATRIX_1;
schemes ;
registrations RELSET_1, XREAL_0, STRUCT_0, VECTSP_1, ORDINAL1, MATRIX_0, MATRIX_1;
constructors HIDDEN, XXREAL_0, FVSUM_1, MATRIX_3, MATRIX_4, MATRIX_1;
requirements HIDDEN;
equalities MATRIX_4;
expansions ;
theorem Th23:
for
n being
Nat for
K being
Field for
M1,
M2 being
Matrix of
n,
K holds
(M1 + M2) @ = (M1 @) + (M2 @)