for D being non empty set
for p being XFinSequence of D st NAT c= D & p . 0 is Nat & p . 0 in dom p holds
p is_an_xrep_of XFS2FS* p