take M = {} ; :: thesis: M is tabular
take 0 ; :: according to MATRIX_1:def 1 :: thesis: for x being set st x in rng M holds
ex s being FinSequence st
( s = x & len s = 0 )
let x be set ; :: thesis: ( x in rng M implies ex s being FinSequence st
( s = x & len s = 0 ) )
assume x in rng M ; :: thesis: ex s being FinSequence st
( s = x & len s = 0 )
hence ex s being FinSequence st
( s = x & len s = 0 ) ; :: thesis: verum