let K be Field; :: thesis: for A being Matrix of 0 ,K holds A is invertible
let A be Matrix of 0 ,K; :: thesis: A is invertible
A * A = 1. (K,0) by Th15;
then A is_reverse_of A by MATRIX_6:def 2;
hence A is invertible by MATRIX_6:def 3; :: thesis: verum