let A be Ordinal; :: thesis: {} +^ A = A
defpred S₁[ Ordinal] means {} +^ $1 = $1;
A1: S₁[ {} ] by Th44;
A2: for A being Ordinal st S₁[A] holds
S₁[ succ A] by Th45;
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 = 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 = sup fi by A4, A6, Th46
.= sup (rng fi) ;
rng fi = A

proof

thus for x being set st x in rng fi holds
x in A :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: A c= rng fi

proof

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

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in rng fi )
assume A9: x in A ; :: thesis: x in rng fi
then reconsider B = x as Ordinal ;
( {} +^ B = B & fi . B = {} +^ B ) by A5, A6, A9;
hence x in rng fi by A6, A9, FUNCT_1:def 5; :: thesis: verum

end;

hence S₁[A] by A7, Th26; :: thesis: verum

end;

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