:: deftheorem Def1 defines LocSeq AMISTD_3:def 1 :
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N
for M being Subset of NAT
for b₄ being Sequence of NAT holds
( b₄ = LocSeq (M,S) iff ( dom b₄ = card M & ( for m being set st m in card M holds
b₄ . m = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . m ) ) );