thus for x, y, z being Element of F_Real holds (x + y) + z = x + (y + z) ; :: according to RLVECT_1:def 3 :: thesis:
thus for x being Element of F_Real holds x + () = x ; :: according to RLVECT_1:def 4 :: thesis:
thus F_Real is right_complementable :: thesis:
proof
let x be Element of F_Real; :: according to ALGSTR_0:def 16 :: thesis:
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:
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:
thus for x, y being Element of F_Real holds x * y = y * x ; :: according to GROUP_1:def 12 :: thesis:
thus for x, y, z being Element of F_Real holds (x * y) * z = x * (y * z) ; :: according to GROUP_1:def 3 :: thesis:
thus for x being Element of F_Real holds () * x = x ; :: according to VECTSP_1:def 8 :: thesis:
thus for x being Element of F_Real holds x * () = x ; :: according to VECTSP_1:def 4 :: thesis:
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:
thus y * x = 1. F_Real by ; :: thesis: verum
end;
thus 0. F_Real <> 1. F_Real ; :: according to STRUCT_0:def 8 :: thesis: verum