let A be Matrix of 0 ,REAL; :: thesis: Det A = 1
thus Det A = 1. F_Real by Th41
.= 1 ; :: thesis: verum