let X be set ; :: thesis: for f being Function holds
( doms (X --> f) = X --> (dom f) & rngs (X --> f) = X --> (rng f) )
let f be Function; :: thesis: ( doms (X --> f) = X --> (dom f) & rngs (X --> f) = X --> (rng f) )
A1: ( dom (X --> (dom f)) = X & dom (doms (X --> f)) = dom (X --> f) ) by Def1;
A2: ( dom (X --> f) = X & (X --> f) " (rng (X --> f)) = dom (X --> f) ) by RELAT_1:134;

now :: thesis: for x being object st x in X holds
(doms (X --> f)) . x = (X --> (dom f)) . x

let x be object ; :: thesis: ( x in X implies (doms (X --> f)) . x = (X --> (dom f)) . x )
assume A3: x in X ; :: thesis: (doms (X --> f)) . x = (X --> (dom f)) . x
then ( (X --> f) . x = f & (X --> (dom f)) . x = dom f ) by FUNCOP_1:7;
hence (doms (X --> f)) . x = (X --> (dom f)) . x by A2, A3, Def1; :: thesis: verum

end;

hence doms (X --> f) = X --> (dom f) by A1; :: thesis: rngs (X --> f) = X --> (rng f)

A4: now :: thesis: for x being object st x in X holds
(rngs (X --> f)) . x = (X --> (rng f)) . x

let x be object ; :: thesis: ( x in X implies (rngs (X --> f)) . x = (X --> (rng f)) . x )
assume A5: x in X ; :: thesis: (rngs (X --> f)) . x = (X --> (rng f)) . x
then ( (X --> f) . x = f & (X --> (rng f)) . x = rng f ) by FUNCOP_1:7;
hence (rngs (X --> f)) . x = (X --> (rng f)) . x by A2, A5, Def2; :: thesis: verum

end;

( dom (X --> (rng f)) = X & dom (rngs (X --> f)) = dom (X --> f) ) by Def2;
hence rngs (X --> f) = X --> (rng f) by A4; :: thesis: verum