let A, B, C be set ; :: thesis: for R being Relation of A,B
for S being Relation of B,C holds
( proj2 (R * S) = S .: (proj2 R) & proj2 (R * S) c= proj2 S )
let R be Relation of A,B; :: thesis: for S being Relation of B,C holds
( proj2 (R * S) = S .: (proj2 R) & proj2 (R * S) c= proj2 S )
let S be Relation of B,C; :: thesis: ( proj2 (R * S) = S .: (proj2 R) & proj2 (R * S) c= proj2 S )
thus A1: proj2 (R * S) = (R * S) .: A by Th50
.= S .: (R .: A) by RELAT_1:126
.= S .: (proj2 R) by Th50 ; :: thesis: proj2 (R * S) c= proj2 S
proj2 R = rng R ;
then S .: (proj2 R) c= S .: B by RELAT_1:123;
hence proj2 (R * S) c= proj2 S by A1, Th50; :: thesis: verum