let D be non empty set ; :: thesis: for d being Element of D holds <*<*d*>*> is tabular
let d be Element of D; :: thesis: <*<*d*>*> is tabular
A1: rng <*<*d*>*> = {<*d*>} by FINSEQ_1:55;
take n = 1; :: 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 = n )
let x be set ; :: thesis: ( x in rng <*<*d*>*> implies ex s being FinSequence st
( s = x & len s = n ) )
assume x in rng <*<*d*>*> ; :: thesis: ex s being FinSequence st
( s = x & len s = n )
then ( x = <*d*> & len <*d*> = n ) by A1, FINSEQ_1:56, TARSKI:def 1;
hence ex s being FinSequence st
( s = x & len s = n ) ; :: thesis: verum