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:59;
A2: dom (l ^ <*x*>) = Seg ((len l) + (len <*x*>)) by FINSEQ_1:def 7
.= Seg ((len l) + 1) by FINSEQ_1:56 ;
( 1 <= 1 + (len l) & 1 + (len l) <= 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 B1: 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 set such that
B2: ( a in dom l & x = l . a ) by FUNCT_1:def 5;
reconsider a = a as Element of NAT by B2;
B3: (l ^ <*x*>) . a = x by B2, FINSEQ_1:def 7;
( a <= len l & len l < 1 + (len l) & dom l c= dom (l ^ <*x*>) ) by A4, B2, FINSEQ_1:3, FINSEQ_1:39, NAT_1:13;
hence contradiction by A1, A3, B1, B3, B2, FUNCT_1:def 8; :: thesis: verum

end;

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

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in vars x or a in rng l )
assume C1: a in vars x ; :: thesis: a in rng l
then reconsider a = a as variable ;
consider j being Nat such that
C2: ( j in dom (l ^ <*x*>) & j < 1 + (len l) & a = (l ^ <*x*>) . j ) by A1, A3, B1, C1, Th32;
reconsider j = j as Element of NAT by ORDINAL1:def 13;
( j <= len l & j >= 1 ) by A2, C2, FINSEQ_1:3, NAT_1:13;
then C3: j in dom l by A4;
then a = l . j by C2, FINSEQ_1:def 7;
hence a in rng l by C3, FUNCT_1:def 5; :: thesis: verum

end;

end;

assume D1: ( not x in rng l & vars x c= rng l ) ; :: thesis: l ^ <*x*> is quasi-loci
EE: l ^ <*x*> is one-to-one

proof

let a, b be set ; :: according to FUNCT_1:def 8 :: thesis: ( not a in dom (l ^ <*x*>) or not b in dom (l ^ <*x*>) or not (l ^ <*x*>) . a = (l ^ <*x*>) . b or a = b )
assume E1: ( a in dom (l ^ <*x*>) & b in dom (l ^ <*x*>) & (l ^ <*x*>) . a = (l ^ <*x*>) . b ) ; :: thesis: a = b
then reconsider a = a, b = b as Element of NAT ;
E2: ( a >= 1 & b >= 1 & a <= 1 + (len l) & b <= 1 + (len l) ) by A2, E1, FINSEQ_1:3;
then ( ( a <= len l or a = 1 + (len l) ) & ( b <= len l or b = 1 + (len l) ) ) by NAT_1:8;
then ( ( a in dom l or a = 1 + (len l) ) & ( b in dom l or b = 1 + (len l) ) ) by A4, E2;
then ( ( ( a in dom l & l . a = (l ^ <*x*>) . a & l . a in rng l ) or a = 1 + (len l) ) & ( ( b in dom l & l . b = (l ^ <*x*>) . b & l . b in rng l ) or b = 1 + (len l) ) ) by FINSEQ_1:def 7, FUNCT_1:def 5;
hence a = b by D1, E1, FINSEQ_1:59, FUNCT_1:def 8; :: thesis: verum

end;

now

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 D2: ( i in dom (l ^ <*x*>) & 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 )
then D3: ( i >= 1 & i <= 1 + (len l) & i is Element of NAT ) by A2, FINSEQ_1:3;
then ( i <= len l or i = 1 + (len l) ) by NAT_1:8;
then D9: ( i in dom l or ( i = 1 + (len l) & z = x ) ) by A4, D2, D3, FINSEQ_1:59;
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 D5: 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 D9, D2, FINSEQ_1:def 7;

suppose D8: ( 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 set such that
D6: ( k in dom l & y = l . k ) by D1, D5, FUNCT_1:def 5;
reconsider k = k as Element of NAT by D6;
take k ; :: thesis: ( k in dom (l ^ <*x*>) & k < i & y = (l ^ <*x*>) . k )
( dom l c= dom (l ^ <*x*>) & k <= len l ) by A4, D6, FINSEQ_1:3, FINSEQ_1:39;
hence ( k in dom (l ^ <*x*>) & k < i & y = (l ^ <*x*>) . k ) by D6, D8, 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
D7: ( j in dom l & j < i & y = l . j ) by D5, Th32;
take j ; :: thesis: ( j in dom (l ^ <*x*>) & j < i & y = (l ^ <*x*>) . j )
( dom l c= dom (l ^ <*x*>) & j is Element of NAT ) by FINSEQ_1:39, ORDINAL1:def 13;
hence ( j in dom (l ^ <*x*>) & j < i & y = (l ^ <*x*>) . j ) by D7, FINSEQ_1:def 7; :: thesis: verum

end;

end;

end;

end;

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