let o be object ; :: thesis: for f being Function-yielding c=-monotone Sequence
for A, B being Ordinal st o in dom (f . B) & B in A holds
(union (rng (f | A))) . o = (union (rng f)) . o
let f be Function-yielding c=-monotone Sequence; :: thesis: for A, B being Ordinal st o in dom (f . B) & B in A holds
(union (rng (f | A))) . o = (union (rng f)) . o
let A, B be Ordinal; :: thesis: ( o in dom (f . B) & B in A implies (union (rng (f | A))) . o = (union (rng f)) . o )
assume A1: ( o in dom (f . B) & B in A ) ; :: thesis: (union (rng (f | A))) . o = (union (rng f)) . o
A2: f . B <> {} by A1;
then B in dom f by FUNCT_1:def 2;
then A3: (f . B) . o = (union (rng f)) . o by A1, Th2;
A4: (f | A) . B = f . B by A1, FUNCT_1:49;
(f | A) . B = f . B by A1, FUNCT_1:49;
then B in dom (f | A) by A2, FUNCT_1:def 2;
hence (union (rng (f | A))) . o = (union (rng f)) . o by A4, A3, Th2, A1; :: thesis: verum