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

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

hence
S is commutative
; :: thesis: verumlet 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;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