A1: for v being Element of F_Rat holds v is right_complementable

proof

let v be Element of F_Rat; :: thesis: v is right_complementable
reconsider v1 = v as Rational ;
set w1 = - v1;
reconsider w = - v1 as Element of F_Rat by RAT_1:def 2;
v + w = v1 + (- v1) by BINOP_2:def 15
.= 0. F_Rat ;
hence v is right_complementable ; :: thesis: verum

end;

A2: now :: thesis: for x, y being Element of F_Rat holds x * y = y * x

let x, y be Element of F_Rat; :: thesis: x * y = y * x
reconsider x1 = x, y1 = y as Rational ;
thus x * y = x1 * y1 by BINOP_2:def 17
.= y * x by BINOP_2:def 17 ; :: thesis: verum

end;

for v being Element of F_Rat st v <> 0. F_Rat holds
v is left_invertible

proof

let v be Element of F_Rat; :: thesis: ( v <> 0. F_Rat implies v is left_invertible )
assume A3: v <> 0. F_Rat ; :: thesis: v is left_invertible
reconsider v1 = v as Rational ;
set w1 = v1 " ;
reconsider w = v1 " as Element of F_Rat by RAT_1:def 2;
w * v = (v1 ") * v1 by BINOP_2:def 17
.= 1. F_Rat by A3, XCMPLX_0:def 7 ;
hence v is left_invertible ; :: thesis: verum

end;

hence ( the carrier of F_Rat is Subset of the carrier of F_Real & the addF of F_Rat = the addF of F_Real || the carrier of F_Rat & the multF of F_Rat = the multF of F_Real || the carrier of F_Rat & 1. F_Rat = 1. F_Real & 0. F_Rat = 0. F_Real & F_Rat is right_complementable & F_Rat is commutative & F_Rat is almost_left_invertible & not F_Rat is degenerated ) by A1, A2, Lm6, Lm7, GROUP_1:def 12, NUMBERS:12; :: thesis: verum