let f be Function-yielding c=-monotone Sequence; :: thesis: for o being object st o in dom (union (rng f)) holds
ex A being Ordinal st
( A in dom f & o in dom (f . A) )
set U = union (rng f);
let x be object ; :: thesis: ( x in dom (union (rng f)) implies ex A being Ordinal st
( A in dom f & x in dom (f . A) ) )
assume x in dom (union (rng f)) ; :: thesis: ex A being Ordinal st
( A in dom f & x in dom (f . A) )
then [x,((union (rng f)) . x)] in union (rng f) by FUNCT_1:def 2;
then consider Y being set such that
A1: ( [x,((union (rng f)) . x)] in Y & Y in rng f ) by TARSKI:def 4;
consider z being object such that
A2: ( z in dom f & f . z = Y ) by FUNCT_1:def 3, A1;
reconsider z = z as Ordinal by A2;
take z ; :: thesis: ( z in dom f & x in dom (f . z) )
thus ( z in dom f & x in dom (f . z) ) by A2, A1, FUNCT_1:1; :: thesis: verum