let b be ordinal number ; :: thesis: for f being Ordinal-Sequence st b is_a_fixpoint_of f holds
ex a being ordinal number st
( a in dom (criticals f) & b = (criticals f) . a )
let f be Ordinal-Sequence; :: thesis: ( b is_a_fixpoint_of f implies ex a being ordinal number st
( a in dom (criticals f) & b = (criticals f) . a ) )
set X = { a where a is Element of dom f : a is_a_fixpoint_of f } ;
assume A1: b is_a_fixpoint_of f ; :: thesis: ex a being ordinal number st
( a in dom (criticals f) & b = (criticals f) . a )
then b in dom f by ABIAN:def 3;
then b in { a where a is Element of dom f : a is_a_fixpoint_of f } by A1;
then b in rng (criticals f) by Th03;
then ex x being set st
( x in dom (criticals f) & b = (criticals f) . x ) by FUNCT_1:def 3;
hence ex a being ordinal number st
( a in dom (criticals f) & b = (criticals f) . a ) ; :: thesis: verum