let x be Element of F_Real; :: according to VECTSP_1:def 16 :: thesis: ( x * (1. F_Real) = x & (1. F_Real) * x = x )
thus ( x * (1. F_Real) = x & (1. F_Real) * x = x ) ; :: thesis: verum