let D, D2, E be non empty set ; :: thesis: for R being Relation of D,E
for x being Element of D holds
( x in R " D2 iff ex y being Element of E st
( [x,y] in R & y in D2 ) )

let R be Relation of D,E; :: thesis: for x being Element of D holds
( x in R " D2 iff ex y being Element of E st
( [x,y] in R & y in D2 ) )

let x be Element of D; :: thesis: ( x in R " D2 iff ex y being Element of E st
( [x,y] in R & y in D2 ) )

thus ( x in R " D2 implies ex y being Element of E st
( [x,y] in R & y in D2 ) ) :: thesis: ( ex y being Element of E st
( [x,y] in R & y in D2 ) implies x in R " D2 )
proof
assume x in R " D2 ; :: thesis: ex y being Element of E st
( [x,y] in R & y in D2 )

then consider y being object such that
A1: [x,y] in R and
A2: y in D2 by RELAT_1:def 14;
reconsider b = y as Element of E by ;
take b ; :: thesis: ( [x,b] in R & b in D2 )
thus ( [x,b] in R & b in D2 ) by A1, A2; :: thesis: verum
end;
given y being Element of E such that A3: ( [x,y] in R & y in D2 ) ; :: thesis: x in R " D2
thus x in R " D2 by ; :: thesis: verum