let R be Ring; :: thesis: for n being Nat
for x being Element of (GL (n,R))
for X being invertible Matrix of n,R st x = X holds
x " = X ~
let n be Nat; :: thesis: for x being Element of (GL (n,R))
for X being invertible Matrix of n,R st x = X holds
x " = X ~
let x be Element of (GL (n,R)); :: thesis: for X being invertible Matrix of n,R st x = X holds
x " = X ~
let X be invertible Matrix of n,R; :: thesis: ( x = X implies x " = X ~ )
assume A1: x = X ; :: thesis: x " = X ~
reconsider h = X ~ as Element of (GL (n,R)) by Th126;
X ~ is_reverse_of X by MATRIX_6:def 4;
then ( (X ~) * X = X * (X ~) & (X ~) * X = 1. (R,n) ) by MATRIX_6:def 2;
then ( X * (X ~) = 1_ (GL (n,R)) & (X ~) * X = 1_ (GL (n,R)) ) by Th130;
then ( 1_ (GL (n,R)) = x * h & 1_ (GL (n,R)) = h * x ) by A1, Th127;
hence x " = X ~ by GROUP_1:5; :: thesis: verum