let p, q be FinSequence; :: thesis: ( p ^ q is quasi-loci implies ( p is quasi-loci & q is FinSequence of Vars ) )
assume A1: p ^ q is quasi-loci ; :: thesis: ( p is quasi-loci & q is FinSequence of Vars )
then A2: p is one-to-one FinSequence of Vars by FINSEQ_1:36, FINSEQ_3:91;

now :: thesis: for i being Nat
for x being variable st i in dom p & x = p . i holds
for y being variable st y in vars x holds
ex j being Nat st
( j in dom p & j < i & y = p . j )

let i be Nat; :: thesis: for x being variable st i in dom p & x = p . i holds
for y being variable st y in vars x holds
ex j being Nat st
( j in dom p & j < i & y = p . j )
let x be variable; :: thesis: ( i in dom p & x = p . i implies for y being variable st y in vars x holds
ex j being Nat st
( j in dom p & j < i & y = p . j ) )
assume that
A3: i in dom p and
A4: x = p . i ; :: thesis: for y being variable st y in vars x holds
ex j being Nat st
( j in dom p & j < i & y = p . j )
let y be variable; :: thesis: ( y in vars x implies ex j being Nat st
( j in dom p & j < i & y = p . j ) )
assume A5: y in vars x ; :: thesis: ex j being Nat st
( j in dom p & j < i & y = p . j )
A6: dom p c= dom (p ^ q) by FINSEQ_1:26;
x = (p ^ q) . i by A3, A4, FINSEQ_1:def 7;
then consider j being Nat such that
A7: j in dom (p ^ q) and
A8: j < i and
A9: y = (p ^ q) . j by A1, A3, A5, A6, Th30;
take j = j; :: thesis: ( j in dom p & j < i & y = p . j )
A10: dom p = Seg (len p) by FINSEQ_1:def 3;
dom (p ^ q) = Seg (len (p ^ q)) by FINSEQ_1:def 3;
then A11: j >= 1 by A7, FINSEQ_1:1;
i <= len p by A3, A10, FINSEQ_1:1;
then j < len p by A8, XXREAL_0:2;
hence ( j in dom p & j < i ) by A8, A10, A11; :: thesis: y = p . j
hence y = p . j by A9, FINSEQ_1:def 7; :: thesis: verum

end;

hence ( p is quasi-loci & q is FinSequence of Vars ) by A1, A2, Th30, FINSEQ_1:36; :: thesis: verum