let a be ordinal number ; :: thesis: 1 |^|^ a = 1
defpred S₁[ Ordinal] means 1 |^|^ $1 = 1;
A1: S₁[ {} ] by Th0;
A2: for a being ordinal number st S₁[a] holds
S₁[ succ a]

proof

let A be Ordinal; :: thesis: ( S₁[A] implies S₁[ succ A] )
assume S₁[A] ; :: thesis: S₁[ succ A]
hence 1 |^|^ (succ A) = exp 1,1 by Th1
.= 1 by ORDINAL2:63 ;
:: thesis: verum

end;

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
1 |^|^ B = 1 ; :: thesis: S₁[A]
deffunc H₁( Ordinal) -> Ordinal = 1 |^|^ $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: 1 |^|^ A = lim fi by A4, A6, Th2;
A8: rng fi c= {1}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng fi or x in {1} )
assume x in rng fi ; :: thesis: x in {1}
then consider y being set such that
A9: ( y in dom fi & x = fi . y ) by FUNCT_1:def 5;
reconsider y = y as Ordinal by A9;
x = 1 |^|^ y by A6, A9
.= 1 by A5, A6, A9 ;
hence x in {1} by TARSKI:def 1; :: thesis: verum

end;

now

thus {} <> 1 ; :: thesis: for b, c being ordinal number st b in 1 & 1 in c holds
ex D being Ordinal st
( D in dom fi & ( for E being Ordinal st D c= E & E in dom fi holds
( b in fi . E & fi . E in c ) ) )
let b, c be ordinal number ; :: thesis: ( b in 1 & 1 in c implies ex D being Ordinal st
( D in dom fi & ( for E being Ordinal st D c= E & E in dom fi holds
( b in fi . E & fi . E in c ) ) ) )
assume A10: ( b in 1 & 1 in c ) ; :: thesis: ex D being Ordinal st
( D in dom fi & ( for E being Ordinal st D c= E & E in dom fi holds
( b in fi . E & fi . E in c ) ) )
consider x being Element of A;
reconsider x = x as Ordinal ;
take D = x; :: thesis: ( D in dom fi & ( for E being Ordinal st D c= E & E in dom fi holds
( b in fi . E & fi . E in c ) ) )
thus D in dom fi by A4, A6; :: thesis: for E being Ordinal st D c= E & E in dom fi holds
( b in fi . E & fi . E in c )
let E be Ordinal; :: thesis: ( D c= E & E in dom fi implies ( b in fi . E & fi . E in c ) )
assume ( D c= E & E in dom fi ) ; :: thesis: ( b in fi . E & fi . E in c )
then fi . E in rng fi by FUNCT_1:def 5;
hence ( b in fi . E & fi . E in c ) by A8, A10, TARSKI:def 1; :: thesis: verum

end;

then 1 is_limes_of fi by ORDINAL2:def 13;
hence 1 |^|^ A = 1 by A7, ORDINAL2:def 14; :: thesis: verum

end;

for a being ordinal number holds S₁[a] from ORDINAL2:sch 1(A1, A2, A3);
hence 1 |^|^ a = 1 ; :: thesis: verum