let D, E, F be non empty set ; :: thesis: for P being Relation of D,E

for R being Relation of E,F

for x, z being object holds

( [x,z] in P * R iff ex y being Element of E st

( [x,y] in P & [y,z] in R ) )

let P be Relation of D,E; :: thesis: for R being Relation of E,F

for x, z being object holds

( [x,z] in P * R iff ex y being Element of E st

( [x,y] in P & [y,z] in R ) )

let R be Relation of E,F; :: thesis: for x, z being object holds

( [x,z] in P * R iff ex y being Element of E st

( [x,y] in P & [y,z] in R ) )

let x, z be object ; :: thesis: ( [x,z] in P * R iff ex y being Element of E st

( [x,y] in P & [y,z] in R ) )

thus ( [x,z] in P * R implies ex y being Element of E st

( [x,y] in P & [y,z] in R ) ) :: thesis: ( ex y being Element of E st

( [x,y] in P & [y,z] in R ) implies [x,z] in P * R )

thus [x,z] in P * R by A3, RELAT_1:def 8; :: thesis: verum

for R being Relation of E,F

for x, z being object holds

( [x,z] in P * R iff ex y being Element of E st

( [x,y] in P & [y,z] in R ) )

let P be Relation of D,E; :: thesis: for R being Relation of E,F

for x, z being object holds

( [x,z] in P * R iff ex y being Element of E st

( [x,y] in P & [y,z] in R ) )

let R be Relation of E,F; :: thesis: for x, z being object holds

( [x,z] in P * R iff ex y being Element of E st

( [x,y] in P & [y,z] in R ) )

let x, z be object ; :: thesis: ( [x,z] in P * R iff ex y being Element of E st

( [x,y] in P & [y,z] in R ) )

thus ( [x,z] in P * R implies ex y being Element of E st

( [x,y] in P & [y,z] in R ) ) :: thesis: ( ex y being Element of E st

( [x,y] in P & [y,z] in R ) implies [x,z] in P * R )

proof

given y being Element of E such that A3:
( [x,y] in P & [y,z] in R )
; :: thesis: [x,z] in P * R
assume
[x,z] in P * R
; :: thesis: ex y being Element of E st

( [x,y] in P & [y,z] in R )

then consider y being object such that

A1: [x,y] in P and

A2: [y,z] in R by RELAT_1:def 8;

reconsider a = y as Element of E by A1, ZFMISC_1:87;

take a ; :: thesis: ( [x,a] in P & [a,z] in R )

thus ( [x,a] in P & [a,z] in R ) by A1, A2; :: thesis: verum

end;( [x,y] in P & [y,z] in R )

then consider y being object such that

A1: [x,y] in P and

A2: [y,z] in R by RELAT_1:def 8;

reconsider a = y as Element of E by A1, ZFMISC_1:87;

take a ; :: thesis: ( [x,a] in P & [a,z] in R )

thus ( [x,a] in P & [a,z] in R ) by A1, A2; :: thesis: verum

thus [x,z] in P * R by A3, RELAT_1:def 8; :: thesis: verum