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