let f be Function-yielding Function; :: thesis: dom (rngs f) = dom f
thus dom (rngs f) c= dom f :: according to XBOOLE_0:def 10 :: thesis: dom f c= dom (rngs f)

proof

let i be set ; :: according to TARSKI:def 3 :: thesis: ( not i in dom (rngs f) or i in dom f )
dom (rngs f) = f " (SubFuncs (rng f)) by Def3;
hence ( not i in dom (rngs f) or i in dom f ) by Th28; :: thesis: verum

end;

thus dom f c= dom (rngs f) :: thesis: verum

proof

let i be set ; :: according to TARSKI:def 3 :: thesis: ( not i in dom f or i in dom (rngs f) )
assume A1: i in dom f ; :: thesis: i in dom (rngs f)
A2: f . i is Function ;
dom (rngs f) = f " (SubFuncs (rng f)) by Def3;
hence i in dom (rngs f) by A1, A2, Th28; :: thesis: verum

end;