let p, q be FinSequence; ( p ^ q is quasi-loci implies ( p is quasi-loci & q is FinSequence of Vars ) )
assume A1:
p ^ q is quasi-loci
; ( 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 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;
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;
( 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
;
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;
( 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
;
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;
( 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;
y = p . jhence
y = p . j
by A9, FINSEQ_1:def 7;
verum end;
hence
( p is quasi-loci & q is FinSequence of Vars )
by A1, A2, Th30, FINSEQ_1:36; verum