environ
vocabularies HIDDEN, NUMBERS, NAT_1, XBOOLE_0, FINSEQ_1, SUBSET_1, RELAT_1, CARD_1, FINSEQ_2, TARSKI, TREES_1, XXREAL_0, ZFMISC_1, FUNCT_1, QC_LANG1, INCSP_1, ARYTM_1, ARYTM_3, MATRIX_1, GOBRD13, CARD_3, FUNCT_6, FINSET_1, CARD_2, MATRIX_0, PARTFUN1, FUNCOP_1, FINSEQ_3;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, REAL_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, COMPLEX1, NAT_1, VALUED_0, RELAT_1, CARD_1, CARD_2, FUNCT_1, INT_1, PARTFUN1, FUNCT_2, FUNCOP_1, FINSET_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, CARD_3, FUNCT_6, BINOP_1, FINSEQOP;
definitions TARSKI, XBOOLE_0;
theorems FINSEQ_1, FINSEQ_2, FINSEQ_3, TARSKI, FUNCOP_1, FUNCT_1, FUNCT_2, ZFMISC_1, NAT_1, RELAT_1, ORDINAL1, CARD_1, CARD_2, XXREAL_0, CARD_3, FUNCT_6, FINSET_1, PARTFUN1, XBOOLE_0, XREAL_1, SEQM_3, INT_1;
schemes FINSEQ_1, BINOP_1, FINSEQ_2, FRAENKEL;
registrations XBOOLE_0, RELAT_1, FUNCT_1, XREAL_0, FINSEQ_1, FINSEQ_2, ORDINAL1, CARD_1, FINSET_1, PRE_POLY, XXREAL_0, NAT_1, INT_1;
constructors HIDDEN, BINOP_1, XXREAL_0, FINSEQOP, RELSET_1, FINSEQ_3, INT_1, CARD_3, FUNCT_6, CARD_2, WELLORD2, NAT_1, PRE_POLY, FINSEQ_4, XCMPLX_0, DOMAIN_1, REAL_1;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
equalities BINOP_1, FINSEQ_2, ORDINAL1, CARD_1;
expansions ;
definition
let D be non
empty set ;
let M be
Matrix of
D;
existence
ex b1 being Matrix of D st
( len b1 = width M & ( for i, j being Nat holds
( [i,j] in Indices b1 iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
b1 * (i,j) = M * (j,i) ) )
uniqueness
for b1, b2 being Matrix of D st len b1 = width M & ( for i, j being Nat holds
( [i,j] in Indices b1 iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
b1 * (i,j) = M * (j,i) ) & len b2 = width M & ( for i, j being Nat holds
( [i,j] in Indices b2 iff [j,i] in Indices M ) ) & ( for i, j being Nat st [j,i] in Indices M holds
b2 * (i,j) = M * (j,i) ) holds
b1 = b2
end;
theorem Th47:
for
x1,
x2,
y1,
y2 being
object holds
(
len ((x1,x2) ][ (y1,y2)) = 2 &
width ((x1,x2) ][ (y1,y2)) = 2 &
Indices ((x1,x2) ][ (y1,y2)) = [:(Seg 2),(Seg 2):] )
theorem Th48:
for
x1,
x2,
y1,
y2 being
object holds
(
[1,1] in Indices ((x1,x2) ][ (y1,y2)) &
[1,2] in Indices ((x1,x2) ][ (y1,y2)) &
[2,1] in Indices ((x1,x2) ][ (y1,y2)) &
[2,2] in Indices ((x1,x2) ][ (y1,y2)) )
theorem
for
D being non
empty set for
a,
b,
c,
d being
Element of
D holds
(
((a,b) ][ (c,d)) * (1,1)
= a &
((a,b) ][ (c,d)) * (1,2)
= b &
((a,b) ][ (c,d)) * (2,1)
= c &
((a,b) ][ (c,d)) * (2,2)
= d )
Lm1:
for D being non empty set
for M being Matrix of D
for k being Nat st k in dom M holds
M . k = Line (M,k)