let A be Ordinal; :: thesis: ( 1 *^ A = A & A *^ 1 = A )
thus 1 *^ A = ({} *^ A) +^ A by Lm1, Th53
.= {} +^ A by Th52
.= A by Th47 ; :: thesis: A *^ 1 = A
defpred S₁[ Ordinal] means $1 *^ (succ {} ) = $1;
A1: for A being Ordinal st ( for B being Ordinal st B in A holds
S₁[B] ) holds
S₁[A]

proof

let A be Ordinal; :: thesis: ( ( for B being Ordinal st B in A holds
S₁[B] ) implies S₁[A] )
assume A2: for B being Ordinal st B in A holds
B *^ (succ {} ) = B ; :: thesis: S₁[A]

A3: now

given B being Ordinal such that A4: A = succ B ; :: thesis: A *^ (succ {} ) = A
thus A *^ (succ {} ) = (B *^ (succ {} )) +^ (succ {} ) by A4, Th53
.= B +^ (succ {} ) by A2, A4, ORDINAL1:10
.= succ (B +^ {} ) by Th45
.= A by A4, Th44 ; :: thesis: verum

end;

now

assume A5: ( A <> {} & ( for B being Ordinal holds A <> succ B ) ) ; :: thesis: A *^ (succ {} ) = A
then A6: A is limit_ordinal by ORDINAL1:42;
deffunc H₁( Ordinal) -> Ordinal = $1 *^ (succ {} );
consider fi being Ordinal-Sequence such that
A7: ( dom fi = A & ( for D being Ordinal st D in A holds
fi . D = H₁(D) ) ) from ORDINAL2:sch 3();
A8: A *^ (succ {} ) = union (sup fi) by A5, A6, A7, Th54
.= union (sup (rng fi)) ;
A = rng fi

proof

thus A c= rng fi :: according to XBOOLE_0:def 10 :: thesis: rng fi c= A

proof

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 ;
x = B *^ (succ {} ) by A2, A9
.= fi . x by A7, A9 ;
hence x in rng fi by A7, A9, FUNCT_1:def 5; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng fi or x in A )
assume x in rng fi ; :: thesis: x in A
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;
fi . y = y *^ (succ {} ) by A7, A10
.= y by A2, A7, A10 ;
hence x in A by A7, A10; :: thesis: verum

end;

hence A *^ (succ {} ) = union A by A8, Th26
.= A by A6, ORDINAL1:def 6 ;
:: thesis: verum

end;

hence S₁[A] by A3, Th52; :: thesis: verum

end;

for A being Ordinal holds S₁[A] from ORDINAL1:sch 2(A1);
hence A *^ 1 = A ; :: thesis: verum