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