theorem Th13: :: GAUSSINT:13

( 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 )