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 that
A2: i in dom l and
A3: 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 A4: 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, A3, Def3;
then consider z being set such that
A5: z in dom (l dom i) and
A6: y = (l dom i) . z by A4, FUNCT_1:def 5;
A7: dom (l dom i) = (dom l) /\ i by RELAT_1:90;
then A8: z in i by A5, XBOOLE_0:def 4;
reconsider z = z as Element of NAT by A5, A7;
reconsider j = z as Nat ;
take j = j; :: thesis: ( j in dom l & j < i & y = l . j )
A9: card z = z by CARD_1:def 5;
card i = i by CARD_1:def 5;
hence ( j in dom l & j < i & y = l . j ) by A5, A6, A7, A8, A9, FUNCT_1:70, NAT_1:42, XBOOLE_0:def 4; :: thesis: verum

end;

assume A10: 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 A11: i in dom l ; :: thesis: (l . i) `1 c= rng (l dom i)
then l . i in rng l 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 A12: y in vars x ;
then reconsider y = y as variable ;
consider j being Nat such that
A13: j in dom l and
A14: j < i and
A15: y = l . j by A10, A11, A12;
A16: card i = i by CARD_1:def 5;
card j = j by CARD_1:def 5;
then j in i by A14, A16, NAT_1:42;
hence y in rng (l dom i) by A13, A15, FUNCT_1:73; :: thesis: verum

end;

end;

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