let y, x, A, B be set ; :: thesis: for R being Subset of [:A,B:] holds
( y in Im (R ` ),x iff ( not [x,y] in R & x in A & y in B ) )
let R be Subset of [:A,B:]; :: thesis: ( y in Im (R ` ),x iff ( not [x,y] in R & x in A & y in B ) )
thus ( y in Im (R ` ),x implies ( not [x,y] in R & x in A & y in B ) ) :: thesis: ( not [x,y] in R & x in A & y in B implies y in Im (R ` ),x )

proof

assume y in Im (R ` ),x ; :: thesis: ( not [x,y] in R & x in A & y in B )
then consider a being set such that
A1: ( [a,y] in R ` & a in {x} ) by RELAT_1:def 13;
[x,y] in [:A,B:] \ R by A1, TARSKI:def 1;
hence ( not [x,y] in R & x in A & y in B ) by XBOOLE_0:def 5, ZFMISC_1:106; :: thesis: verum

end;

assume A2: ( not [x,y] in R & x in A & y in B ) ; :: thesis: y in Im (R ` ),x
ex a being set st
( [a,y] in R ` & a in {x} )

proof

A3: x in {x} by TARSKI:def 1;
[x,y] in [:A,B:] by A2, ZFMISC_1:106;
then [x,y] in [:A,B:] \ R by A2, XBOOLE_0:def 5;
hence ex a being set st
( [a,y] in R ` & a in {x} ) by A3; :: thesis: verum

end;

hence y in Im (R ` ),x by RELAT_1:def 13; :: thesis: verum