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