let A be Ordinal; :: thesis: ( exp (A,1) = A & exp (1,A) = 1 )
defpred S₁[ Ordinal] means exp (1,$1) = 1;
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 exp (1,A) = 1 ; :: thesis: S₁[ succ A]
hence exp (1,(succ A)) = 1 *^ 1 by Th44
.= 1 by Th39 ;
:: thesis: verum

end;

thus exp (A,1) = A *^ (exp (A,0)) by Lm1, Th44
.= A *^ 1 by Th43
.= A by Th39 ; :: thesis: exp (1,A) = 1
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 = exp (1,$1);
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
exp (1,B) = 1 ; :: 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();
A7: 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
A8: y in dom fi and
A9: x = fi . y by FUNCT_1:def 3;
reconsider y = y as Ordinal by A8;
x = exp (1,y) by A6, A8, A9
.= 1 by A5, A6, A8 ;
hence x in {1} by TARSKI:def 1; :: thesis: verum

end;

now :: thesis: ( 0 <> 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 ) ) ) ) )

set x = the Element of A;
thus 0 <> 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 ) ) )
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 A3, 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 that
D c= E and
A11: E in dom fi ; :: thesis: ( B in fi . E & fi . E in C )
fi . E in rng fi by A11, FUNCT_1:def 3;
hence ( B in fi . E & fi . E in C ) by A7, A10, TARSKI:def 1; :: thesis: verum

end;

then A12: 1 is_limes_of fi by Def9;
exp (1,A) = lim fi by A3, A4, A6, Th45;
hence S₁[A] by A12, Def10; :: thesis: verum

end;

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