let D be non empty set ; :: thesis: for A being Matrix of 1,3,D holds A @ is 3,1 -size
let A be Matrix of 1,3,D; :: thesis: A @ is 3,1 -size
( 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

proof

let p be FinSequence of D; :: thesis: ( p in rng (A @) implies len p = 1 )
assume A7: p in rng (A @) ; :: thesis: len p = 1
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: verum

end;

hence A @ is 3,1 -size by A1, MATRIX_0:def 2; :: thesis: verum