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 3 :: 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 4 :: 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 2 :: 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 12 :: 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 3 :: 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 7 :: 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