let s be FinSequence; :: thesis: <*s*> is tabular
take len s ; :: according to MATRIX_0:def 1 :: thesis: for x being object st x in rng <*s*> holds
ex s being FinSequence st
( s = x & len s = len s )
let x be object ; :: thesis: ( x in rng <*s*> implies ex s being FinSequence st
( s = x & len s = len s ) )
assume x in rng <*s*> ; :: thesis: ex s being FinSequence st
( s = x & len s = len s )
then A1: x in {s} by FINSEQ_1:38;
then reconsider t = x as FinSequence by TARSKI:def 1;
take t ; :: thesis: ( t = x & len t = len s )
thus ( t = x & len t = len s ) by A1, TARSKI:def 1; :: thesis: verum