per cases ( x nin dom C or x in dom C ) ;

suppose x nin dom C ; :: thesis: C . x is the carrier of O -valued

then C . x = {} by FUNCT_1:def 2;
then rng (C . x) = {} ;
hence rng (C . x) c= the carrier of O ; :: according to RELAT_1:def 19 :: thesis: verum

end;

suppose x in dom C ; :: thesis: C . x is the carrier of O -valued

hence C . x is the carrier of O -valued by Def14; :: thesis: verum

end;

end;