let A be Ordinal; :: thesis: A *^ 0 = 0
defpred S₁[ Ordinal] means $1 *^ 0 = 0 ;
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 *^ 0 = 0 ; :: thesis: S₁[ succ A]
hence (succ A) *^ 0 = 0 +^ 0 by Th36
.= 0 by Th27 ;
:: thesis: verum

end;

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

proof

deffunc H₁( Ordinal) -> Ordinal = $1 *^ 0;
let A be Ordinal; :: thesis: ( A <> 0 & A is limit_ordinal & ( for B being Ordinal st B in A holds
S₁[B] ) implies S₁[A] )
assume that
A3: A <> 0 and
A4: A is limit_ordinal and
A5: for B being Ordinal st B in A holds
B *^ 0 = 0 ; :: 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 0

proof

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

proof

let x be object ; :: thesis: ( x in rng fi implies x in succ 0 )
assume x in rng fi ; :: thesis: x in succ 0
then consider y being object such that
A7: y in dom fi and
A8: x = fi . y by FUNCT_1:def 3;
reconsider y = y as Ordinal by A7;
x = y *^ 0 by A6, A7, A8
.= 0 by A5, A6, A7 ;
hence x in succ 0 by TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in succ 0 or x in rng fi )
assume x in succ 0 ; :: thesis: x in rng fi
then A9: x = 0 by TARSKI:def 1;
0 c= A ;
then A10: 0 c< A by A3;
then A11: 0 in A by ORDINAL1:11;
0 *^ 0 = 0 by Th35;
then fi . x = x by A6, A10, A9, ORDINAL1:11;
hence x in rng fi by A6, A11, A9, FUNCT_1:def 3; :: thesis: verum

end;

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

end;

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