let V be Ring; :: thesis: for V1 being Subring of V holds
( ( for v1, w1 being Element of V1
for v, w being Element of V st v1 = v & w1 = w holds
v1 + w1 = v + w ) & ( for v1, w1 being Element of V1
for v, w being Element of V st v1 = v & w1 = w holds
v1 * w1 = v * w ) & 1_ V1 = 1_ V & 0. V1 = 0. V )
let V1 be Subring of V; :: thesis: ( ( for v1, w1 being Element of V1
for v, w being Element of V st v1 = v & w1 = w holds
v1 + w1 = v + w ) & ( for v1, w1 being Element of V1
for v, w being Element of V st v1 = v & w1 = w holds
v1 * w1 = v * w ) & 1_ V1 = 1_ V & 0. V1 = 0. V )

hereby :: thesis: ( ( for v1, w1 being Element of V1
for v, w being Element of V st v1 = v & w1 = w holds
v1 * w1 = v * w ) & 1_ V1 = 1_ V & 0. V1 = 0. V )

let x1, y1 be Element of V1; :: thesis: for x, y being Element of V st x1 = x & y1 = y holds
x1 + y1 = x + y
let x, y be Element of V; :: thesis: ( x1 = x & y1 = y implies x1 + y1 = x + y )
assume A1: ( x1 = x & y1 = y ) ; :: thesis: x1 + y1 = x + y
x1 + y1 = ( the addF of V || the carrier of V1) . [x1,y1] by C0SP1:def 3;
hence x1 + y1 = x + y by A1, FUNCT_1:49; :: thesis: verum

end;

hereby :: thesis: ( 1_ V1 = 1_ V & 0. V1 = 0. V )

let x1, y1 be Element of V1; :: thesis: for x, y being Element of V st x1 = x & y1 = y holds
x1 * y1 = x * y
let x, y be Element of V; :: thesis: ( x1 = x & y1 = y implies x1 * y1 = x * y )
assume A2: ( x1 = x & y1 = y ) ; :: thesis: x1 * y1 = x * y
x1 * y1 = ( the multF of V || the carrier of V1) . [x1,y1] by C0SP1:def 3;
hence x1 * y1 = x * y by A2, FUNCT_1:49; :: thesis: verum

end;

thus ( 1_ V1 = 1_ V & 0. V1 = 0. V ) by C0SP1:def 3; :: thesis: verum