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 ;
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 ; :: thesis: verum