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
take n = 1; :: 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 = n )
let x be object ; :: thesis: ( x in rng <*<*d*>*> implies ex s being FinSequence st
( s = x & len s = n ) )
assume A1: x in rng <*<*d*>*> ; :: thesis: ex s being FinSequence st
( s = x & len s = n )
A2: len <*d*> = n by FINSEQ_1:39;
rng <*<*d*>*> = {<*d*>} by FINSEQ_1:38;
then x = <*d*> by A1, TARSKI:def 1;
hence ex s being FinSequence st
( s = x & len s = n ) by A2; :: thesis: verum