set X = { [t,p] where t is Element of T, p is FinSequence of D : len p = A . t } ;
A1: { [t,p] where t is Element of T, p is FinSequence of D : len p = A . t } c= [:T,(D *):]

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { [t,p] where t is Element of T, p is FinSequence of D : len p = A . t } or a in [:T,(D *):] )
assume a in { [t,p] where t is Element of T, p is FinSequence of D : len p = A . t } ; :: thesis: a in [:T,(D *):]
then consider t being Element of T, p being FinSequence of D such that
A2: a = [t,p] and
len p = A . t ;
p in D * by FINSEQ_1:def 11;
hence a in [:T,(D *):] by A2, ZFMISC_1:def 2; :: thesis: verum

end;

consider a being object such that
A4: ( a in T & A . a = 0 ) by Def18;
reconsider t = a as Element of T by A4;
consider p being FinSequence of D such that
A5: len p = A . t by FINSEQ_1:19;
[t,p] in { [t,p] where t is Element of T, p is FinSequence of D : len p = A . t } by A5;
hence { [t,p] where t is Element of T, p is FinSequence of D : len p = A . t } is non empty Subset of [:T,(D *):] by A1; :: thesis: verum