let A be Ordinal; :: thesis: ( exp A,1 = A & exp 1,A = 1 )
thus exp A,1 = A *^ (exp A,{} ) by Lm1, Th61
.= A *^ 1 by Th60
.= A by Th56 ; :: thesis: exp 1,A = 1
defpred S₁[ Ordinal] means exp 1,$1 = 1;
A1: S₁[ {} ] by Th60;
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 exp 1,A = 1 ; :: thesis: S₁[ succ A]
hence exp 1,(succ A) = 1 *^ 1 by Th61
.= 1 by Th56 ;
:: 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
exp 1,B = 1 ; :: thesis: S₁[A]
deffunc H₁( Ordinal) -> Ordinal = exp 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: exp 1,A = lim fi by A4, A6, Th62;
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 = exp 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 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 ) ) )
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 Def13;
hence S₁[A] by A7, Def14; :: thesis: verum

end;

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