let K1 be Subfield of F_Rat ; 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; XBOOLE_0:def 10 the carrier of F_Rat c= the carrier of K1
let x be object ; TARSKI:def 3 ( 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
; 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; verum