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)) = (X --> f) " (SubFuncs (rng (X --> f))) ) by Def2, FUNCOP_1:19;
A2: rng (X --> f) c= {f} by FUNCOP_1:19;
A3: SubFuncs (rng (X --> f)) = rng (X --> f)

proof

thus SubFuncs (rng (X --> f)) c= rng (X --> f) by Th27; :: according to XBOOLE_0:def 10 :: thesis: rng (X --> f) c= SubFuncs (rng (X --> f))
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (X --> f) or x in SubFuncs (rng (X --> f)) )
assume x in rng (X --> f) ; :: thesis: x in SubFuncs (rng (X --> f))
hence x in SubFuncs (rng (X --> f)) by A2, Def1; :: thesis: verum

end;

A4: ( dom (X --> f) = X & (X --> f) " (rng (X --> f)) = dom (X --> f) ) by FUNCOP_1:19, RELAT_1:169;

now

let x be set ; :: thesis: ( x in X implies (doms (X --> f)) . x = (X --> (dom f)) . x )
assume A5: 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:13;
hence (doms (X --> f)) . x = (X --> (dom f)) . x by A4, A3, A5, Def2; :: thesis: verum

end;

hence doms (X --> f) = X --> (dom f) by A1, A4, A3, FUNCT_1:9; :: thesis: rngs (X --> f) = X --> (rng f)

A6: now

let x be set ; :: thesis: ( x in X implies (rngs (X --> f)) . x = (X --> (rng f)) . x )
assume A7: 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:13;
hence (rngs (X --> f)) . x = (X --> (rng f)) . x by A4, A3, A7, Def3; :: thesis: verum

end;

( dom (X --> (rng f)) = X & dom (rngs (X --> f)) = (X --> f) " (SubFuncs (rng (X --> f))) ) by Def3, FUNCOP_1:19;
hence rngs (X --> f) = X --> (rng f) by A4, A3, A6, FUNCT_1:9; :: thesis: verum