let l be one-to-one FinSequence of Vars ; ( 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 ( ( 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
;
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;
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;
( 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
;
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;
( 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
;
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;
( 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;
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 )
; l is quasi-loci
hence
l is quasi-loci
by Def3; verum