let A, B, C be set ; :: thesis: for R being Relation of A,B
for S being Relation of B,C holds
( proj1 (R * S) = (R ~ ) .: (proj1 S) & proj1 (R * S) c= proj1 R )
let R be Relation of A,B; :: thesis: for S being Relation of B,C holds
( proj1 (R * S) = (R ~ ) .: (proj1 S) & proj1 (R * S) c= proj1 R )
let S be Relation of B,C; :: thesis: ( proj1 (R * S) = (R ~ ) .: (proj1 S) & proj1 (R * S) c= proj1 R )
thus A1: proj1 (R * S) = ((R * S) ~ ) .: C by Th51
.= ((S ~ ) * (R ~ )) .: C by RELAT_1:54
.= (R ~ ) .: ((S ~ ) .: C) by RELAT_1:159
.= (R ~ ) .: (proj1 S) by Th51 ; :: thesis: proj1 (R * S) c= proj1 R
proj1 S = dom S ;
then proj1 (R * S) c= (R ~ ) .: B by A1, RELAT_1:156;
hence proj1 (R * S) c= proj1 R by Th51; :: thesis: verum