environ
vocabularies HIDDEN, NUMBERS, PRE_TOPC, EUCLID, FINSEQ_1, REAL_1, SUBSET_1, GOBOARD1, NAT_1, XBOOLE_0, CARD_1, ARYTM_3, XXREAL_0, TARSKI, ARYTM_1, RELAT_1, ORDINAL4, PARTFUN1, FUNCT_1, RLTOPSP1, TOPREAL1, MCART_1, MATRIX_1, INCSP_1, ZFMISC_1, TREES_1, ORDINAL2, COMPLEX1, STRUCT_0, GOBOARD2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, RELAT_1, FUNCT_1, PARTFUN1, FINSEQ_1, VALUED_0, STRUCT_0, PRE_TOPC, SEQ_4, MATRIX_0, MATRIX_1, RLTOPSP1, EUCLID, TOPREAL1, GOBOARD1, XXREAL_0;
definitions TARSKI, TOPREAL1, GOBOARD1, XBOOLE_0;
theorems TARSKI, NAT_1, ZFMISC_1, FUNCT_1, FINSEQ_1, ABSVALUE, SEQ_4, FINSEQ_2, MATRIX_0, EUCLID, TOPREAL1, TOPREAL3, GOBOARD1, FINSEQ_4, FINSEQ_3, PARTFUN2, INT_1, XBOOLE_0, XBOOLE_1, XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1, PARTFUN1, SEQM_3, RLTOPSP1;
schemes NAT_1, MATRIX_0, FINSEQ_4;
registrations RELSET_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, STRUCT_0, EUCLID, VALUED_0, CARD_1, SEQM_3, SEQ_4, INT_1, ORDINAL1;
constructors HIDDEN, PARTFUN1, SQUARE_1, NAT_1, COMPLEX1, SEQ_4, TOPREAL1, GOBOARD1, XXREAL_2, SEQM_3, RELSET_1, DOMAIN_1, BINOP_2, RVSUM_1, REAL_1;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities TOPREAL1, XBOOLE_0;
expansions TOPREAL1, GOBOARD1, XBOOLE_0;
definition
let v1,
v2 be
FinSequence of
REAL ;
assume A1:
v1 <> {}
;
existence
ex b1 being Matrix of (TOP-REAL 2) st
( len b1 = len v1 & width b1 = len v2 & ( for n, m being Nat st [n,m] in Indices b1 holds
b1 * (n,m) = |[(v1 . n),(v2 . m)]| ) )
uniqueness
for b1, b2 being Matrix of (TOP-REAL 2) st len b1 = len v1 & width b1 = len v2 & ( for n, m being Nat st [n,m] in Indices b1 holds
b1 * (n,m) = |[(v1 . n),(v2 . m)]| ) & len b2 = len v1 & width b2 = len v2 & ( for n, m being Nat st [n,m] in Indices b2 holds
b2 * (n,m) = |[(v1 . n),(v2 . m)]| ) holds
b1 = b2
end;