hereby :: according to TOPS_5:def 1 :: thesis: J * f is non-Empty

let y be object ; :: thesis: ( y in rng (J * f) implies y is TopSpace )
assume y in rng (J * f) ; :: thesis: y is TopSpace
then y in rng J by RELAT_1:26, TARSKI:def 3;
hence y is TopSpace by Def1; :: thesis: verum

end;

for S being 1-sorted st S in rng (J * f) holds
not S is empty

proof

let S be 1-sorted ; :: thesis: ( S in rng (J * f) implies not S is empty )
assume S in rng (J * f) ; :: thesis: not S is empty
then S in rng J by RELAT_1:26, TARSKI:def 3;
hence not S is empty by WAYBEL_3:def 7; :: thesis: verum

end;

hence J * f is non-Empty by WAYBEL_3:def 7; :: thesis: verum