let R, Q, 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 Th160
.= rng (Q * S) by A1, Th160 ; :: thesis: verum