let S be Subring of R; :: thesis: S is domRing-like

now :: thesis: for a, b being Element of S holds
( not a * b = 0. S or a = 0. S or b = 0. S )

let a, b be Element of S; :: thesis: ( not a * b = 0. S or a = 0. S or b = 0. S )
assume A1: a * b = 0. S ; :: thesis: ( a = 0. S or b = 0. S )
the carrier of S c= the carrier of R by C0SP1:def 3;
then reconsider x = a, y = b as Element of R ;
A2: [x,y] in [: the carrier of S, the carrier of S:] by ZFMISC_1:def 2;
A3: 0. S = 0. R by C0SP1:def 3;
a * b = ( the multF of R || the carrier of S) . (x,y) by C0SP1:def 3
.= x * y by A2, FUNCT_1:49 ;
hence ( a = 0. S or b = 0. S ) by A1, A3, VECTSP_2:def 1; :: thesis: verum

end;

hence S is domRing-like by VECTSP_2:def 1; :: thesis: verum