thus F_Complex is add-associative ; :: thesis:
thus F_Complex is right_zeroed :: thesis:

proof

let x be Element of F_Complex; :: according to RLVECT_1:def 4 :: thesis:
reconsider x1 = x as Element of COMPLEX by Def1;
thus x + (0. F_Complex) = the addF of F_Complex . (x1,0c) by Def1
.= addcomplex . (x1,0c) by Def1
.= x1 + 0c by BINOP_2:def 3
.= x ; :: thesis:

end;

thus F_Complex is right_complementable :: thesis:

proof

let x be Element of F_Complex; :: according to ALGSTR_0:def 16 :: thesis:
reconsider x1 = x as Element of COMPLEX by Def1;
- x1 in COMPLEX by XCMPLX_0:def 2;
then reconsider y = - x1 as Element of F_Complex by Def1;
take y ; :: according to ALGSTR_0:def 11 :: thesis:
thus x + y = 0. F_Complex by Def1; :: thesis:

end;

thus F_Complex is Abelian ; :: thesis:
thus F_Complex is commutative ; :: thesis:
thus F_Complex is associative ; :: thesis:
thus F_Complex is left_unital ; :: thesis:
thus F_Complex is right_unital ; :: thesis:
thus F_Complex is distributive ; :: thesis:
thus F_Complex is almost_left_invertible :: thesis:

proof

let x be Element of F_Complex; :: according to ALGSTR_0:def 38 :: thesis:
reconsider x1 = x as Element of COMPLEX by Def1;
assume A1: x <> 0. F_Complex ; :: thesis:
x1 " in COMPLEX by XCMPLX_0:def 2;
then reconsider y = x1 " as Element of F_Complex by Def1;
take y ; :: according to ALGSTR_0:def 27 :: thesis:
x1 <> 0c by A1, Def1;
hence y * x = 1. F_Complex by Lm2, XCMPLX_0:def 7; :: thesis:

end;

0. F_Complex <> 1. F_Complex by Def1, Lm1;
hence not F_Complex is degenerated ; :: thesis: