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
ex e1 being Element of n -invertible_Matrices_over R st e1 is_a_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
ex e1 being Element of n -invertible_Matrices_over R st e1 is_a_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 ex e1 being Element of n -invertible_Matrices_over R st e1 is_a_unity_wrt F )
assume A1: F = (matrix_mult (n,R)) || (n -invertible_Matrices_over R) ; :: thesis: ex e1 being Element of n -invertible_Matrices_over R st e1 is_a_unity_wrt F
reconsider e1 = One (R,n) as Element of n -invertible_Matrices_over R by Th145;
take e1 ; :: thesis: e1 is_a_unity_wrt F
thus e1 is_a_unity_wrt F by A1, Th151; :: thesis: verum