let R be Ring; for S being RingExtension of R
for T being Subset of S holds R is Subring of RAdj (R,T)
let S be RingExtension of R; for T being Subset of S holds R is Subring of RAdj (R,T)
let T be Subset of S; R is Subring of RAdj (R,T)
set P = RAdj (R,T);
X:
R is Subring of S
by FIELD_4:def 1;
A: 1. (RAdj (R,T)) =
1. S
by dRA
.=
1. R
by X, C0SP1:def 3
;
B: 0. (RAdj (R,T)) =
0. S
by dRA
.=
0. R
by X, C0SP1:def 3
;
C:
the carrier of R c= the carrier of (RAdj (R,T))
then Y:
[: the carrier of R, the carrier of R:] c= [: the carrier of (RAdj (R,T)), the carrier of (RAdj (R,T)):]
by ZFMISC_1:96;
D: the addF of (RAdj (R,T)) || the carrier of R =
( the addF of S || (carrierRA T)) || the carrier of R
by dRA
.=
( the addF of S || the carrier of (RAdj (R,T))) || the carrier of R
by dRA
.=
the addF of S || the carrier of R
by Y, FUNCT_1:51
.=
the addF of R
by X, C0SP1:def 3
;
the multF of (RAdj (R,T)) || the carrier of R =
( the multF of S || (carrierRA T)) || the carrier of R
by dRA
.=
( the multF of S || the carrier of (RAdj (R,T))) || the carrier of R
by dRA
.=
the multF of S || the carrier of R
by Y, FUNCT_1:51
.=
the multF of R
by X, C0SP1:def 3
;
hence
R is Subring of RAdj (R,T)
by A, B, C, D, C0SP1:def 3; verum