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