let G1, G2, G3 be Group; :: thesis: ( G1 is Subgroup of G2 & G2 is Subgroup of G3 implies G1 is Subgroup of G3 )

assume that

A1: G1 is Subgroup of G2 and

A2: G2 is Subgroup of G3 ; :: thesis: G1 is Subgroup of G3

set h = the multF of G3;

set C = the carrier of G3;

set B = the carrier of G2;

set A = the carrier of G1;

A3: the carrier of G1 c= the carrier of G2 by A1, Def5;

then A4: [: the carrier of G1, the carrier of G1:] c= [: the carrier of G2, the carrier of G2:] by ZFMISC_1:96;

the carrier of G2 c= the carrier of G3 by A2, Def5;

then A5: the carrier of G1 c= the carrier of G3 by A3;

the multF of G1 = the multF of G2 || the carrier of G1 by A1, Def5

.= ( the multF of G3 || the carrier of G2) || the carrier of G1 by A2, Def5

.= the multF of G3 || the carrier of G1 by A4, FUNCT_1:51 ;

hence G1 is Subgroup of G3 by A5, Def5; :: thesis: verum

assume that

A1: G1 is Subgroup of G2 and

A2: G2 is Subgroup of G3 ; :: thesis: G1 is Subgroup of G3

set h = the multF of G3;

set C = the carrier of G3;

set B = the carrier of G2;

set A = the carrier of G1;

A3: the carrier of G1 c= the carrier of G2 by A1, Def5;

then A4: [: the carrier of G1, the carrier of G1:] c= [: the carrier of G2, the carrier of G2:] by ZFMISC_1:96;

the carrier of G2 c= the carrier of G3 by A2, Def5;

then A5: the carrier of G1 c= the carrier of G3 by A3;

the multF of G1 = the multF of G2 || the carrier of G1 by A1, Def5

.= ( the multF of G3 || the carrier of G2) || the carrier of G1 by A2, Def5

.= the multF of G3 || the carrier of G1 by A4, FUNCT_1:51 ;

hence G1 is Subgroup of G3 by A5, Def5; :: thesis: verum