let L be 1-sorted ; :: thesis: for A, B, C being AlgebraStr over L st A is Subalgebra of B & B is Subalgebra of C holds

A is Subalgebra of C

let A, B, C be AlgebraStr over L; :: thesis: ( A is Subalgebra of B & B is Subalgebra of C implies A is Subalgebra of C )

assume that

A1: A is Subalgebra of B and

A2: B is Subalgebra of C ; :: thesis: A is Subalgebra of C

A3: the carrier of A c= the carrier of B by A1, Def3;

then A4: [: the carrier of A, the carrier of A:] c= [: the carrier of B, the carrier of B:] by ZFMISC_1:96;

the carrier of B c= the carrier of C by A2, Def3;

hence the carrier of A c= the carrier of C by A3; :: according to POLYALG1:def 3 :: thesis: ( 1. A = 1. C & 0. A = 0. C & the addF of A = the addF of C || the carrier of A & the multF of A = the multF of C || the carrier of A & the lmult of A = the lmult of C | [: the carrier of L, the carrier of A:] )

thus 1. A = 1. B by A1, Def3

.= 1. C by A2, Def3 ; :: thesis: ( 0. A = 0. C & the addF of A = the addF of C || the carrier of A & the multF of A = the multF of C || the carrier of A & the lmult of A = the lmult of C | [: the carrier of L, the carrier of A:] )

thus 0. A = 0. B by A1, Def3

.= 0. C by A2, Def3 ; :: thesis: ( the addF of A = the addF of C || the carrier of A & the multF of A = the multF of C || the carrier of A & the lmult of A = the lmult of C | [: the carrier of L, the carrier of A:] )

thus the addF of A = the addF of B || the carrier of A by A1, Def3

.= ( the addF of C || the carrier of B) || the carrier of A by A2, Def3

.= the addF of C || the carrier of A by A4, FUNCT_1:51 ; :: thesis: ( the multF of A = the multF of C || the carrier of A & the lmult of A = the lmult of C | [: the carrier of L, the carrier of A:] )

thus the multF of A = the multF of B || the carrier of A by A1, Def3

.= ( the multF of C || the carrier of B) || the carrier of A by A2, Def3

.= the multF of C || the carrier of A by A4, FUNCT_1:51 ; :: thesis: the lmult of A = the lmult of C | [: the carrier of L, the carrier of A:]

A5: [: the carrier of L, the carrier of A:] c= [: the carrier of L, the carrier of B:] by A3, ZFMISC_1:96;

thus the lmult of A = the lmult of B | [: the carrier of L, the carrier of A:] by A1, Def3

.= ( the lmult of C | [: the carrier of L, the carrier of B:]) | [: the carrier of L, the carrier of A:] by A2, Def3

.= the lmult of C | [: the carrier of L, the carrier of A:] by A5, FUNCT_1:51 ; :: thesis: verum

A is Subalgebra of C

let A, B, C be AlgebraStr over L; :: thesis: ( A is Subalgebra of B & B is Subalgebra of C implies A is Subalgebra of C )

assume that

A1: A is Subalgebra of B and

A2: B is Subalgebra of C ; :: thesis: A is Subalgebra of C

A3: the carrier of A c= the carrier of B by A1, Def3;

then A4: [: the carrier of A, the carrier of A:] c= [: the carrier of B, the carrier of B:] by ZFMISC_1:96;

the carrier of B c= the carrier of C by A2, Def3;

hence the carrier of A c= the carrier of C by A3; :: according to POLYALG1:def 3 :: thesis: ( 1. A = 1. C & 0. A = 0. C & the addF of A = the addF of C || the carrier of A & the multF of A = the multF of C || the carrier of A & the lmult of A = the lmult of C | [: the carrier of L, the carrier of A:] )

thus 1. A = 1. B by A1, Def3

.= 1. C by A2, Def3 ; :: thesis: ( 0. A = 0. C & the addF of A = the addF of C || the carrier of A & the multF of A = the multF of C || the carrier of A & the lmult of A = the lmult of C | [: the carrier of L, the carrier of A:] )

thus 0. A = 0. B by A1, Def3

.= 0. C by A2, Def3 ; :: thesis: ( the addF of A = the addF of C || the carrier of A & the multF of A = the multF of C || the carrier of A & the lmult of A = the lmult of C | [: the carrier of L, the carrier of A:] )

thus the addF of A = the addF of B || the carrier of A by A1, Def3

.= ( the addF of C || the carrier of B) || the carrier of A by A2, Def3

.= the addF of C || the carrier of A by A4, FUNCT_1:51 ; :: thesis: ( the multF of A = the multF of C || the carrier of A & the lmult of A = the lmult of C | [: the carrier of L, the carrier of A:] )

thus the multF of A = the multF of B || the carrier of A by A1, Def3

.= ( the multF of C || the carrier of B) || the carrier of A by A2, Def3

.= the multF of C || the carrier of A by A4, FUNCT_1:51 ; :: thesis: the lmult of A = the lmult of C | [: the carrier of L, the carrier of A:]

A5: [: the carrier of L, the carrier of A:] c= [: the carrier of L, the carrier of B:] by A3, ZFMISC_1:96;

thus the lmult of A = the lmult of B | [: the carrier of L, the carrier of A:] by A1, Def3

.= ( the lmult of C | [: the carrier of L, the carrier of B:]) | [: the carrier of L, the carrier of A:] by A2, Def3

.= the lmult of C | [: the carrier of L, the carrier of A:] by A5, FUNCT_1:51 ; :: thesis: verum