let D be non empty set ; :: thesis: for i, j being 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 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 that
A1: p = A . i and
A2: ( 1 <= i & i <= len A ) and
A3: ( 1 <= j & j <= width A ) and
A4: len p = width A ; :: thesis: A * (i,j) = p . j
A5: j in Seg (width A) by A3;
then j in dom p by A4, FINSEQ_1:def 3;
then ( rng p c= D & p . j in rng p ) by FINSEQ_1:def 4, FUNCT_1:def 3;
then reconsider xp = p . j as Element of D ;
A6: xp = p . j ;
i in dom A by A2, FINSEQ_3:25;
then [i,j] in Indices A by A5, ZFMISC_1:87;
hence A * (i,j) = p . j by A1, A6, MATRIX_0:def 5; :: thesis: verum