Im (P,x) c= rng P
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Im (P,x) or y in rng P )
assume y in Im (P,x) ; :: thesis: y in rng P
then [x,y] in P by RELAT_1:169;
hence y in rng P by XTUPLE_0:def 13; :: thesis: verum
end;
hence Im (P,x) is finite ; :: thesis: verum