let l be quasi-loci; :: thesis: for x being variable holds
( l ^ <*x*> is quasi-loci iff ( not x in rng l & vars x c= rng l ) )
let x be variable; :: thesis: ( l ^ <*x*> is quasi-loci iff ( not x in rng l & vars x c= rng l ) )
A1: (l ^ <*x*>) . (1 + (len l)) = x by FINSEQ_1:42;
A2: dom (l ^ <*x*>) = Seg ((len l) + (len <*x*>)) by FINSEQ_1:def 7
.= Seg ((len l) + 1) by FINSEQ_1:39 ;
1 <= 1 + (len l) by NAT_1:11;
then A3: 1 + (len l) in dom (l ^ <*x*>) by A2;
A4: dom l = Seg (len l) by FINSEQ_1:def 3;

hereby :: thesis: ( not x in rng l & vars x c= rng l implies l ^ <*x*> is quasi-loci )

assume A5: l ^ <*x*> is quasi-loci ; :: thesis: ( not x in rng l & vars x c= rng l )
thus not x in rng l :: thesis: vars x c= rng l

proof

assume x in rng l ; :: thesis: contradiction
then consider a being object such that
A6: a in dom l and
A7: x = l . a by FUNCT_1:def 3;
reconsider a = a as Element of NAT by A6;
A8: (l ^ <*x*>) . a = x by A6, A7, FINSEQ_1:def 7;
A9: a <= len l by A4, A6, FINSEQ_1:1;
A10: len l < 1 + (len l) by NAT_1:13;
dom l c= dom (l ^ <*x*>) by FINSEQ_1:26;
hence contradiction by A1, A3, A5, A6, A8, A9, A10, FUNCT_1:def 4; :: thesis: verum

end;

thus vars x c= rng l :: thesis: verum

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in vars x or a in rng l )
assume A11: a in vars x ; :: thesis: a in rng l
then reconsider a = a as variable ;
consider j being Nat such that
A12: j in dom (l ^ <*x*>) and
A13: j < 1 + (len l) and
A14: a = (l ^ <*x*>) . j by A1, A3, A5, A11, Th30;
reconsider j = j as Element of NAT by ORDINAL1:def 12;
A15: j <= len l by A13, NAT_1:13;
j >= 1 by A2, A12, FINSEQ_1:1;
then A16: j in dom l by A4, A15;
then a = l . j by A14, FINSEQ_1:def 7;
hence a in rng l by A16, FUNCT_1:def 3; :: thesis: verum

end;

end;

assume that
A17: not x in rng l and
A18: vars x c= rng l ; :: thesis: l ^ <*x*> is quasi-loci
A19: l ^ <*x*> is one-to-one

proof

let a, b be object ; :: according to FUNCT_1:def 4 :: thesis: ( not a in proj1 (l ^ <*x*>) or not b in proj1 (l ^ <*x*>) or not (l ^ <*x*>) . a = (l ^ <*x*>) . b or a = b )
assume that
A20: a in dom (l ^ <*x*>) and
A21: b in dom (l ^ <*x*>) and
A22: (l ^ <*x*>) . a = (l ^ <*x*>) . b ; :: thesis: a = b
reconsider a = a, b = b as Element of NAT by A20, A21;
A23: a >= 1 by A2, A20, FINSEQ_1:1;
A24: b >= 1 by A2, A21, FINSEQ_1:1;
A25: a <= 1 + (len l) by A2, A20, FINSEQ_1:1;
A26: b <= 1 + (len l) by A2, A21, FINSEQ_1:1;
A27: ( a <= len l or a = 1 + (len l) ) by A25, NAT_1:8;
A28: ( b <= len l or b = 1 + (len l) ) by A26, NAT_1:8;
A29: ( a in dom l or a = 1 + (len l) ) by A4, A23, A27;
A30: ( b in dom l or b = 1 + (len l) ) by A4, A24, A28;
A31: ( ( a in dom l & l . a = (l ^ <*x*>) . a & l . a in rng l ) or a = 1 + (len l) ) by A29, FINSEQ_1:def 7, FUNCT_1:def 3;
( ( b in dom l & l . b = (l ^ <*x*>) . b & l . b in rng l ) or b = 1 + (len l) ) by A30, FINSEQ_1:def 7, FUNCT_1:def 3;
hence a = b by A17, A22, A31, FINSEQ_1:42, FUNCT_1:def 4; :: thesis: verum

