theorem :: MATGRP_0:57

for R being Ring
for n, i, j being Nat st i < j holds
for r being Element of R holds (1. (R,n)) + ((canMat (i,j,n,R)) * r) is upper_triangular