for x being object st x in dom (F | J) holds
(F | J) . x is 1-sorted

proof

let x be object ; :: thesis: ( x in dom (F | J) implies (F | J) . x is 1-sorted )
assume A1: x in dom (F | J) ; :: thesis: (F | J) . x is 1-sorted
( J c= I & dom F = I ) by PARTFUN1:def 2;
then dom (F | J) c= dom F by RELAT_1:62;
then ( (F | J) . x = F . x & F . x is 1-sorted ) by A1, FUNCT_1:47, PRALG_1:def 12;
hence (F | J) . x is 1-sorted ; :: thesis: verum

end;

hence ( F | J is 1-sorted-yielding & F | J is J -defined & F | J is total ) by PRALG_1:def 12; :: thesis: verum