take n = 0 ; :: according to MATRIX_0:def 1 :: thesis: for x being object st x in rng {} holds
ex s being FinSequence st
( s = x & len s = n )
let x be object ; :: thesis: ( x in rng {} implies ex s being FinSequence st
( s = x & len s = n ) )
assume x in rng {} ; :: thesis: ex s being FinSequence st
( s = x & len s = n )
hence ex t being FinSequence st
( t = x & len t = n ) ; :: thesis: verum