let l be one-to-one FinSequence of Vars ; :: thesis: ( 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 ) )

hereby :: thesis: ( ( 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 ) ) implies l is quasi-loci )

assume A1: l is quasi-loci ; :: thesis: 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 )
let i be Nat; :: thesis: 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 )
let x be variable; :: thesis: ( i in dom l & x = l . i implies for y being variable st y in vars x holds
ex j being Nat st
( j in dom l & j < i & y = l . j ) )
assume A2: ( i in dom l & x = l . i ) ; :: thesis: for y being variable st y in vars x holds
ex j being Nat st
( j in dom l & j < i & y = l . j )
let y be variable; :: thesis: ( y in vars x implies ex j being Nat st
( j in dom l & j < i & y = l . j ) )
assume A3: y in vars x ; :: thesis: ex j being Nat st
( j in dom l & j < i & y = l . j )
vars x c= rng (l | i) by A1, A2, QuasiLociDef;
then consider z being set such that
A4: ( z in dom (l dom i) & y = (l dom i) . z ) by A3, FUNCT_1:def 5;
dom (l dom i) = (dom l) /\ i by RELAT_1:90;
then A5: ( z in dom l & z in i ) by A4, XBOOLE_0:def 4;
then reconsider z = z as Element of NAT ;
reconsider j = z as Nat ;
take j = j; :: thesis: ( j in dom l & j < i & y = l . j )
( card z = z & card i = i ) by CARD_1:def 5;
hence ( j in dom l & j < i & y = l . j ) by A4, A5, FUNCT_1:70, NAT_1:42; :: thesis: verum

end;

assume A6: 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 ) ; :: thesis: l is quasi-loci

now

let i be Nat; :: thesis: ( i in dom l implies (l . i) `1 c= rng (l dom i) )
assume A8: i in dom l ; :: thesis: (l . i) `1 c= rng (l dom i)
then ( l . i in rng l & rng l c= Vars ) by FUNCT_1:def 5;
then reconsider x = l . i as variable ;
thus (l . i) `1 c= rng (l dom i) :: thesis: verum

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in (l . i) `1 or y in rng (l dom i) )
assume y in (l . i) `1 ; :: thesis: y in rng (l dom i)
then A7: y in vars x ;
then reconsider y = y as variable ;
consider j being Nat such that
A9: ( j in dom l & j < i & y = l . j ) by A6, A7, A8;
( card i = i & card j = j ) by CARD_1:def 5;
then j in i by A9, NAT_1:42;
hence y in rng (l dom i) by A9, FUNCT_1:73; :: thesis: verum

end;

end;

hence l is quasi-loci by QuasiLociDef; :: thesis: verum