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

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