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 )

thus x in R " D2 by A3, RELAT_1:def 14; :: thesis: verum

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

given y being Element of E such that A3:
( [x,y] in R & y in D2 )
; :: thesis: x in R " D2
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;( [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

thus x in R " D2 by A3, RELAT_1:def 14; :: thesis: verum