let R be Ring; :: thesis: for n being Nat
for x being object holds
( x is invertible Element of (Matrix_ring (n,R)) iff x is invertible Matrix of n,R )
let n be Nat; :: thesis: for x being object holds
( x is invertible Element of (Matrix_ring (n,R)) iff x is invertible Matrix of n,R )
let x be object ; :: thesis: ( x is invertible Element of (Matrix_ring (n,R)) iff x is invertible Matrix of n,R )

hereby :: thesis: ( x is invertible Matrix of n,R implies x is invertible Element of (Matrix_ring (n,R)) )

assume x is invertible Element of (Matrix_ring (n,R)) ; :: thesis: x is invertible Matrix of n,R
then ex X9 being invertible Matrix of n,R st X9 = x by Th143;
hence x is invertible Matrix of n,R ; :: thesis: verum

end;

assume x is invertible Matrix of n,R ; :: thesis: x is invertible Element of (Matrix_ring (n,R))
hence x is invertible Element of (Matrix_ring (n,R)) by Th143, Th72; :: thesis: verum