scheme :: DTCONSTR:sch 1
DTConstrStrEx{ F₁() -> non empty set , P₁[ object , object ] } :

ex G being non empty strict DTConstrStr st
( the carrier of G = F₁() & ( for x being Symbol of G
for p being FinSequence of the carrier of G holds
( x ==> p iff P₁[x,p] ) ) )