let D be non empty set ; 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; 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; 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; ( 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
; 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; verum