A2: ( i in dom M & j in Seg (width M) ) by A1, ZFMISC_1:106;
then A3: 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 A3, FINSEQ_1:def 11;
M <> {} by A1, ZFMISC_1:106;
then ( len M <> 0 & len M >= 0 ) by NAT_1:2;
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 t being FinSequence st
( s = t & len t = n ) by A4, A6;
ex v being FinSequence st
( p = v & len v = n ) by A3, A6;
then j in dom p by A2, A5, A7, FINSEQ_1:def 3;
then ( p . j in rng p & rng p c= D ) by FINSEQ_1:def 4, FUNCT_1:def 5;
then reconsider a = p . j as Element of D ;
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