thus for x, y, z being Element of F_Real holds (x + y) + z = x + (y + z) ; :: according to RLVECT_1:def 3 :: thesis: ( F_Real is right_zeroed & F_Real is right_complementable & F_Real is Abelian & F_Real is commutative & F_Real is associative & F_Real is left_unital & F_Real is right_unital & F_Real is distributive & F_Real is almost_left_invertible & not F_Real is degenerated )
thus for x being Element of F_Real holds x + (0. F_Real) = x ; :: according to RLVECT_1:def 4 :: thesis: ( F_Real is right_complementable & F_Real is Abelian & F_Real is commutative & F_Real is associative & F_Real is left_unital & F_Real is right_unital & F_Real is distributive & F_Real is almost_left_invertible & not F_Real is degenerated )
thus F_Real is right_complementable :: thesis: ( F_Real is Abelian & F_Real is commutative & F_Real is associative & F_Real is left_unital & F_Real is right_unital & F_Real is distributive & F_Real is almost_left_invertible & not F_Real is degenerated )
proof
let x be Element of F_Real; :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
reconsider x9 = x as Element of REAL ;
reconsider y = - x9 as Element of F_Real by XREAL_0:def 1;
take y ; :: according to ALGSTR_0:def 11 :: thesis: x + y = 0. F_Real
thus x + y = 0. F_Real ; :: thesis: verum
end;
thus for x, y being Element of F_Real holds x + y = y + x ; :: according to RLVECT_1:def 2 :: thesis: ( F_Real is commutative & F_Real is associative & F_Real is left_unital & F_Real is right_unital & F_Real is distributive & F_Real is almost_left_invertible & not F_Real is degenerated )
thus for x, y being Element of F_Real holds x * y = y * x ; :: according to GROUP_1:def 12 :: thesis: ( F_Real is associative & F_Real is left_unital & F_Real is right_unital & F_Real is distributive & F_Real is almost_left_invertible & not F_Real is degenerated )
thus for x, y, z being Element of F_Real holds (x * y) * z = x * (y * z) ; :: according to GROUP_1:def 3 :: thesis: ( F_Real is left_unital & F_Real is right_unital & F_Real is distributive & F_Real is almost_left_invertible & not F_Real is degenerated )
thus for x being Element of F_Real holds (1. F_Real) * x = x ; :: according to VECTSP_1:def 8 :: thesis: ( F_Real is right_unital & F_Real is distributive & F_Real is almost_left_invertible & not F_Real is degenerated )
thus for x being Element of F_Real holds x * (1. F_Real) = x ; :: according to VECTSP_1:def 4 :: thesis: ( F_Real is distributive & F_Real is almost_left_invertible & not F_Real is degenerated )
thus for x, y, z being Element of F_Real holds
( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) ) ; :: according to VECTSP_1:def 7 :: thesis: ( F_Real is almost_left_invertible & not F_Real is degenerated )
hereby :: according to VECTSP_1:def 9 :: thesis: not F_Real is degenerated
let x be Element of F_Real; :: thesis: ( x <> 0. F_Real implies ex y being Element of F_Real st y * x = 1. F_Real )
reconsider x9 = x as Element of REAL ;
assume A1: x <> 0. F_Real ; :: thesis: ex y being Element of F_Real st y * x = 1. F_Real
reconsider y = x9 " as Element of F_Real by XREAL_0:def 1;
take y = y; :: thesis: y * x = 1. F_Real
thus y * x = 1. F_Real by A1, XCMPLX_0:def 7; :: thesis: verum
end;
thus 0. F_Real <> 1. F_Real ; :: according to STRUCT_0:def 8 :: thesis: verum