let L1, L2, L3 be Ring; ( 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
; 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; verum