let b be ordinal number ; :: thesis: ( b <> {} & b is limit_ordinal implies for phi being Ordinal-Sequence st dom phi = b & ( for c being ordinal number st c in b holds
phi . c = epsilon_ c ) holds
epsilon_ b = Union phi )
assume A0: ( b <> {} & b is limit_ordinal ) ; :: thesis: for phi being Ordinal-Sequence st dom phi = b & ( for c being ordinal number st c in b holds
phi . c = epsilon_ c ) holds
epsilon_ b = Union phi
let f be Ordinal-Sequence; :: thesis: ( dom f = b & ( for c being ordinal number st c in b holds
f . c = epsilon_ c ) implies epsilon_ b = Union f )
assume A1: ( dom f = b & ( for c being ordinal number st c in b holds
f . c = epsilon_ c ) ) ; :: thesis: epsilon_ b = Union f
then f is increasing Ordinal-Sequence by Th34;
then Union f is_limes_of f by A0, A1, ThND;
then Union f = lim f by ORDINAL2:def 14;
hence epsilon_ b = Union f by A0, A1, Th32; :: thesis: verum