let X be finite Subset of Vars ; :: thesis: ex l being quasi-loci st rng l = varcl X
reconsider Y = varcl X as finite Subset of Vars by ABCMIZ_1:24;
defpred S₁[ set , set ] means $1 in $2 `1 ;
P1: for x, y being set st x in Y & y in Y & S₁[x,y] holds
not S₁[y,x]

proof

let x, y be set ; :: thesis: ( x in Y & y in Y & S₁[x,y] implies not S₁[y,x] )
assume Z0: ( x in Y & y in Y & S₁[x,y] & S₁[y,x] ) ; :: thesis: contradiction
x in Vars by Z0;
then consider A being Subset of Vars , j being Element of NAT such that
Z1: ( x = [(varcl A),j] & A is finite ) by ABCMIZ_1:18;
y in Vars by Z0;
then consider B being Subset of Vars , k being Element of NAT such that
Z2: ( y = [(varcl B),k] & B is finite ) by ABCMIZ_1:18;
C1: ( y in varcl A & x in varcl B ) by Z0, Z1, Z2, MCART_1:7;
C2: ( varcl A in {(varcl A)} & varcl B in {(varcl B)} ) by TARSKI:def 1;
( {(varcl A)} in x & {(varcl B)} in y ) by TARSKI:def 2, Z2, Z1;
hence contradiction by C1, C2, ORDINAL1:6; :: thesis: verum

end;

P2: for x, y, z being set st x in Y & y in Y & z in Y & S₁[x,y] & S₁[y,z] holds
S₁[x,z]

proof

let x, y, z be set ; :: thesis: ( x in Y & y in Y & z in Y & S₁[x,y] & S₁[y,z] implies S₁[x,z] )
assume Z0: ( x in Y & y in Y & z in Y & S₁[x,y] & S₁[y,z] ) ; :: thesis: S₁[x,z]
y in Vars by Z0;
then consider B being Subset of Vars , k being Element of NAT such that
Z2: ( y = [(varcl B),k] & B is finite ) by ABCMIZ_1:18;
z in Vars by Z0;
then consider C being Subset of Vars , j being Element of NAT such that
Z3: ( z = [(varcl C),j] & C is finite ) by ABCMIZ_1:18;
D0: ( z `1 = varcl C & y `1 = varcl B ) by Z3, Z2, MCART_1:7;
then varcl B c= varcl C by Z0, Z2, ABCMIZ_1:def 1;
hence S₁[x,z] by D0, Z0; :: thesis: verum

end;

consider l being one-to-one FinSequence such that
A1: rng l = Y and
A2: for i, j being Nat st i in dom l & j in dom l & S₁[l . i,l . j] holds
i < j from ABCMIZ_A:sch 3(P1, P2);
reconsider l = l as one-to-one FinSequence of Vars by A1, FINSEQ_1:def 4;

now

let i be Nat; :: thesis: for x being variable st i in dom l & x = l . i holds
for y being variable st y in vars x holds
ex a being Nat st
( a in dom l & a < i & y = l . a )
let x be variable; :: thesis: ( i in dom l & x = l . i implies for y being variable st y in vars x holds
ex a being Nat st
( a in dom l & a < i & y = l . a ) )
assume B1: ( i in dom l & x = l . i ) ; :: thesis: for y being variable st y in vars x holds
ex a being Nat st
( a in dom l & a < i & y = l . a )
let y be variable; :: thesis: ( y in vars x implies ex a being Nat st
( a in dom l & a < i & y = l . a ) )
assume B2: y in vars x ; :: thesis: ex a being Nat st
( a in dom l & a < i & y = l . a )
x in Vars ;
then consider A being Subset of Vars , j being Element of NAT such that
Z1: ( x = [(varcl A),j] & A is finite ) by ABCMIZ_1:18;
( x in rng l & vars x = varcl A ) by B1, Z1, MCART_1:7, FUNCT_1:def 5;
then vars x c= Y by A1, Z1, ABCMIZ_1:def 1;
then consider a being set such that
B3: ( a in dom l & y = l . a ) by A1, B2, FUNCT_1:def 5;
reconsider a = a as Nat by B3;
take a = a; :: thesis: ( a in dom l & a < i & y = l . a )
thus ( a in dom l & a < i & y = l . a ) by A2, B1, B2, B3; :: thesis: verum

end;

then reconsider l = l as quasi-loci by ABCMIZ_1:30;
take l ; :: thesis: rng l = varcl X
thus rng l = varcl X by A1; :: thesis: verum