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

hereby :: thesis: ( x is invertible Matrix of n,R implies x in n -invertible_Matrices_over R )

assume x in n -invertible_Matrices_over R ; :: thesis: x is invertible Matrix of n,R
then ex X being Element of n -Matrices_over R st
( X = x & X is invertible Matrix of n,R ) ;
hence x is invertible Matrix of n,R ; :: thesis: verum

end;

assume A1: x is invertible Matrix of n,R ; :: thesis: x in n -invertible_Matrices_over R
then x is Element of n -Matrices_over R by MATRIX_1:2;
hence x in n -invertible_Matrices_over R by A1; :: thesis: verum