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

S4: now

let b be ordinal number ; :: 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 EXP; :: 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 number ; :: according to ORDINAL2:def 13 :: thesis: for b₁ being set holds
( not b in proj1 (U exp a) or b = {} 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 number ; :: thesis: ( not b in proj1 (U exp a) or b = {} 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 <> {} & 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;
S7: (U exp a) | b is increasing by S4, 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 EXP;
(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 number ; :: 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 number such that
B1: ( d in b & c in exp (a,d) ) by B2, A5, A9, ORDINAL5:11;
d in U by A8, B1, ORDINAL1:10;
then exp (a,d) = (U exp a) . d by EXP
.= ((U exp a) | b) . d by B1, FUNCT_1:49 ;
hence c in Union ((U exp a) | b) by A6, B1, CARD_5:2; :: thesis: verum

end;

let c be ordinal number ; :: 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 set such that
B3: ( x in b & c in ((U exp a) | b) . x ) by A6, CARD_5:2;
reconsider x = x as Ordinal by B3;
x in U by A8, B3, ORDINAL1:10;
then exp (a,x) = (U exp a) . x by EXP
.= ((U exp a) | b) . x by B3, FUNCT_1:49 ;
hence c in (U exp a) . b by B2, B3, A5, A9, ORDINAL5:11; :: thesis: verum

end;

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