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 Th61
.= 1 by Th56 ;
:: thesis: verum

end;

thus exp (A,1) = A *^ (exp (A,{})) by Lm1, Th61
.= A *^ 1 by Th60
.= A by Th56 ; :: thesis: exp (1,A) = 1
A2: 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

deffunc H₁( Ordinal) -> Ordinal = exp (1,$1);
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
A3: A <> {} 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 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
A8: y in dom fi and
A9: x = fi . y by FUNCT_1:def 5;
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

consider x being Element of A;
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 ) ) )
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 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 5;
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 Def13;
exp (1,A) = lim fi by A3, A4, A6, Th62;
hence S₁[A] by A12, Def14; :: thesis: verum

end;

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