let A be Ordinal; :: thesis: A *^ {} = {}
defpred S₁[ Ordinal] means $1 *^ {} = {} ;
A1: S₁[ {} ] by Th52;
A2: for A being Ordinal st S₁[A] holds
S₁[ succ A]

proof

let A be Ordinal; :: thesis: ( S₁[A] implies S₁[ succ A] )
assume A *^ {} = {} ; :: thesis: S₁[ succ A]
hence (succ A) *^ {} = {} +^ {} by Th53
.= {} by Th44 ;
:: thesis: verum

end;

A3: for A being Ordinal st A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S₁[B] ) holds
S₁[A]

proof

let A be Ordinal; :: thesis: ( A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S₁[B] ) implies S₁[A] )
assume that
A4: ( A <> {} & A is limit_ordinal ) and
A5: for B being Ordinal st B in A holds
B *^ {} = {} ; :: thesis: S₁[A]
deffunc H₁( Ordinal) -> Ordinal = $1 *^ {} ;
consider fi being Ordinal-Sequence such that
A6: ( dom fi = A & ( for B being Ordinal st B in A holds
fi . B = H₁(B) ) ) from ORDINAL2:sch 3();
A7: A *^ {} = union (sup fi) by A4, A6, Th54
.= union (sup (rng fi)) ;
rng fi = succ {}

proof

{} c= A ;
then A8: {} c< A by A4, XBOOLE_0:def 8;
then A9: {} in A by ORDINAL1:21;
thus for x being set st x in rng fi holds
x in succ {} :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: succ {} c= rng fi

proof

let x be set ; :: thesis: ( x in rng fi implies x in succ {} )
assume x in rng fi ; :: thesis: x in succ {}
then consider y being set such that
A10: ( y in dom fi & x = fi . y ) by FUNCT_1:def 5;
reconsider y = y as Ordinal by A10;
x = y *^ {} by A6, A10
.= {} by A5, A6, A10 ;
hence x in succ {} by TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in succ {} or x in rng fi )
assume x in succ {} ; :: thesis: x in rng fi
then A11: ( x = {} & {} *^ {} = {} ) by Th52, TARSKI:def 1;
then fi . x = x by A6, A8, ORDINAL1:21;
hence x in rng fi by A6, A9, A11, FUNCT_1:def 5; :: thesis: verum

end;

then sup (rng fi) = succ {} by Th26;
hence S₁[A] by A7, Th2; :: thesis: verum

end;

for A being Ordinal holds S₁[A] from ORDINAL2:sch 1(A1, A2, A3);
hence A *^ {} = {} ; :: thesis: verum