let a, b be Ordinal; :: thesis: for g being Ordinal-Sequence-valued Sequence st a in dom g & b in dom (criticals g) holds
(criticals g) . b is_a_fixpoint_of g . a
let g be Ordinal-Sequence-valued Sequence; :: thesis: ( a in dom g & b in dom (criticals g) implies (criticals g) . b is_a_fixpoint_of g . a )
assume that
A1: a in dom g and
A2: b in dom (criticals g) ; :: thesis: (criticals g) . b is_a_fixpoint_of g . a
set h = criticals g;
set X = { c where c is Element of dom (g . 0) : ( c in dom (g . 0) & ( for f being Ordinal-Sequence st f in rng g holds
c is_a_fixpoint_of f ) ) } ;
{ c where c is Element of dom (g . 0) : ( c in dom (g . 0) & ( for f being Ordinal-Sequence st f in rng g holds
c is_a_fixpoint_of f ) ) } is ordinal-membered by Th46;
then rng (criticals g) = { c where c is Element of dom (g . 0) : ( c in dom (g . 0) & ( for f being Ordinal-Sequence st f in rng g holds
c is_a_fixpoint_of f ) ) } by Th19;
then (criticals g) . b in { c where c is Element of dom (g . 0) : ( c in dom (g . 0) & ( for f being Ordinal-Sequence st f in rng g holds
c is_a_fixpoint_of f ) ) } by A2, FUNCT_1:def 3;
then consider c being Element of dom (g . 0) such that
A3: ( (criticals g) . b = c & c in dom (g . 0) & ( for f being Ordinal-Sequence st f in rng g holds
c is_a_fixpoint_of f ) ) ;
g . a in rng g by A1, FUNCT_1:def 3;
hence (criticals g) . b is_a_fixpoint_of g . a by A3; :: thesis: verum