set X = Gauss_INT_Ring ;
let v, w be Element of Gauss_INT_Ring; :: according to GROUP_1:def 12 :: thesis: v * w = w * v
reconsider v1 = v, w1 = w as G_INTEG by Th2;
thus v * w = v1 * w1 by Th6
.= w * v by Th6 ; :: thesis: verum