set X = { [t,p] where t is Element of T, p is FinSequence of D : len p = A . t } ;
{ [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
A1: a = [t,p] and
len p = A . t ;
p in D * by FINSEQ_1:def 11;
hence a in [:T,(D *):] by A1, ZFMISC_1:def 2; :: thesis: verum

end;

hence { [t,p] where t is Element of T, p is FinSequence of D : len p = A . t } is Subset of [:T,(D *):] ; :: thesis: verum