let D be non empty set ; :: thesis: for i, j being Element of NAT
for A being Matrix of D
for p being FinSequence of D st p = A . i & 1 <= i & i <= len A & 1 <= j & j <= width A & len p = width A holds
A * i,j = p . j
let i, j be Element of NAT ; :: thesis: for A being Matrix of D
for p being FinSequence of D st p = A . i & 1 <= i & i <= len A & 1 <= j & j <= width A & len p = width A holds
A * i,j = p . j
let A be Matrix of D; :: thesis: for p being FinSequence of D st p = A . i & 1 <= i & i <= len A & 1 <= j & j <= width A & len p = width A holds
A * i,j = p . j
let p be FinSequence of D; :: thesis: ( p = A . i & 1 <= i & i <= len A & 1 <= j & j <= width A & len p = width A implies A * i,j = p . j )
assume A1: ( p = A . i & 1 <= i & i <= len A & 1 <= j & j <= width A & len p = width A ) ; :: thesis: A * i,j = p . j
then A2: i in dom A by FINSEQ_3:27;
A3: j in Seg (width A) by A1;
then A4: [i,j] in Indices A by A2, ZFMISC_1:106;
A5: rng p c= D by FINSEQ_1:def 4;
j in dom p by A1, A3, FINSEQ_1:def 3;
then p . j in rng p by FUNCT_1:def 5;
then reconsider xp = p . j as Element of D by A5;
( p = A . i & xp = p . j ) by A1;
hence A * i,j = p . j by A4, MATRIX_1:def 6; :: thesis: verum