let A be Ordinal; :: thesis: ( 1 *^ A = A & A *^ 1 = A )
defpred S₁[ Ordinal] means $1 *^ (succ 0) = $1;
thus 1 *^ A = (0 *^ A) +^ A by Lm1, Th36
.= 0 +^ A by Th35
.= A by Th30 ; :: thesis: A *^ 1 = A
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 0) = B ; :: thesis: S₁[A]

A3: now :: thesis: ( A <> 0 & ( for B being Ordinal holds A <> succ B ) implies A *^ (succ 0) = A )

deffunc H₁( Ordinal) -> Ordinal = $1 *^ (succ 0);
assume that
A4: A <> 0 and
A5: for B being Ordinal holds A <> succ B ; :: thesis: A *^ (succ 0) = A
consider fi being Ordinal-Sequence such that
A6: ( dom fi = A & ( for D being Ordinal st D in A holds
fi . D = H₁(D) ) ) from ORDINAL2:sch 3();
A7: A = rng fi

proof

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in rng fi )
assume A8: x in A ; :: thesis: x in rng fi
then reconsider B = x as Ordinal ;
x = B *^ (succ 0) by A2, A8
.= fi . x by A6, A8 ;
hence x in rng fi by A6, A8, FUNCT_1:def 3; :: thesis: verum

end;

let x be object ; :: 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 object such that
A9: y in dom fi and
A10: x = fi . y by FUNCT_1:def 3;
reconsider y = y as Ordinal by A9;
fi . y = y *^ (succ 0) by A6, A9
.= y by A2, A6, A9 ;
hence x in A by A6, A9, A10; :: thesis: verum

end;

A11: A is limit_ordinal by A5, ORDINAL1:29;
then A *^ (succ 0) = union (sup fi) by A4, A6, Th37
.= union (sup (rng fi)) ;
hence A *^ (succ 0) = union A by A7, Th18
.= A by A11 ;
:: thesis: verum

end;

now :: thesis: ( ex B being Ordinal st A = succ B implies A *^ (succ 0) = A )

given B being Ordinal such that A12: A = succ B ; :: thesis: A *^ (succ 0) = A
thus A *^ (succ 0) = (B *^ (succ 0)) +^ (succ 0) by A12, Th36
.= B +^ (succ 0) by A2, A12, ORDINAL1:6
.= succ (B +^ 0) by Th28
.= A by A12, Th27 ; :: thesis: verum

end;

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

end;

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