let S be R -isomorphic Ring; :: thesis: S is commutative
set f = the Isomorphism of R,S;
reconsider g = the Isomorphism of R,S " as Isomorphism of S,R by Lm7;
A1: g " = the Isomorphism of R,S ;

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

let a, b be Element of the carrier of S; :: thesis: a * b = b * a
thus a * b = the Isomorphism of R,S . (g . (a * b)) by A1, FUNCT_2:26
.= the Isomorphism of R,S . ((g . a) * (g . b)) by GROUP_6:def 6
.= the Isomorphism of R,S . (g . (b * a)) by GROUP_6:def 6
.= b * a by A1, FUNCT_2:26 ; :: thesis: verum

end;

hence S is commutative ; :: thesis: verum