defpred S₁[ non empty Ordinal] means for b being Ordinal st omega -exponent $1 in omega -exponent b holds
$1 in exp (omega,(omega -exponent b));
A1: for c being Ordinal
for n being non zero Nat holds S₁[n *^ (exp (omega,c))]

proof

let c be Ordinal; :: thesis: for n being non zero Nat holds S₁[n *^ (exp (omega,c))]
let n be non zero Nat; :: thesis: S₁[n *^ (exp (omega,c))]
let b be Ordinal; :: thesis: ( omega -exponent (n *^ (exp (omega,c))) in omega -exponent b implies n *^ (exp (omega,c)) in exp (omega,(omega -exponent b)) )
assume A2: omega -exponent (n *^ (exp (omega,c))) in omega -exponent b ; :: thesis: n *^ (exp (omega,c)) in exp (omega,(omega -exponent b))
( 0 in n & n in omega ) by XBOOLE_1:61, ORDINAL1:11, ORDINAL1:def 12;
then c in omega -exponent b by A2, ORDINAL5:58;
then exp (omega,c) in exp (omega,(omega -exponent b)) by ORDINAL4:24;
hence n *^ (exp (omega,c)) in exp (omega,(omega -exponent b)) by Th42; :: thesis: verum

end;

A3: for c being Ordinal
for d being non empty Ordinal
for n being non zero Nat st S₁[d] & not c in rng (omega -exponent (CantorNF d)) holds
S₁[d (+) (n *^ (exp (omega,c)))]

proof

let c be Ordinal; :: thesis: for d being non empty Ordinal
for n being non zero Nat st S₁[d] & not c in rng (omega -exponent (CantorNF d)) holds
S₁[d (+) (n *^ (exp (omega,c)))]
let d be non empty Ordinal; :: thesis: for n being non zero Nat st S₁[d] & not c in rng (omega -exponent (CantorNF d)) holds
S₁[d (+) (n *^ (exp (omega,c)))]
let n be non zero Nat; :: thesis: ( S₁[d] & not c in rng (omega -exponent (CantorNF d)) implies S₁[d (+) (n *^ (exp (omega,c)))] )
assume A4: ( S₁[d] & not c in rng (omega -exponent (CantorNF d)) ) ; :: thesis: S₁[d (+) (n *^ (exp (omega,c)))]
let b be Ordinal; :: thesis: ( omega -exponent (d (+) (n *^ (exp (omega,c)))) in omega -exponent b implies d (+) (n *^ (exp (omega,c))) in exp (omega,(omega -exponent b)) )
assume omega -exponent (d (+) (n *^ (exp (omega,c)))) in omega -exponent b ; :: thesis: d (+) (n *^ (exp (omega,c))) in exp (omega,(omega -exponent b))
then (omega -exponent d) \/ (omega -exponent (n *^ (exp (omega,c)))) in omega -exponent b by Th100;
then ( omega -exponent d in omega -exponent b & omega -exponent (n *^ (exp (omega,c))) in omega -exponent b ) by XBOOLE_1:7, ORDINAL1:12;
then ( d in exp (omega,(omega -exponent b)) & n *^ (exp (omega,c)) in exp (omega,(omega -exponent b)) ) by A1, A4;
hence d (+) (n *^ (exp (omega,c))) in exp (omega,(omega -exponent b)) by Th101; :: thesis: verum

end;

A5: for a being non empty Ordinal holds S₁[a] from ORDINAL7:sch 1(A1, A3);
let a, b be Ordinal; :: thesis: ( omega -exponent a in omega -exponent b implies a in exp (omega,(omega -exponent b)) )

per cases ( a <> {} or a = {} ) ;

suppose a <> {} ; :: thesis: ( omega -exponent a in omega -exponent b implies a in exp (omega,(omega -exponent b)) )

hence ( omega -exponent a in omega -exponent b implies a in exp (omega,(omega -exponent b)) ) by A5; :: thesis: verum

end;

suppose A6: a = {} ; :: thesis: ( omega -exponent a in omega -exponent b implies a in exp (omega,(omega -exponent b)) )

assume omega -exponent a in omega -exponent b ; :: thesis: a in exp (omega,(omega -exponent b))
thus a in exp (omega,(omega -exponent b)) by A6, XBOOLE_1:61, ORDINAL1:11; :: thesis: verum

end;

end;