let x be Element of F_Rat; :: according to VECTSP_1:def 6 :: thesis: ( x * (1. F_Rat) = x & (1. F_Rat) * x = x )
reconsider x1 = x as Rational ;
thus x * (1. F_Rat) = x1 * 1 by BINOP_2:def 17
.= x ; :: thesis: (1. F_Rat) * x = x
thus (1. F_Rat) * x = 1 * x1 by BINOP_2:def 17
.= x ; :: thesis: verum