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
A1: f is normal and
A2: ( union X in dom f & not X is empty ) and
A3: 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 A3;
hence union X = f . (union X) by A1, A2, Th36; :: thesis: verum