let D be non empty set ; :: thesis: for n being Nat
for A being Matrix of n,D
for p being FinSequence of D
for i being Nat st p = A . i & i in Seg n holds
len p = n
let n be Nat; :: thesis: for A being Matrix of n,D
for p being FinSequence of D
for i being Nat 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 Nat st p = A . i & i in Seg n holds
len p = n
let p be FinSequence of D; :: thesis: for i being Nat st p = A . i & i in Seg n holds
len p = n
let i be Nat; :: thesis: ( p = A . i & i in Seg n implies len p = n )
assume that
A1: p = A . i and
A2: i in Seg n ; :: thesis: len p = n
consider n2 being Nat such that
A3: for x being object st x in rng A holds
ex s being FinSequence of D st
( s = x & len s = n2 ) by MATRIX_0:9;
len A = n by MATRIX_0:24;
then A4: i in dom A by A2, FINSEQ_1:def 3;
then A . i in rng A by FUNCT_1:def 3;
then consider s being FinSequence of D such that
A5: s = A . i and
len s = n2 by A3;
s in rng A by A4, A5, FUNCT_1:def 3;
hence len p = n by A1, A5, MATRIX_0:def 2; :: thesis: verum