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