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

let B be Ordinal; :: thesis:
assume that
S₁[B] and
succ B <> {} ; :: thesis:
thus exp ({},(succ B)) = {} *^ (exp ({},B)) by ORDINAL2:44
.= {} by ORDINAL2:35 ; :: thesis:

end;

A2: for B being Ordinal st B <> 0 & B is limit_ordinal & ( for C being Ordinal st C in B holds
S₁[C] ) holds
S₁[B]

proof

deffunc H₁( Ordinal) -> set = exp ({},$1);
let A be Ordinal; :: thesis:
assume that
A3: A <> 0 and
A4: A is limit_ordinal and
A5: for C being Ordinal st C in A holds
S₁[C] and
A <> {} ; :: 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();
0 is_limes_of fi

proof

per cases ;
:: according to ORDINAL2:def 9

case 0 = 0 ; :: thesis:

take B = 1; :: thesis:
{} in A by A3, ORDINAL3:8;
hence B in dom fi by A4, A6, Lm3, ORDINAL1:28; :: thesis:
let D be Ordinal; :: thesis:
assume A7: B c= D ; :: thesis:
assume A8: D in dom fi ; :: thesis:
then S₁[D] by A5, A6;
hence fi . D = 0 by A6, A7, A8, Lm3, ORDINAL1:21; :: thesis:

end;

case 0 <> 0 ; :: thesis:

thus for b₁, b₂ being set holds
( not b₁ in 0 or not 0 in b₂ or ex b₃ being set st
( b₃ in dom fi & ( for b₄ being set holds
( not b₃ c= b₄ or not b₄ in dom fi or ( b₁ in fi . b₄ & fi . b₄ in b₂ ) ) ) ) ) ; :: thesis:

end;

then lim fi = {} by ORDINAL2:def 10;
hence exp ({},A) = {} by A3, A4, A6, ORDINAL2:45; :: thesis:

end;

A9: S₁[ 0 ] ;
for B being Ordinal holds S₁[B] from ORDINAL2:sch 1(A9, A1, A2);
hence ( A <> {} implies exp ({},A) = {} ) ; :: thesis: