theorem LMLT11: :: ZMODUL08:4

(Int-mult-left F_Rat) | [:INT,INT:] = Int-mult-left INT.Ring