let A be Ordinal; :: thesis:
defpred S₁[ Ordinal] means exp (1,$1) = 1;
A1: for A being Ordinal st S₁[A] holds
S₁[ succ A]

let A be Ordinal; :: thesis:
assume exp (1,A) = 1 ; :: thesis:
hence exp (1,(succ A)) = 1 *^ 1 by Th44
.= 1 by Th39 ;
:: thesis:

end;

thus exp (A,1) = A *^ (exp (A,0)) by Lm1, Th44
.= A *^ 1 by Th43
.= A by Th39 ; :: thesis:
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]

deffunc H₁( Ordinal) -> Ordinal = exp (1,$1);
let A be Ordinal; :: thesis:
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:
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}

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng fi ; :: thesis:
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:

end;

set x = the Element of A;
thus 0 <> 1 ; :: thesis:
let B, C be Ordinal; :: thesis:
assume A10: ( B in 1 & 1 in C ) ; :: thesis:
reconsider x = the Element of A as Ordinal ;
take D = x; :: thesis:
thus D in dom fi by A3, A6; :: thesis:
let E be Ordinal; :: thesis:
assume that
D c= E and
A11: E in dom fi ; :: thesis:
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:

end;

end;