now :: thesis: for x, z being object st [x,z] in P * R holds
[x,z] in [:X,Z:]
let x, z be object ; :: thesis: ( [x,z] in P * R implies [x,z] in [:X,Z:] )
assume [x,z] in P * R ; :: thesis: [x,z] in [:X,Z:]
then ex y being object st
( [x,y] in P & [y,z] in R ) by RELAT_1:def 8;
then ( x in X & z in Z ) by ZFMISC_1:87;
hence [x,z] in [:X,Z:] by ZFMISC_1:87; :: thesis: verum
end;
hence P * R is Relation of X,Z by RELAT_1:def 3; :: thesis: verum