:: deftheorem defines is_an_xrep_of PRGCOR_2:def 1 :
for D being non empty set
for p being XFinSequence of D
for q being FinSequence of D holds
( p is_an_xrep_of q iff ( NAT c= D & p . 0 = len q & len q < len p & ( for i being Nat st 1 <= i & i <= len q holds
p . i = q . i ) ) );