let X be set ; :: thesis: for f being Ordinal-Sequence st f is normal & union X in dom f & not X is empty & ( for x being set st x in X holds
x is_a_fixpoint_of f ) holds
union X = f . (union X)
let f be Ordinal-Sequence; :: thesis: ( f is normal & union X in dom f & not X is empty & ( for x being set st x in X holds
x is_a_fixpoint_of f ) implies union X = f . (union X) )
assume that
Z0: f is normal and
Z1: ( union X in dom f & not X is empty ) and
Z2: for x being set st x in X holds
x is_a_fixpoint_of f ; :: thesis: union X = f . (union X)
for x being set st x in X holds
ex y being set st
( x c= y & y in X & y is_a_fixpoint_of f ) by Z2;
hence union X = f . (union X) by Z0, Z1, Th08a; :: thesis: verum