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 set 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 set 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 set 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 set ; :: 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

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 set such that
A1: ( [x,y] in P & [y,z] in R ) by RELAT_1:def 8;
reconsider a = y as Element of E by A1, ZFMISC_1:106;
take a ; :: thesis: ( [x,a] in P & [a,z] in R )
thus ( [x,a] in P & [a,z] in R ) by A1; :: thesis: verum

end;

given y being Element of E such that A2: ( [x,y] in P & [y,z] in R ) ; :: thesis: [x,z] in P * R
thus [x,z] in P * R by A2, RELAT_1:def 8; :: thesis: verum