let f be Function-yielding c=-monotone Sequence; :: thesis: for A being Ordinal st A in dom f holds
( dom (f . A) c= dom (union (rng f)) & ( for o being object st o in dom (f . A) holds
(f . A) . o = (union (rng f)) . o ) )
set U = union (rng f);
let A be Ordinal; :: thesis: ( A in dom f implies ( dom (f . A) c= dom (union (rng f)) & ( for o being object st o in dom (f . A) holds
(f . A) . o = (union (rng f)) . o ) ) )
assume A1: A in dom f ; :: thesis: ( dom (f . A) c= dom (union (rng f)) & ( for o being object st o in dom (f . A) holds
(f . A) . o = (union (rng f)) . o ) )
A2: f . A in rng f by A1, FUNCT_1:def 3;
thus dom (f . A) c= dom (union (rng f)) :: thesis: for o being object st o in dom (f . A) holds
(f . A) . o = (union (rng f)) . o

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in dom (f . A) or y in dom (union (rng f)) )
assume y in dom (f . A) ; :: thesis: y in dom (union (rng f))
then [y,((f . A) . y)] in f . A by FUNCT_1:def 2;
then [y,((f . A) . y)] in union (rng f) by A2, TARSKI:def 4;
hence y in dom (union (rng f)) by FUNCT_1:1; :: thesis: verum

end;

let y be object ; :: thesis: ( y in dom (f . A) implies (f . A) . y = (union (rng f)) . y )
assume y in dom (f . A) ; :: thesis: (f . A) . y = (union (rng f)) . y
then [y,((f . A) . y)] in f . A by FUNCT_1:def 2;
then [y,((f . A) . y)] in union (rng f) by A2, TARSKI:def 4;
hence (f . A) . y = (union (rng f)) . y by FUNCT_1:1; :: thesis: verum