let x, X, Y be set ; :: thesis: ( x in X implies Im ([:X,Y:],x) = Y )
assume Z: x in X ; :: thesis: Im ([:X,Y:],x) = Y
thus Im ([:X,Y:],x) c= Y :: according to XBOOLE_0:def 10 :: thesis: Y c= Im ([:X,Y:],x)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Im ([:X,Y:],x) or y in Y )
assume y in Im ([:X,Y:],x) ; :: thesis: y in Y
then ex z being set st
( [z,y] in [:X,Y:] & z in {x} ) by Def13;
hence y in Y by ZFMISC_1:106; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Y or y in Im ([:X,Y:],x) )
assume y in Y ; :: thesis: y in Im ([:X,Y:],x)
then A: [x,y] in [:X,Y:] by Z, ZFMISC_1:106;
x in {x} by TARSKI:def 1;
hence y in Im ([:X,Y:],x) by A, Def13; :: thesis: verum