thus F_Complex is add-associative :: thesis: ( F_Complex is right_zeroed & F_Complex is right_complementable & F_Complex is Abelian & F_Complex is commutative & F_Complex is associative & F_Complex is left_unital & F_Complex is right_unital & F_Complex is distributive & F_Complex is almost_left_invertible & not F_Complex is degenerated )

proof

let x, y, z be Element of F_Complex ; :: according to RLVECT_1:def 6 :: thesis: (x + y) + z = x + (y + z)
reconsider x1 = x, y1 = y, z1 = z as Element of COMPLEX by Def1;
thus (x + y) + z = addcomplex . [(the addF of F_Complex . [x1,y1]),z1] by Def1
.= addcomplex . (addcomplex . x1,y1),z1 by Def1
.= addcomplex . (x1 + y1),z1 by BINOP_2:def 3
.= (x1 + y1) + z1 by BINOP_2:def 3
.= x1 + (y1 + z1)
.= addcomplex . x1,(y1 + z1) by BINOP_2:def 3
.= addcomplex . [x1,(addcomplex . y1,z1)] by BINOP_2:def 3
.= addcomplex . [x1,(the addF of F_Complex . [y1,z1])] by Def1
.= x + (y + z) by Def1 ; :: thesis: verum

end;

thus F_Complex is right_zeroed :: thesis: ( F_Complex is right_complementable & F_Complex is Abelian & F_Complex is commutative & F_Complex is associative & F_Complex is left_unital & F_Complex is right_unital & F_Complex is distributive & F_Complex is almost_left_invertible & not F_Complex is degenerated )

proof

let x be Element of F_Complex ; :: according to RLVECT_1:def 7 :: thesis: x + (0. F_Complex ) = x
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: verum

end;

thus F_Complex is right_complementable :: thesis: ( F_Complex is Abelian & F_Complex is commutative & F_Complex is associative & F_Complex is left_unital & F_Complex is right_unital & F_Complex is distributive & F_Complex is almost_left_invertible & not F_Complex is degenerated )

proof

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

end;

thus F_Complex is Abelian :: thesis: ( F_Complex is commutative & F_Complex is associative & F_Complex is left_unital & F_Complex is right_unital & F_Complex is distributive & F_Complex is almost_left_invertible & not F_Complex is degenerated )

proof

let x, y be Element of F_Complex ; :: according to RLVECT_1:def 5 :: thesis: x + y = y + x
thus x + y = y + x ; :: thesis: verum

end;

thus F_Complex is commutative :: thesis: ( F_Complex is associative & F_Complex is left_unital & F_Complex is right_unital & F_Complex is distributive & F_Complex is almost_left_invertible & not F_Complex is degenerated )

proof

let x, y be Element of F_Complex ; :: according to GROUP_1:def 16 :: thesis: x * y = y * x
thus x * y = y * x ; :: thesis: verum

end;

thus F_Complex is associative :: thesis: ( F_Complex is left_unital & F_Complex is right_unital & F_Complex is distributive & F_Complex is almost_left_invertible & not F_Complex is degenerated )

proof

let x, y, z be Element of F_Complex ; :: according to GROUP_1:def 4 :: thesis: (x * y) * z = x * (y * z)
reconsider x1 = x, y1 = y, z1 = z as Element of COMPLEX by Def1;
thus (x * y) * z = multcomplex . (the multF of F_Complex . x1,y1),z1 by Def1
.= multcomplex . (multcomplex . x1,y1),z1 by Def1
.= multcomplex . (x1 * y1),z1 by BINOP_2:def 5
.= (x1 * y1) * z1 by BINOP_2:def 5
.= x1 * (y1 * z1)
.= multcomplex . x1,(y1 * z1) by BINOP_2:def 5
.= multcomplex . x1,(multcomplex . y1,z1) by BINOP_2:def 5
.= multcomplex . x1,(the multF of F_Complex . y1,z1) by Def1
.= x * (y * z) by Def1 ; :: thesis: verum

end;

thus F_Complex is left_unital ; :: thesis: ( F_Complex is right_unital & F_Complex is distributive & F_Complex is almost_left_invertible & not F_Complex is degenerated )
thus F_Complex is right_unital ; :: thesis: ( F_Complex is distributive & F_Complex is almost_left_invertible & not F_Complex is degenerated )
thus F_Complex is distributive :: thesis: ( F_Complex is almost_left_invertible & not F_Complex is degenerated )

proof

let x, y, z be Element of F_Complex ; :: according to VECTSP_1:def 18 :: thesis: ( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
reconsider x1 = x, y1 = y, z1 = z as Element of COMPLEX by Def1;
thus x * (y + z) = multcomplex . x1,(the addF of F_Complex . y1,z1) by Def1
.= multcomplex . x1,(addcomplex . y1,z1) by Def1
.= multcomplex . x1,(y1 + z1) by BINOP_2:def 3
.= x1 * (y1 + z1) by BINOP_2:def 5
.= (x1 * y1) + (x1 * z1)
.= addcomplex . (x1 * y1),(x1 * z1) by BINOP_2:def 3
.= addcomplex . (multcomplex . x1,y1),(x1 * z1) by BINOP_2:def 5
.= addcomplex . (multcomplex . x1,y1),(multcomplex . x1,z1) by BINOP_2:def 5
.= the addF of F_Complex . (multcomplex . x1,y1),(multcomplex . x1,z1) by Def1
.= the addF of F_Complex . (the multF of F_Complex . x1,y1),(multcomplex . x1,z1) by Def1
.= (x * y) + (x * z) by Def1 ; :: thesis: (y + z) * x = (y * x) + (z * x)
thus (y + z) * x = multcomplex . (the addF of F_Complex . y1,z1),x1 by Def1
.= multcomplex . (addcomplex . y1,z1),x1 by Def1
.= multcomplex . (y1 + z1),x1 by BINOP_2:def 3
.= (y1 + z1) * x1 by BINOP_2:def 5
.= (y1 * x1) + (z1 * x1)
.= addcomplex . (y1 * x1),(z1 * x1) by BINOP_2:def 3
.= addcomplex . (multcomplex . y1,x1),(z1 * x1) by BINOP_2:def 5
.= addcomplex . (multcomplex . y1,x1),(multcomplex . z1,x1) by BINOP_2:def 5
.= the addF of F_Complex . (multcomplex . y1,x1),(multcomplex . z1,x1) by Def1
.= the addF of F_Complex . (the multF of F_Complex . y1,x1),(multcomplex . z1,x1) by Def1
.= (y * x) + (z * x) by Def1 ; :: thesis: verum

end;

thus F_Complex is almost_left_invertible :: thesis: not F_Complex is degenerated

proof

let x be Element of F_Complex ; :: according to ALGSTR_0:def 39 :: thesis: ( x = 0. F_Complex or x is left_invertible )
reconsider x1 = x as Element of COMPLEX by Def1;
assume A1: x <> 0. F_Complex ; :: thesis: x is left_invertible
reconsider y = x1 " as Element of F_Complex by Def1;
take y ; :: according to ALGSTR_0:def 27 :: thesis: y * x = 1. F_Complex
x1 <> 0c by A1, Def1;
hence y * x = 1. F_Complex by Lm2, XCMPLX_0:def 7; :: thesis: verum

end;

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