let R be Ring; :: thesis: for n being Nat
for S being Subring of R
for M1 being Matrix of n,R
for M2 being Matrix of n,S st M1 = M2 & M2 is invertible holds
M1 is invertible
let n be Nat; :: thesis: for S being Subring of R
for M1 being Matrix of n,R
for M2 being Matrix of n,S st M1 = M2 & M2 is invertible holds
M1 is invertible
let S be Subring of R; :: thesis: for M1 being Matrix of n,R
for M2 being Matrix of n,S st M1 = M2 & M2 is invertible holds
M1 is invertible
let M1 be Matrix of n,R; :: thesis: for M2 being Matrix of n,S st M1 = M2 & M2 is invertible holds
M1 is invertible
let M2 be Matrix of n,S; :: thesis: ( M1 = M2 & M2 is invertible implies M1 is invertible )
assume A1: M1 = M2 ; :: thesis: ( not M2 is invertible or M1 is invertible )
assume M2 is invertible ; :: thesis: M1 is invertible
then consider N2 being Matrix of n,S such that
A2: M2 is_reverse_of N2 by MATRIX_6:def 3;
A3: ( M2 * N2 = N2 * M2 & M2 * N2 = 1. (S,n) ) by A2, MATRIX_6:def 2;
reconsider N1 = N2 as Matrix of n,R by Th82;
( M1 * N1 = N1 * M1 & M1 * N1 = 1. (R,n) )

proof

thus M1 * N1 = M2 * N2 by A1, Th92
.= N1 * M1 by A1, A3, Th92 ; :: thesis: M1 * N1 = 1. (R,n)
thus M1 * N1 = M2 * N2 by A1, Th92
.= 1. (R,n) by A3, Th95 ; :: thesis: verum

end;

hence M1 is invertible by MATRIX_6:def 2, MATRIX_6:def 3; :: thesis: verum