let R be Ring; :: thesis: for n being Nat holds One (R,n) is_a_unity_wrt matrix_mult (n,R)
let n be Nat; :: thesis: One (R,n) is_a_unity_wrt matrix_mult (n,R)
set mu = matrix_mult (n,R);
for x being Element of n -Matrices_over R holds
( (matrix_mult (n,R)) . ((One (R,n)),x) = x & (matrix_mult (n,R)) . (x,(One (R,n))) = x )

proof

let x be Element of n -Matrices_over R; :: thesis: ( (matrix_mult (n,R)) . ((One (R,n)),x) = x & (matrix_mult (n,R)) . (x,(One (R,n))) = x )
reconsider X = x as Matrix of n,R ;
thus (matrix_mult (n,R)) . ((One (R,n)),x) = (1. (R,n)) * X by Def5
.= x by MATRIX_3:18 ; :: thesis: (matrix_mult (n,R)) . (x,(One (R,n))) = x
thus (matrix_mult (n,R)) . (x,(One (R,n))) = X * (1. (R,n)) by Def5
.= x by MATRIX_3:19 ; :: thesis: verum

end;

hence One (R,n) is_a_unity_wrt matrix_mult (n,R) by BINOP_1:3; :: thesis: verum