let x be Element of ; :: 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