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 )

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

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