let x be Element of F_Complex; :: thesis: F_Rat is Subring of FQ_Ring x
A1: the addF of F_Rat = the addF of (FQ_Ring x) || the carrier of F_Rat by Lm57;
A2: the multF of F_Rat = the multF of (FQ_Ring x) || the carrier of F_Rat by Lm58;
A3: 1. (FQ_Ring x) = 1. F_Complex by Lm52
.= 1. F_Rat by C0SP1:def 3, Th3 ;
0. (FQ_Ring x) = 0. F_Rat by Lm48, Lm7, SUBSET_1:def 8;
hence F_Rat is Subring of FQ_Ring x by Lm55, A1, A2, A3, C0SP1:def 3; :: thesis: verum