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 Th51
.= S .: (R .: A) by RELAT_1:159
.= S .: (proj2 R) by Th51 ; :: thesis: proj2 (R * S) c= proj2 S
proj2 R = rng R ;
then S .: (proj2 R) c= S .: B by RELAT_1:156;
hence proj2 (R * S) c= proj2 S by A1, Th51; :: thesis: verum