let X be set ; :: thesis: for f being Function holds rng (X -indexing f) = (X \ (dom f)) \/ (f .: X)
let f be Function; :: thesis: rng (X -indexing f) = (X \ (dom f)) \/ (f .: X)
dom (id X) = X ;
hence rng (X -indexing f) = ((id X) .: (X \ (dom (f | X)))) \/ (rng (f | X)) by FRECHET:12
.= ((id X) .: (X \ (dom (f | X)))) \/ (f .: X) by RELAT_1:115
.= (X \ (dom (f | X))) \/ (f .: X) by FUNCT_1:92
.= (X \ ((dom f) /\ X)) \/ (f .: X) by RELAT_1:61
.= (X \ (dom f)) \/ (f .: X) by XBOOLE_1:47 ;
:: thesis: verum