take <*> (D * ) ; :: thesis: <*> (D * ) is tabular
take 0 ; :: according to MATRIX_1:def 1 :: thesis: for x being set st x in rng (<*> (D * )) holds
ex s being FinSequence st
( s = x & len s = 0 )
thus for x being set st x in rng (<*> (D * )) holds
ex s being FinSequence st
( s = x & len s = 0 ) ; :: thesis: verum