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 object such that
A5: z in dom (l dom i) and
A6: y = (l dom i) . z by A4, FUNCT_1:def 3;
A7: dom (l dom i) = (dom l) /\ i by RELAT_1:61;
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 )
A8: card (Segm z) = z ;
card (Segm i) = i ;
hence ( j in dom l & j < i & y = l . j ) by A5, A6, A7, A8, FUNCT_1:47, NAT_1:41, XBOOLE_0:def 4; :: thesis: verum

end;

assume A9: 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 :: thesis: for i being Nat st i in dom l holds
(l . i) `1 c= rng (l dom i)

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

proof

let y be object ; :: 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 A11: y in vars x ;
then reconsider y = y as variable ;
consider j being Nat such that
A12: j in dom l and
A13: j < i and
A14: y = l . j by A9, A10, A11;
A15: card (Segm i) = i ;
card (Segm j) = j ;
then j in i by A13, A15, NAT_1:41;
hence y in rng (l dom i) by A12, A14, FUNCT_1:50; :: thesis: verum

end;

end;

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