i in dom M by A1, ZFMISC_1:106;
then A2: M . i in rng M by FUNCT_1:def 5;
rng M c= D * by FINSEQ_1:def 4;
then reconsider p = M . i as FinSequence of D by A2, FINSEQ_1:def 11;
A3: j in Seg (width M) by A1, ZFMISC_1:106;
( M <> {} & len M >= 0 ) by A1, NAT_1:2, ZFMISC_1:106;
then len M > 0 by XXREAL_0:1;
then consider s being FinSequence such that
A4: s in rng M and
A5: len s = width M by Def4;
consider n being Nat such that
A6: for x being set st x in rng M holds
ex t being FinSequence st
( t = x & len t = n ) by Def1;
A7: ex v being FinSequence st
( p = v & len v = n ) by A2, A6;
ex t being FinSequence st
( s = t & len t = n ) by A4, A6;
then j in dom p by A3, A5, A7, FINSEQ_1:def 3;
then A8: p . j in rng p by FUNCT_1:def 5;
rng p c= D by FINSEQ_1:def 4;
then reconsider a = p . j as Element of D by A8;
take a ; :: thesis: ex p being FinSequence of D st
( p = M . i & a = p . j )
take p ; :: thesis: ( p = M . i & a = p . j )
thus ( p = M . i & a = p . j ) ; :: thesis: verum