let i be Nat; :: thesis: ex l being quasi-loci st len l = i
defpred S₁[ Nat] means ex l being quasi-loci st len l = $1;
( <*> Vars is quasi-loci & len (<*> Vars) = 0 ) by ABCMIZ_1:29;
then A1: S₁[ 0 ] ;
A2: for j being Nat st S₁[j] holds
S₁[j + 1]

proof

let j be Nat; :: thesis: ( S₁[j] implies S₁[j + 1] )
given l being quasi-loci such that A3: len l = j ; :: thesis: S₁[j + 1]
reconsider l1 = l ^ <*[(rng l),1]*> as quasi-loci by Th29;
take l1 ; :: thesis: len l1 = j + 1
thus len l1 = j + 1 by A3, FINSEQ_2:16; :: thesis: verum

end;

for j being Nat holds S₁[j] from NAT_1:sch 2(A1, A2);
hence ex l being quasi-loci st len l = i ; :: thesis: verum