let K1 be Subfield of F_Rat ; :: thesis: the carrier of K1 = the carrier of F_Rat
thus the carrier of K1 c= the carrier of F_Rat by EC_PF_1:def 1; :: according to XBOOLE_0:def 10 :: thesis: the carrier of F_Rat c= the carrier of K1
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of F_Rat or x in the carrier of K1 )
set C1 = the carrier of K1;
A1: INT c= the carrier of K1 by Th24;
A2: NAT c= the carrier of K1 by Th23;
assume x in the carrier of F_Rat ; :: thesis: x in the carrier of K1
then reconsider x1 = x as Rational ;
consider m being Integer, k being Nat such that
A3: ( k > 0 & x1 = m / k ) by RAT_1:8;
A4: m in the carrier of K1 by A1, INT_1:def 2;
reconsider k2 = k, m2 = m as Element of F_Rat by RAT_1:def 2;
reconsider k0 = k as Element of K1 by A2, ORDINAL1:def 12;
A5: k0 <> 0. F_Rat by A3;
then k0 <> 0. K1 by EC_PF_1:def 1;
then consider k0i being Element of K1 such that
A6: k0i * k0 = 1. K1 by VECTSP_1:def 9;
the carrier of K1 c= the carrier of F_Rat by EC_PF_1:def 1;
then reconsider kk0 = k0i as Element of F_Rat ;
kk0 * k2 = 1. K1 by A6, Th18
.= 1. F_Rat by EC_PF_1:def 1 ;
then A7: kk0 = k2 " by A5, VECTSP_1:def 10;
A8: the multF of K1 = the multF of F_Rat || the carrier of K1 by EC_PF_1:def 1;
m / k = m2 / k2 by Th16, A3
.= the multF of K1 . (m2,(k2 ")) by A4, A7, A8, FUNCT_1:49, ZFMISC_1:87 ;
hence x in the carrier of K1 by A3, A4, A7, BINOP_1:17; :: thesis: verum