let b be Ordinal; :: thesis: ( b <> {} & b is limit_ordinal implies for phi being Ordinal-Sequence st dom phi = b & ( for c being Ordinal st c in b holds
phi . c = epsilon_ c ) holds
epsilon_ b = Union phi )
assume A1: ( b <> {} & b is limit_ordinal ) ; :: thesis: for phi being Ordinal-Sequence st dom phi = b & ( for c being Ordinal 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 st c in b holds
f . c = epsilon_ c ) implies epsilon_ b = Union f )
assume A2: ( dom f = b & ( for c being Ordinal st c in b holds
f . c = epsilon_ c ) ) ; :: thesis: epsilon_ b = Union f
then f is increasing Ordinal-Sequence by Th45;
then Union f is_limes_of f by A1, A2, Th6;
then Union f = lim f by ORDINAL2:def 10;
hence epsilon_ b = Union f by A1, A2, Th43; :: thesis: verum