let n be Nat; :: thesis: for K being Field
for M1 being Matrix of n,K st M1 is Involutory holds
M1 is invertible
let K be Field; :: thesis: for M1 being Matrix of n,K st M1 is Involutory holds
M1 is invertible
let M1 be Matrix of n,K; :: thesis: ( M1 is Involutory implies M1 is invertible )
assume M1 is Involutory ; :: thesis: M1 is invertible
then M1 * M1 = 1. (K,n) by Def3;
then M1 is_reverse_of M1 by MATRIX_6:def 2;
hence M1 is invertible by MATRIX_6:def 3; :: thesis: verum