let R be Ring; :: thesis: for n, i, j being Nat st i <> j holds
for r being Element of R holds (1. (R,n)) + (r * (canMat (i,j,n,R))) is invertible Matrix of n,R
let n be Nat; :: thesis: for i, j being Nat st i <> j holds
for r being Element of R holds (1. (R,n)) + (r * (canMat (i,j,n,R))) is invertible Matrix of n,R
let i, j be Nat; :: thesis: ( i <> j implies for r being Element of R holds (1. (R,n)) + (r * (canMat (i,j,n,R))) is invertible Matrix of n,R )
assume A1: i <> j ; :: thesis: for r being Element of R holds (1. (R,n)) + (r * (canMat (i,j,n,R))) is invertible Matrix of n,R
let r be Element of R; :: thesis: (1. (R,n)) + (r * (canMat (i,j,n,R))) is invertible Matrix of n,R
set M = (1. (R,n)) + (r * (canMat (i,j,n,R)));

per cases ( n = 0 or n > 0 ) ;

suppose n = 0 ; :: thesis: (1. (R,n)) + (r * (canMat (i,j,n,R))) is invertible Matrix of n,R

then ((1. (R,n)) + (r * (canMat (i,j,n,R)))) * ((1. (R,n)) + (r * (canMat (i,j,n,R)))) = 1. (R,n) by MATRIX_0:45;
hence (1. (R,n)) + (r * (canMat (i,j,n,R))) is invertible Matrix of n,R by MATRIX_6:def 2, MATRIX_6:def 3; :: thesis: verum

end;

suppose A2: n > 0 ; :: thesis: (1. (R,n)) + (r * (canMat (i,j,n,R))) is invertible Matrix of n,R

ex M2 being Matrix of n,R st (1. (R,n)) + (r * (canMat (i,j,n,R))) is_reverse_of M2

proof

consider M2 being Matrix of n,R such that
A3: M2 = (1. (R,n)) - (r * (canMat (i,j,n,R))) ;
take M2 ; :: thesis: (1. (R,n)) + (r * (canMat (i,j,n,R))) is_reverse_of M2
A4: ( len (1. (R,n)) = len (r * (canMat (i,j,n,R))) & width (1. (R,n)) = width (r * (canMat (i,j,n,R))) & len (r * (canMat (i,j,n,R))) = width (1. (R,n)) & len (1. (R,n)) > 0 & len (r * (canMat (i,j,n,R))) > 0 )

proof

thus len (1. (R,n)) = n by MATRIX_0:24
.= len (r * (canMat (i,j,n,R))) by MATRIX_0:24 ; :: thesis: ( width (1. (R,n)) = width (r * (canMat (i,j,n,R))) & len (r * (canMat (i,j,n,R))) = width (1. (R,n)) & len (1. (R,n)) > 0 & len (r * (canMat (i,j,n,R))) > 0 )
thus width (1. (R,n)) = n by MATRIX_0:24
.= width (r * (canMat (i,j,n,R))) by MATRIX_0:24 ; :: thesis: ( len (r * (canMat (i,j,n,R))) = width (1. (R,n)) & len (1. (R,n)) > 0 & len (r * (canMat (i,j,n,R))) > 0 )
thus len (r * (canMat (i,j,n,R))) = n by MATRIX_0:24
.= width (1. (R,n)) by MATRIX_0:24 ; :: thesis: ( len (1. (R,n)) > 0 & len (r * (canMat (i,j,n,R))) > 0 )
thus len (1. (R,n)) > 0 by A2, MATRIX_0:24; :: thesis: len (r * (canMat (i,j,n,R))) > 0
thus len (r * (canMat (i,j,n,R))) > 0 by A2, MATRIX_0:24; :: thesis: verum

end;

A5: ( len (1. (R,n)) = len (r * (canMat (i,j,n,R))) & width (1. (R,n)) = width (r * (canMat (i,j,n,R))) & len (1. (R,n)) = width ((1. (R,n)) + (r * (canMat (i,j,n,R)))) & len (1. (R,n)) > 0 & len ((1. (R,n)) + (r * (canMat (i,j,n,R)))) > 0 )

proof