end;

now :: thesis: for i being Nat
for z being variable st i in dom (l ^ <*x*>) & z = (l ^ <*x*>) . i holds
for y being variable st y in vars z holds
ex j being Nat st
( j in dom (l ^ <*x*>) & j < i & y = (l ^ <*x*>) . j )

let i be Nat; :: thesis: for z being variable st i in dom (l ^ <*x*>) & z = (l ^ <*x*>) . i holds
for y being variable st y in vars z holds
ex j being Nat st
( j in dom (l ^ <*x*>) & j < i & y = (l ^ <*x*>) . j )
let z be variable; :: thesis: ( i in dom (l ^ <*x*>) & z = (l ^ <*x*>) . i implies for y being variable st y in vars z holds
ex j being Nat st
( j in dom (l ^ <*x*>) & j < i & y = (l ^ <*x*>) . j ) )
assume that
A32: i in dom (l ^ <*x*>) and
A33: z = (l ^ <*x*>) . i ; :: thesis: for y being variable st y in vars z holds
ex j being Nat st
( j in dom (l ^ <*x*>) & j < i & y = (l ^ <*x*>) . j )
A34: i >= 1 by A2, A32, FINSEQ_1:1;
i <= 1 + (len l) by A2, A32, FINSEQ_1:1;
then ( i <= len l or i = 1 + (len l) ) by NAT_1:8;
then A35: ( i in dom l or ( i = 1 + (len l) & z = x ) ) by A4, A33, A34, FINSEQ_1:42;
let y be variable; :: thesis: ( y in vars z implies ex j being Nat st
( j in dom (l ^ <*x*>) & j < i & y = (l ^ <*x*>) . j ) )
assume A36: y in vars z ; :: thesis: ex j being Nat st
( j in dom (l ^ <*x*>) & j < i & y = (l ^ <*x*>) . j )
thus ex j being Nat st
( j in dom (l ^ <*x*>) & j < i & y = (l ^ <*x*>) . j ) :: thesis: verum

proof

per cases ( ( i = 1 + (len l) & z = x ) or ( i in dom l & z = l . i ) ) by A33, A35, FINSEQ_1:def 7;

suppose A37: ( i = 1 + (len l) & z = x ) ; :: thesis: ex j being Nat st
( j in dom (l ^ <*x*>) & j < i & y = (l ^ <*x*>) . j )

then consider k being object such that
A38: k in dom l and
A39: y = l . k by A18, A36, FUNCT_1:def 3;
reconsider k = k as Element of NAT by A38;
take k ; :: thesis: ( k in dom (l ^ <*x*>) & k < i & y = (l ^ <*x*>) . k )
A40: dom l c= dom (l ^ <*x*>) by FINSEQ_1:26;
k <= len l by A4, A38, FINSEQ_1:1;
hence ( k in dom (l ^ <*x*>) & k < i & y = (l ^ <*x*>) . k ) by A37, A38, A39, A40, FINSEQ_1:def 7, NAT_1:13; :: thesis: verum

end;

suppose ( i in dom l & z = l . i ) ; :: thesis: ex j being Nat st
( j in dom (l ^ <*x*>) & j < i & y = (l ^ <*x*>) . j )

then consider j being Nat such that
A41: j in dom l and
A42: j < i and
A43: y = l . j by A36, Th30;
take j ; :: thesis: ( j in dom (l ^ <*x*>) & j < i & y = (l ^ <*x*>) . j )
dom l c= dom (l ^ <*x*>) by FINSEQ_1:26;
hence ( j in dom (l ^ <*x*>) & j < i & y = (l ^ <*x*>) . j ) by A41, A42, A43, FINSEQ_1:def 7; :: thesis: verum

end;

end;

end;

end;

hence l ^ <*x*> is quasi-loci by A19, Th30; :: thesis: verum