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