let R be Ring; :: thesis: for n being Nat holds One (R,n) = the_unity_wrt (matrix_mult (n,R))
let n be Nat; :: thesis: One (R,n) = the_unity_wrt (matrix_mult (n,R))
ex e being Element of n -Matrices_over R st e is_a_unity_wrt matrix_mult (n,R)

proof

take e = One (R,n); :: thesis: e is_a_unity_wrt matrix_mult (n,R)
thus e is_a_unity_wrt matrix_mult (n,R) by Th148; :: thesis: verum

end;

then A1: the_unity_wrt (matrix_mult (n,R)) is_a_unity_wrt matrix_mult (n,R) by BINOP_1:def 8;
One (R,n) is_a_unity_wrt matrix_mult (n,R) by Th148;
hence One (R,n) = the_unity_wrt (matrix_mult (n,R)) by A1, BINOP_1:10; :: thesis: verum