set C = MaxConstrSign ;
let n be Nat; :: thesis:
let s be SortSymbol of MaxConstrSign; :: thesis:
deffunc H₁( Nat) -> object = [{},$1];
consider l being FinSequence such that
A1: len l = n and
A2: for i being Nat st i in dom l holds
l . i = H₁(i) from FINSEQ_1:sch 2();
A3: l is one-to-one

let i, j be object ; :: according to FUNCT_1:def 4 :: thesis:
assume A4: ( i in dom l & j in dom l & l . i = l . j ) ; :: thesis:
reconsider i = i, j = j as Nat by A4;
( l . i = H₁(i) & l . i = H₁(j) ) by A2, A4;
then i = H₁(j) `2 ;
hence i = j ; :: thesis:

end;

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in rng l ; :: thesis:
then consider a being object such that
A5: ( a in dom l & z = l . a ) by FUNCT_1:def 3;
reconsider a = a as Nat by A5;
z = H₁(a) by A2, A5;
hence z in Vars by ABCMIZ_1:25; :: thesis:

end;

then reconsider l = l as one-to-one FinSequence of Vars by A3, FINSEQ_1:def 4;
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; :: thesis:
let x be variable; :: thesis:
assume ( i in dom l & x = l . i ) ; :: thesis:
then x = H₁(i) by A2;
hence for y being variable st y in vars x holds
ex j being Nat st
( j in dom l & j < i & y = l . j ) ; :: thesis:

end;