let m be Nat; :: thesis: ( 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 ; :: thesis: 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; :: thesis: 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
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng M or x in 1 -tuples_on REAL )
assume A7: x in rng M ; :: thesis: x in 1 -tuples_on REAL
then consider s being FinSequence such that
A8: s = x and
A9: len s = n by A4;
consider n0 being Nat such that
A10: for x being object st x in rng M holds
ex p being FinSequence of F_Real st
( x = p & len p = n0 ) by MATRIX_0:9;
consider p being FinSequence of F_Real such that
A11: x = p and
len p = n0 by A10, A7;
rng p c= REAL ;
hence x in 1 -tuples_on REAL by A11, A8, A9, A5, A6, A3, FINSEQ_2:132; :: thesis: verum
end;
hence M is FinSequence of 1 -tuples_on REAL by FINSEQ_1:def 4; :: thesis: verum