let S be Subring of R; :: thesis: S is commutative

now :: thesis: for a, b being Element of S holds a * b = b * a

let a, b be Element of S; :: thesis: a * b = b * a
the carrier of S c= the carrier of R by C0SP1:def 3;
then reconsider x = a, y = b as Element of R ;
A1: [x,y] in [: the carrier of S, the carrier of S:] by ZFMISC_1:def 2;
A2: [y,x] in [: the carrier of S, the carrier of S:] by ZFMISC_1:def 2;
thus a * b = ( the multF of R || the carrier of S) . (x,y) by C0SP1:def 3
.= x * y by A1, FUNCT_1:49
.= y * x by GROUP_1:def 12
.= ( the multF of R || the carrier of S) . (b,a) by A2, FUNCT_1:49
.= b * a by C0SP1:def 3 ; :: thesis: verum

end;

hence S is commutative ; :: thesis: verum