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 A1, ZFMISC_1:87;
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 A3, RELAT_1:def 14; :: thesis: verum