theorem Th30: :: ABCMIZ_1:30

for l being one-to-one FinSequence of Vars holds
( l is quasi-loci iff for i being Nat
for x being variable st i in dom l & x = l . i holds
for y being variable st y in vars x holds
ex j being Nat st
( j in dom l & j < i & y = l . j ) )