let m be Nat; ( 0 < m implies for M being Matrix of m,1,F_Real holds M is FinSequence of 1 -tuples_on REAL )
assume A0:
0 < m
; for M being Matrix of m,1,F_Real holds M is FinSequence of 1 -tuples_on REAL
let M be Matrix of m,1,F_Real; M is FinSequence of 1 -tuples_on REAL
A1:
len M = m
by A0, MATRIX_0:23;
width M = 1
by A0, MATRIX_0:23;
then consider s being FinSequence such that
A2:
s in rng M
and
A3:
len s = 1
by A0, A1, MATRIX_0:def 3;
consider n being Nat such that
A4:
for x being object st x in rng M holds
ex s being FinSequence st
( s = x & len s = n )
by MATRIX_0:def 1;
consider s1 being FinSequence such that
A5:
s1 = s
and
A6:
len s1 = n
by A4, A2;
rng M c= 1 -tuples_on REAL
hence
M is FinSequence of 1 -tuples_on REAL
by FINSEQ_1:def 4; verum