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