for G being non empty DTConstrStr
for s being Element of G
for p being FinSequence st s ==> p holds
p is FinSequence of the carrier of G