let R be Ring; :: thesis: for n being Nat
for F being BinOp of (n -invertible_Matrices_over R) st F = (matrix_mult (n,R)) || (n -invertible_Matrices_over R) holds
One (R,n) = the_unity_wrt F
let n be Nat; :: thesis: for F being BinOp of (n -invertible_Matrices_over R) st F = (matrix_mult (n,R)) || (n -invertible_Matrices_over R) holds
One (R,n) = the_unity_wrt F
let F be BinOp of (n -invertible_Matrices_over R); :: thesis: ( F = (matrix_mult (n,R)) || (n -invertible_Matrices_over R) implies One (R,n) = the_unity_wrt F )
assume A1: F = (matrix_mult (n,R)) || (n -invertible_Matrices_over R) ; :: thesis: One (R,n) = the_unity_wrt F
reconsider e1 = One (R,n) as Element of n -invertible_Matrices_over R by Th145;
ex e being Element of n -invertible_Matrices_over R st e is_a_unity_wrt F by A1, Th152;
then ( the_unity_wrt F is_a_unity_wrt F & e1 is_a_unity_wrt F ) by A1, Th151, BINOP_1:def 8;
hence One (R,n) = the_unity_wrt F by BINOP_1:10; :: thesis: verum