thus for w being Element of RAT holds multrat . (1,w) = w :: according to BINOP_1:def 7,BINOP_1:def 16 :: thesis: 1 is_a_right_unity_wrt multrat

proof

let w be Element of RAT ; :: thesis: multrat . (1,w) = w
thus multrat . (1,w) = 1 * w by Def17
.= w ; :: thesis: verum

end;

let w be Element of RAT ; :: according to BINOP_1:def 17 :: thesis: multrat . (w,1) = w
thus multrat . (w,1) = w * 1 by Def17
.= w ; :: thesis: verum