set f = U exp a;
A1: dom (U exp a) = On U by FUNCT_2:def 1;
A2: 0 in a by ORDINAL3:8;
succ 0 c= a ;
then 1 c< a ;
then A3: 1 in a by ORDINAL1:11;

A4: now :: thesis: for b being Ordinal st b in dom (U exp a) holds
(U exp a) . b = exp (a,b)

let b be Ordinal; :: thesis: ( b in dom (U exp a) implies (U exp a) . b = exp (a,b) )
assume b in dom (U exp a) ; :: thesis: (U exp a) . b = exp (a,b)
then b in U by A1, ORDINAL1:def 9;
hence (U exp a) . b = exp (a,b) by Def8; :: thesis: verum

end;

hence U exp a is increasing by A3, ORDINAL5:10; :: according to ORDINAL6:def 3 :: thesis: U exp a is continuous
let b be Ordinal; :: according to ORDINAL2:def 13 :: thesis: for b₁ being set holds
( not b in dom (U exp a) or b = 0 or not b is limit_ordinal or not b₁ = (U exp a) . b or b₁ is_limes_of (U exp a) | b )
let c be Ordinal; :: thesis: ( not b in dom (U exp a) or b = 0 or not b is limit_ordinal or not c = (U exp a) . b or c is_limes_of (U exp a) | b )
assume A5: ( b in dom (U exp a) & b <> 0 & b is limit_ordinal & c = (U exp a) . b ) ; :: thesis: c is_limes_of (U exp a) | b
then b c= dom (U exp a) by ORDINAL1:def 2;
then A6: dom ((U exp a) | b) = b by RELAT_1:62;
A7: (U exp a) | b is increasing by A4, A3, ORDINAL4:15, ORDINAL5:10;
A8: b in U by A1, A5, ORDINAL1:def 9;
then A9: (U exp a) . b = exp (a,b) by Def8;
(U exp a) . b = Union ((U exp a) | b)

proof

thus (U exp a) . b c= Union ((U exp a) | b) :: according to XBOOLE_0:def 10 :: thesis: Union ((U exp a) | b) c= (U exp a) . b

proof

let c be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not c in (U exp a) . b or c in Union ((U exp a) | b) )
assume c in (U exp a) . b ; :: thesis: c in Union ((U exp a) | b)
then consider d being Ordinal such that
A10: ( d in b & c in exp (a,d) ) by A2, A5, A9, ORDINAL5:11;
d in U by A8, A10, ORDINAL1:10;
then exp (a,d) = (U exp a) . d by Def8
.= ((U exp a) | b) . d by A10, FUNCT_1:49 ;
hence c in Union ((U exp a) | b) by A6, A10, CARD_5:2; :: thesis: verum

end;

let c be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not c in Union ((U exp a) | b) or c in (U exp a) . b )
assume c in Union ((U exp a) | b) ; :: thesis: c in (U exp a) . b
then consider x being object such that
A11: ( x in b & c in ((U exp a) | b) . x ) by A6, CARD_5:2;
reconsider x = x as Ordinal by A11;
x in U by A8, A11, ORDINAL1:10;
then exp (a,x) = (U exp a) . x by Def8
.= ((U exp a) | b) . x by A11, FUNCT_1:49 ;
hence c in (U exp a) . b by A2, A11, A5, A9, ORDINAL5:11; :: thesis: verum

end;

hence c is_limes_of (U exp a) | b by A5, A7, A6, ORDINAL5:6; :: thesis: verum