let K1, K2, K3 be strict Field; :: thesis: ( K1 is Subfield of K2 & K2 is Subfield of K3 implies K1 is Subfield of K3 )
assume AS: ( K1 is Subfield of K2 & K2 is Subfield of K3 ) ; :: thesis: K1 is Subfield of K3
set C1 = the carrier of K1;
set C2 = the carrier of K2;
set C = the carrier of K3;
set ADD = the addF of K3;
set MULT = the multF of K3;
A0: the carrier of K1 c= the carrier of K2 by AS, PFDef2;
then A1: [: the carrier of K1, the carrier of K1:] c= [: the carrier of K2, the carrier of K2:] by ZFMISC_1:96;
the carrier of K2 c= the carrier of K3 by AS, PFDef2;
then A2: the carrier of K1 c= the carrier of K3 by A0, XBOOLE_1:1;
A3: the addF of K2 = the addF of K3 || the carrier of K2 by AS, PFDef2;
A4: the addF of K1 = the addF of K2 || the carrier of K1 by AS, PFDef2
.= the addF of K3 || the carrier of K1 by A1, A3, FUNCT_1:51 ;
A5: the multF of K2 = the multF of K3 || the carrier of K2 by AS, PFDef2;
A6: the multF of K1 = the multF of K2 || the carrier of K1 by AS, PFDef2
.= the multF of K3 || the carrier of K1 by A1, A5, FUNCT_1:51 ;
( 1. K1 = 1. K2 & 0. K1 = 0. K2 ) by AS, PFDef2;
then ( 1. K1 = 1. K3 & 0. K1 = 0. K3 ) by AS, PFDef2;
hence K1 is Subfield of K3 by A2, A4, A6, PFDef2; :: thesis: verum