let E be set ; :: thesis: for a being Element of E ^omega holds a in (Lex E) |^ (len a)
let a be Element of E ^omega ; :: thesis: a in (Lex E) |^ (len a)
defpred S₁[ Nat] means for a being Element of E ^omega st len a = $1 holds
a in (Lex E) |^ $1;

A1: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]

now :: thesis: for b being Element of E ^omega st len b = n + 1 holds
b in (Lex E) |^ (n + 1)

let b be Element of E ^omega ; :: thesis: ( len b = n + 1 implies b in (Lex E) |^ (n + 1) )
assume len b = n + 1 ; :: thesis: b in (Lex E) |^ (n + 1)
then consider c being Element of E ^omega , e being Element of E such that
A3: len c = n and
A4: b = c ^ <%e%> by Th7;
<%e%> is Element of E ^omega by A4, Th5;
then e in E by Th6;
then <%e%> in Lex E by Def4;
then A5: <%e%> in (Lex E) |^ 1 by Th25;
c in (Lex E) |^ n by A2, A3;
hence b in (Lex E) |^ (n + 1) by A4, A5, Th40; :: thesis: verum

end;

hence S₁[n + 1] ; :: thesis: verum

end;

A6: S₁[ 0 ]

proof

let a be Element of E ^omega ; :: thesis: ( len a = 0 implies a in (Lex E) |^ 0 )
assume len a = 0 ; :: thesis: a in (Lex E) |^ 0
then a = <%> E ;
then a in {(<%> E)} by TARSKI:def 1;
hence a in (Lex E) |^ 0 by Th24; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A6, A1);
hence a in (Lex E) |^ (len a) ; :: thesis: verum