let A be Ordinal; :: thesis: A *^ {} = {}
defpred S₁[ Ordinal] means $1 *^ {} = {} ;
A1: 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;

A2: 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

deffunc H₁( Ordinal) -> Ordinal = $1 *^ {} ;
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
A3: A <> {} and
A4: A is limit_ordinal and
A5: for B being Ordinal st B in A holds
B *^ {} = {} ; :: thesis: S₁[A]
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();
rng fi = succ {}

proof

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
A7: y in dom fi and
A8: x = fi . y by FUNCT_1:def 5;
reconsider y = y as Ordinal by A7;
x = y *^ {} by A6, A7, A8
.= {} by A5, A6, A7 ;
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 A9: x = {} by TARSKI:def 1;
{} c= A ;
then A10: {} c< A by A3, XBOOLE_0:def 8;
then A11: {} in A by ORDINAL1:21;
{} *^ {} = {} by Th52;
then fi . x = x by A6, A10, A9, ORDINAL1:21;
hence x in rng fi by A6, A11, A9, FUNCT_1:def 5; :: thesis: verum

end;

then A12: sup (rng fi) = succ {} by Th26;
A *^ {} = union (sup fi) by A3, A4, A6, Th54
.= union (sup (rng fi)) ;
hence S₁[A] by A12, Th2; :: thesis: verum

end;

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