let f be Function; :: thesis: for X being set st rng f c= X holds
(id X) * f = f
let X be set ; :: thesis: ( rng f c= X implies (id X) * f = f )
assume rng f c= X ; :: thesis: (id X) * f = f
then reconsider g = f as Function of (dom f),X by FUNCT_2:2;
(id X) * g = g by FUNCT_2:17;
hence (id X) * f = f ; :: thesis: verum