let x be Element of F_Complex ; :: according to VECTSP_1:def 16 :: thesis: ( x * (1. F_Complex ) = x & (1. F_Complex ) * x = x )
1. F_Complex = 1r by Def1;
hence ( x * (1. F_Complex ) = x & (1. F_Complex ) * x = x ) ; :: thesis: verum