let A, B be Ring; :: thesis: ( 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 ; :: thesis: ( 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 ;
In ((1. A),B) = In ((1. B),B) by A1, C0SP1:def 3
.= 1. B ;
hence ( In ((0. A),B) = 0. B & In ((1. A),B) = 1. B ) by A2; :: thesis: verum