let x be Element of F_Complex; :: according to VECTSP_1:def 6 :: 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