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:35
.= (R ~) .: ((S ~) .: C) by RELAT_1:126
.= (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:123;
hence proj1 (R * S) c= proj1 R by Th51; :: thesis: verum