thus len (1. (R,n)) = len (r * (canMat (i,j,n,R))) by A4; :: thesis: ( width (1. (R,n)) = width (r * (canMat (i,j,n,R))) & len (1. (R,n)) = width ((1. (R,n)) + (r * (canMat (i,j,n,R)))) & len (1. (R,n)) > 0 & len ((1. (R,n)) + (r * (canMat (i,j,n,R)))) > 0 )
thus width (1. (R,n)) = width (r * (canMat (i,j,n,R))) by A4; :: thesis: ( len (1. (R,n)) = width ((1. (R,n)) + (r * (canMat (i,j,n,R)))) & len (1. (R,n)) > 0 & len ((1. (R,n)) + (r * (canMat (i,j,n,R)))) > 0 )
thus len (1. (R,n)) = n by MATRIX_0:24
.= width ((1. (R,n)) + (r * (canMat (i,j,n,R)))) by MATRIX_0:24 ; :: thesis: ( len (1. (R,n)) > 0 & len ((1. (R,n)) + (r * (canMat (i,j,n,R)))) > 0 )
thus len (1. (R,n)) > 0 by A4; :: thesis: len ((1. (R,n)) + (r * (canMat (i,j,n,R)))) > 0
thus len ((1. (R,n)) + (r * (canMat (i,j,n,R)))) > 0 by A2, MATRIX_0:24; :: thesis: verum

end;

A6: (r * (canMat (i,j,n,R))) * (r * (canMat (i,j,n,R))) = ((r * (canMat (i,j,n,R))) * r) * (canMat (i,j,n,R)) by Th24
.= (r * ((canMat (i,j,n,R)) * r)) * (canMat (i,j,n,R)) by Th26
.= (r * (r * (canMat (i,j,n,R)))) * (canMat (i,j,n,R)) by Th56
.= ((r * r) * (canMat (i,j,n,R))) * (canMat (i,j,n,R)) by Th27
.= (r * r) * ((canMat (i,j,n,R)) * (canMat (i,j,n,R))) by Th29
.= (r * r) * (0. (R,n)) by A1, Th50
.= 0. (R,n) by Th28 ;
A7: ( len (1. (R,n)) = len (r * (canMat (i,j,n,R))) & width (1. (R,n)) = width (r * (canMat (i,j,n,R))) )

proof

thus len (1. (R,n)) = n by MATRIX_0:24
.= len (r * (canMat (i,j,n,R))) by MATRIX_0:24 ; :: thesis: width (1. (R,n)) = width (r * (canMat (i,j,n,R)))
thus width (1. (R,n)) = n by MATRIX_0:24
.= width (r * (canMat (i,j,n,R))) by MATRIX_0:24 ; :: thesis: verum

end;

A8: ((1. (R,n)) + (r * (canMat (i,j,n,R)))) * M2 = (((1. (R,n)) + (r * (canMat (i,j,n,R)))) * (1. (R,n))) - (((1. (R,n)) + (r * (canMat (i,j,n,R)))) * (r * (canMat (i,j,n,R)))) by A3, A5, MATRIXR2:20
.= ((1. (R,n)) + (r * (canMat (i,j,n,R)))) - (((1. (R,n)) + (r * (canMat (i,j,n,R)))) * (r * (canMat (i,j,n,R)))) by MATRIX_3:19
.= ((1. (R,n)) + (r * (canMat (i,j,n,R)))) - (((1. (R,n)) * (r * (canMat (i,j,n,R)))) + ((r * (canMat (i,j,n,R))) * (r * (canMat (i,j,n,R))))) by A4, MATRIX_4:63
.= ((1. (R,n)) + (r * (canMat (i,j,n,R)))) - ((r * (canMat (i,j,n,R))) + (0. (R,n))) by A6, MATRIX_3:18
.= ((1. (R,n)) + (r * (canMat (i,j,n,R)))) - (r * (canMat (i,j,n,R))) by MATRIX_1:5
.= 1. (R,n) by A7, MATRIX_4:38 ;
A9: ( len (1. (R,n)) = len (r * (canMat (i,j,n,R))) & width (1. (R,n)) = width (r * (canMat (i,j,n,R))) & len ((1. (R,n)) + (r * (canMat (i,j,n,R)))) = width (1. (R,n)) & len (1. (R,n)) > 0 & len ((1. (R,n)) + (r * (canMat (i,j,n,R)))) > 0 )

proof

