let a be Ordinal; :: thesis: 1 |^|^ a = 1
defpred S₁[ Ordinal] means 1 |^|^ $1 = 1;
A1: S₁[ 0 ] by Th13;
A2: for a being Ordinal 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 Th14
.= 1 by ORDINAL2:46 ;
:: thesis: verum

end;

A3: 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

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
A4: ( A <> 0 & 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, Th15;
A8: rng fi c= {1}

proof

let x be object ; :: 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 object such that
A9: ( y in dom fi & x = fi . y ) by FUNCT_1:def 3;
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 :: thesis: ( {} <> 1 & ( for b, c being Ordinal 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 ) ) ) ) )

thus {} <> 1 ; :: thesis: for b, c being Ordinal 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; :: 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 ) ) )
set x = the Element of A;
reconsider x = the Element of A 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 3;
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 9;
hence 1 |^|^ A = 1 by A7, ORDINAL2:def 10; :: thesis: verum

end;

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