let Q, R, S be Relation; :: thesis: ( rng R = rng Q implies rng (R * S) = rng (Q * S) )
assume A1: rng R = rng Q ; :: thesis: rng (R * S) = rng (Q * S)
thus rng (R * S) = S .: (rng R) by Th119
.= rng (Q * S) by A1, Th119 ; :: thesis: verum