let K1, K2, K3 be Field; :: thesis: ( K1 is Subfield of K2 & K2 is Subfield of K3 implies K1 is Subfield of K3 )
assume A1: ( 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;
A2: the carrier of K1 c= the carrier of K2 by A1, Def1;
then A3: [: 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 A1, Def1;
then A4: the carrier of K1 c= the carrier of K3 by A2;
A5: the addF of K2 = the addF of K3 || the carrier of K2 by A1, Def1;
A6: the addF of K1 = the addF of K2 || the carrier of K1 by A1, Def1
.= the addF of K3 || the carrier of K1 by A3, A5, FUNCT_1:51 ;
A7: the multF of K2 = the multF of K3 || the carrier of K2 by A1, Def1;
A8: the multF of K1 = the multF of K2 || the carrier of K1 by A1, Def1
.= the multF of K3 || the carrier of K1 by A3, A7, FUNCT_1:51 ;
( 1. K1 = 1. K2 & 0. K1 = 0. K2 ) by A1, Def1;
then ( 1. K1 = 1. K3 & 0. K1 = 0. K3 ) by A1, Def1;
hence K1 is Subfield of K3 by A4, A6, A8, Def1; :: thesis: verum