let A, B be Ring; ( A is Subring of B implies ( In ((0. A),B) = 0. B & In ((1. A),B) = 1. B ) )
assume A1:
A is Subring of B
; ( In ((0. A),B) = 0. B & In ((1. A),B) = 1. B )
then A2: In ((0. A),B) =
In ((0. B),B)
by C0SP1:def 3
.=
0. B
by SUBSET_1:def 8
;
In ((1. A),B) =
In ((1. B),B)
by A1, C0SP1:def 3
.=
1. B
by SUBSET_1:def 8
;
hence
( In ((0. A),B) = 0. B & In ((1. A),B) = 1. B )
by A2; verum