let f be Function-yielding c=-monotone Sequence; :: thesis: for A being Ordinal
for X being set st ( for o being object st o in X holds
ex B being Ordinal st
( o in dom (f . B) & B in A ) ) holds
(union (rng (f | A))) .: X = (union (rng f)) .: X
let A be Ordinal; :: thesis: for X being set st ( for o being object st o in X holds
ex B being Ordinal st
( o in dom (f . B) & B in A ) ) holds
(union (rng (f | A))) .: X = (union (rng f)) .: X
let X be set ; :: thesis: ( ( for o being object st o in X holds
ex B being Ordinal st
( o in dom (f . B) & B in A ) ) implies (union (rng (f | A))) .: X = (union (rng f)) .: X )
assume A1: for x being object st x in X holds
ex B being Ordinal st
( x in dom (f . B) & B in A ) ; :: thesis: (union (rng (f | A))) .: X = (union (rng f)) .: X
union (rng (f | A)) c= union (rng f) by ZFMISC_1:77;
hence (union (rng (f | A))) .: X c= (union (rng f)) .: X by RELAT_1:124; :: according to XBOOLE_0:def 10 :: thesis: (union (rng f)) .: X c= (union (rng (f | A))) .: X
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (union (rng f)) .: X or y in (union (rng (f | A))) .: X )
assume A2: y in (union (rng f)) .: X ; :: thesis: y in (union (rng (f | A))) .: X
consider x being object such that
A3: ( x in dom (union (rng f)) & x in X & (union (rng f)) . x = y ) by A2, FUNCT_1:def 6;
consider B being Ordinal such that
A4: ( x in dom (f . B) & B in A ) by A3, A1;
A5: f . B <> {} by A4;
then B in dom f by FUNCT_1:def 2;
then A6: (f . B) . x = (union (rng f)) . x by A4, Th2;
A7: (f | A) . B = f . B by A4, FUNCT_1:49;
then A8: B in dom (f | A) by A5, FUNCT_1:def 2;
then A9: dom ((f | A) . B) c= dom (union (rng (f | A))) by Th2;
y = (union (rng (f | A))) . x by A8, Th2, A7, A4, A3, A6;
hence y in (union (rng (f | A))) .: X by A9, A7, A4, A3, FUNCT_1:def 6; :: thesis: verum