let L1, L2, L3 be Ring; :: thesis: ( L1 is Subring of L2 & L2 is Subring of L3 implies L1 is Subring of L3 )
assume that
A1: L1 is Subring of L2 and
A2: L2 is Subring of L3 ; :: thesis: L1 is Subring of L3
A3: ( the carrier of L1 c= the carrier of L2 & the addF of L1 = the addF of L2 || the carrier of L1 & the multF of L1 = the multF of L2 || the carrier of L1 & 1. L1 = 1. L2 & 0. L1 = 0. L2 ) by A1, C0SP1:def 3;
A4: ( the carrier of L2 c= the carrier of L3 & the addF of L2 = the addF of L3 || the carrier of L2 & the multF of L2 = the multF of L3 || the carrier of L2 & 1. L2 = 1. L3 & 0. L2 = 0. L3 ) by A2, C0SP1:def 3;
set A1 = [: the carrier of L1, the carrier of L1:];
set A2 = [: the carrier of L2, the carrier of L2:];
set A3 = [: the carrier of L3, the carrier of L3:];
A8: the carrier of L1 c= the carrier of L3 by A3, A4;
A9: the addF of L1 = the addF of L2 || the carrier of L1 by A1, C0SP1:def 3
.= ( the addF of L3 || the carrier of L2) || the carrier of L1 by A2, C0SP1:def 3
.= the addF of L3 || the carrier of L1 by A3, ZFMISC_1:96, RELAT_1:74 ;
A10: the multF of L1 = the multF of L2 || the carrier of L1 by A1, C0SP1:def 3
.= ( the multF of L3 || the carrier of L2) || the carrier of L1 by A2, C0SP1:def 3
.= the multF of L3 || the carrier of L1 by A3, ZFMISC_1:96, RELAT_1:74 ;
A11: 1. L1 = 1. L2 by A1, C0SP1:def 3
.= 1. L3 by A2, C0SP1:def 3 ;
0. L1 = 0. L2 by A1, C0SP1:def 3
.= 0. L3 by A2, C0SP1:def 3 ;
hence L1 is Subring of L3 by A8, A9, A10, A11, C0SP1:def 3; :: thesis: verum