let D be non empty set ; :: thesis: for n being Element of NAT
for A being Matrix of n,D
for p being FinSequence of D
for i being natural number st p = A . i & i in Seg n holds
len p = n
let n be Element of NAT ; :: thesis: for A being Matrix of n,D
for p being FinSequence of D
for i being natural number st p = A . i & i in Seg n holds
len p = n
let A be Matrix of n,D; :: thesis: for p being FinSequence of D
for i being natural number st p = A . i & i in Seg n holds
len p = n
let p be FinSequence of D; :: thesis: for i being natural number st p = A . i & i in Seg n holds
len p = n
let i be natural number ; :: thesis: ( p = A . i & i in Seg n implies len p = n )
assume A1: ( p = A . i & i in Seg n ) ; :: thesis: len p = n
consider n2 being Nat such that
A2: for x being set st x in rng A holds
ex s being FinSequence of D st
( s = x & len s = n2 ) by MATRIX_1:9;
( len A = n & width A = n ) by MATRIX_1:25;
then A3: i in dom A by A1, FINSEQ_1:def 3;
then A . i in rng A by FUNCT_1:def 5;
then consider s being FinSequence of D such that
A4: ( s = A . i & len s = n2 ) by A2;
s in rng A by A3, A4, FUNCT_1:def 5;
hence len p = n by A1, A4, MATRIX_1:def 3; :: thesis: verum