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:50, FINSEQ_3:98;

now

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 A3: ( i in dom p & 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 A4: y in vars x ; :: thesis: ex j being Nat st
( j in dom p & j < i & y = p . j )
dom p c= dom (p ^ q) by FINSEQ_1:39;
then ( i in dom (p ^ q) & x = (p ^ q) . i ) by A3, FINSEQ_1:def 7;
then consider j being Nat such that
A5: ( j in dom (p ^ q) & j < i & y = (p ^ q) . j ) by A1, A4, Th32;
take j = j; :: thesis: ( j in dom p & j < i & y = p . j )
A6: ( dom p = Seg (len p) & dom (p ^ q) = Seg (len (p ^ q)) ) by FINSEQ_1:def 3;
then A7: ( j >= 1 & i <= len p ) by A3, A5, FINSEQ_1:3;
then j < len p by A5, XXREAL_0:2;
hence ( j in dom p & j < i ) by A5, A6, A7; :: thesis: y = p . j
hence y = p . j by A5, FINSEQ_1:def 7; :: thesis: verum

end;

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