for y being object st y in rng (F | J) holds
y is Group

proof

let y be object ; :: thesis: ( y in rng (F | J) implies y is Group )
assume y in rng (F | J) ; :: thesis: y is Group
then consider j being object such that
A1: ( j in dom (F | J) & y = (F | J) . j ) by FUNCT_1:def 3;
A2: y = F . j by A1, FUNCT_1:47;
( dom (F | J) = J & dom F = I ) by PARTFUN1:def 2;
then F . j in rng F by A1, FUNCT_1:3;
hence y is Group by A2, Def1; :: thesis: verum

end;

hence ( F | J is Group-yielding & F | J is J -defined & F | J is total ) ; :: thesis: verum