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

proof

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

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: ( A <> 0 & A is limit_ordinal & ( for C being Ordinal st C in A holds
S₁[C] ) implies S₁[A] )
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: exp ({},A) = {}
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 ( 0 = 0 or 0 <> 0 ) ;
:: according to ORDINAL2:def 9

case 0 = 0 ; :: thesis: 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 fi . b₂ = 0 ) ) )

take B = 1; :: thesis: ( B in dom fi & ( for b₁ being set holds
( not B c= b₁ or not b₁ in dom fi or fi . b₁ = 0 ) ) )
{} in A by A3, ORDINAL3:8;
hence B in dom fi by A4, A6, Lm3, ORDINAL1:28; :: thesis: for b₁ being set holds
( not B c= b₁ or not b₁ in dom fi or fi . b₁ = 0 )
let D be Ordinal; :: thesis: ( not B c= D or not D in dom fi or fi . D = 0 )
assume A7: B c= D ; :: thesis: ( not D in dom fi or fi . D = 0 )
assume A8: D in dom fi ; :: thesis: fi . D = 0
then S₁[D] by A5, A6;
hence fi . D = 0 by A6, A7, A8, Lm3, ORDINAL1:21; :: thesis: verum

end;

case 0 <> 0 ; :: thesis: 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₂ ) ) ) ) )

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: verum

end;

end;

end;

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

end;

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