let R be Ring; :: thesis:
let n be Nat; :: thesis:
let X be invertible Matrix of n,R; :: thesis:
assume A1: n <> 1 ; :: thesis:
reconsider g = X as Element of (GL (n,R)) by Th126;

let Y be invertible Matrix of n,R; :: thesis:
reconsider h = Y as Element of (GL (n,R)) by Th126;
thus X * Y = g * h by Th127
.= h * g by A2, GROUP_5:77
.= Y * X by Th127 ; :: thesis:

end;

then consider z being Element of R such that
A3: ( z in center R & z in UnitGroup R & X = z * (1. (R,n)) ) by A1, Th123;
take z = z; :: thesis:
thus z in center R by A3; :: thesis:
thus z in UnitGroup R by A3; :: thesis:
thus X = z * (1. (R,n)) by A3; :: thesis:

end;

given z being Element of R such that A4: ( z in center R & z in UnitGroup R & X = z * (1. (R,n)) ) ; :: thesis:
for h being Element of (GL (n,R)) holds g * h = h * g

let h be Element of (GL (n,R)); :: thesis:
reconsider Y = h as invertible Matrix of n,R by Th126;
thus g * h = X * Y by Th127
.= Y * (z * (1. (R,n))) by A4, Th100
.= h * g by A4, Th127 ; :: thesis:

end;