thus len (1. (R,n)) = n by MATRIX_0:24
.= len (r * (canMat (i,j,n,R))) by MATRIX_0:24 ; :: thesis: ( width (1. (R,n)) = width (r * (canMat (i,j,n,R))) & len ((1. (R,n)) + (r * (canMat (i,j,n,R)))) = width (1. (R,n)) & len (1. (R,n)) > 0 & len ((1. (R,n)) + (r * (canMat (i,j,n,R)))) > 0 )
thus width (1. (R,n)) = n by MATRIX_0:24
.= width (r * (canMat (i,j,n,R))) by MATRIX_0:24 ; :: thesis: ( len ((1. (R,n)) + (r * (canMat (i,j,n,R)))) = width (1. (R,n)) & len (1. (R,n)) > 0 & len ((1. (R,n)) + (r * (canMat (i,j,n,R)))) > 0 )
thus len ((1. (R,n)) + (r * (canMat (i,j,n,R)))) = n by MATRIX_0:24
.= width (1. (R,n)) by MATRIX_0:24 ; :: thesis: ( len (1. (R,n)) > 0 & len ((1. (R,n)) + (r * (canMat (i,j,n,R)))) > 0 )
thus len (1. (R,n)) > 0 by A2, MATRIX_0:24; :: thesis: len ((1. (R,n)) + (r * (canMat (i,j,n,R)))) > 0
thus len ((1. (R,n)) + (r * (canMat (i,j,n,R)))) > 0 by A2, MATRIX_0:24; :: thesis: verum

end;

A10: ( len (1. (R,n)) = len (r * (canMat (i,j,n,R))) & width (1. (R,n)) = width (r * (canMat (i,j,n,R))) & width (r * (canMat (i,j,n,R))) = len (1. (R,n)) & len (r * (canMat (i,j,n,R))) > 0 & len (1. (R,n)) > 0 )

proof

thus len (1. (R,n)) = len (r * (canMat (i,j,n,R))) by A9; :: thesis: ( width (1. (R,n)) = width (r * (canMat (i,j,n,R))) & width (r * (canMat (i,j,n,R))) = len (1. (R,n)) & len (r * (canMat (i,j,n,R))) > 0 & len (1. (R,n)) > 0 )
thus width (1. (R,n)) = width (r * (canMat (i,j,n,R))) by A9; :: thesis: ( width (r * (canMat (i,j,n,R))) = len (1. (R,n)) & len (r * (canMat (i,j,n,R))) > 0 & len (1. (R,n)) > 0 )
thus width (r * (canMat (i,j,n,R))) = n by MATRIX_0:24
.= len (1. (R,n)) by MATRIX_0:24 ; :: thesis: ( len (r * (canMat (i,j,n,R))) > 0 & len (1. (R,n)) > 0 )
thus len (r * (canMat (i,j,n,R))) > 0 by A2, MATRIX_0:24; :: thesis: len (1. (R,n)) > 0
thus len (1. (R,n)) > 0 by A9; :: thesis: verum

end;

M2 * ((1. (R,n)) + (r * (canMat (i,j,n,R)))) = ((1. (R,n)) * ((1. (R,n)) + (r * (canMat (i,j,n,R))))) - ((r * (canMat (i,j,n,R))) * ((1. (R,n)) + (r * (canMat (i,j,n,R))))) by A3, A9, MATRIXR2:16
.= ((1. (R,n)) + (r * (canMat (i,j,n,R)))) - ((r * (canMat (i,j,n,R))) * ((1. (R,n)) + (r * (canMat (i,j,n,R))))) by MATRIX_3:18
.= ((1. (R,n)) + (r * (canMat (i,j,n,R)))) - (((r * (canMat (i,j,n,R))) * (1. (R,n))) + (0. (R,n))) by A6, A10, MATRIX_4:62
.= ((1. (R,n)) + (r * (canMat (i,j,n,R)))) - ((r * (canMat (i,j,n,R))) * (1. (R,n))) by MATRIX_1:5
.= ((1. (R,n)) + (r * (canMat (i,j,n,R)))) - (r * (canMat (i,j,n,R))) by MATRIX_3:19
.= 1. (R,n) by A10, MATRIX_4:21 ;
hence (1. (R,n)) + (r * (canMat (i,j,n,R))) is_reverse_of M2 by A8, MATRIX_6:def 2; :: thesis: verum

end;

hence (1. (R,n)) + (r * (canMat (i,j,n,R))) is invertible Matrix of n,R by MATRIX_6:def 3; :: thesis: verum

end;

end;