let D be non empty set ; :: thesis:
let A be Matrix of 1,3,D; :: thesis:
( width A = 3 & len A = 1 ) by MATRIX_0:23;
then A1: ( len (A @) = 3 & width (A @) = 1 ) by MATRIX_0:29;
then consider s1 being FinSequence such that
A2: s1 in rng (A @) and
A3: len s1 = 1 by MATRIX_0:def 3;
consider n0 being Nat such that
A4: for x being object st x in rng (A @) holds
ex s being FinSequence st
( s = x & len s = n0 ) by MATRIX_0:def 1;
consider s being FinSequence such that
A5: s = s1 and
A6: len s = n0 by A2, A4;
for p being FinSequence of D st p in rng (A @) holds
len p = 1

let p be FinSequence of D; :: thesis:
assume A7: p in rng (A @) ; :: thesis:
consider s being FinSequence such that
A8: s = p and
A9: len s = n0 by A7, A4;
thus len p = 1 by A3, A5, A6, A8, A9; :: thesis:

end;