let a, b be ordinal number ; :: thesis: for g being Ordinal-Sequence-valued T-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 T-Sequence; :: thesis: ( a in dom g & b in dom (criticals g) implies (criticals g) . b is_a_fixpoint_of g . a )
assume that
Z0: a in dom g and
Z1: 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 ThA1;
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 ThN1a;
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 Z1, FUNCT_1:def 3;
then consider c being Element of dom (g . 0) such that
A1: ( (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 Z0, FUNCT_1:def 3;
hence (criticals g) . b is_a_fixpoint_of g . a by A1; :: thesis: verum