let R be Ring; :: thesis: for n being Nat
for g being Element of (GL (n,R))
for X, Y being Matrix of n,R st X = g holds
( Y = (inverse_op (GL (n,R))) . g iff Y is_reverse_of X )
let n be Nat; :: thesis: for g being Element of (GL (n,R))
for X, Y being Matrix of n,R st X = g holds
( Y = (inverse_op (GL (n,R))) . g iff Y is_reverse_of X )
let g be Element of (GL (n,R)); :: thesis: for X, Y being Matrix of n,R st X = g holds
( Y = (inverse_op (GL (n,R))) . g iff Y is_reverse_of X )
let X, Y be Matrix of n,R; :: thesis: ( X = g implies ( Y = (inverse_op (GL (n,R))) . g iff Y is_reverse_of X ) )
assume A1: X = g ; :: thesis: ( Y = (inverse_op (GL (n,R))) . g iff Y is_reverse_of X )

hereby :: thesis: ( Y is_reverse_of X implies Y = (inverse_op (GL (n,R))) . g )

assume Y = (inverse_op (GL (n,R))) . g ; :: thesis: Y is_reverse_of X
then A2: Y = g " by GROUP_1:def 6;
A3: X * Y = g * (g ") by A1, A2, Th127
.= 1_ (GL (n,R)) by GROUP_1:def 5
.= 1. (R,n) by Th130 ;
Y * X = (g ") * g by A1, A2, Th127
.= 1_ (GL (n,R)) by GROUP_1:def 5
.= 1. (R,n) by Th130 ;
hence Y is_reverse_of X by A3, MATRIX_6:def 2; :: thesis: verum

end;

assume A4: Y is_reverse_of X ; :: thesis: Y = (inverse_op (GL (n,R))) . g
then reconsider h = Y as Element of (GL (n,R)) by Th128, MATRIX_6:def 3;
A5: ( Y * X = X * Y & Y * X = 1. (R,n) ) by A4, MATRIX_6:def 2;
A6: 1_ (GL (n,R)) = 1. (R,n) by Th130
.= h * g by A1, A5, Th127 ;
1_ (GL (n,R)) = 1. (R,n) by Th130
.= g * h by A1, A5, Th127 ;
then h = g " by A6, GROUP_1:5
.= (inverse_op (GL (n,R))) . g by GROUP_1:def 6 ;
hence Y = (inverse_op (GL (n,R))) . g ; :: thesis: verum