let n be Element of NAT ; for K being Field
for A being Matrix of n,K holds
( A is invertible iff ex B being Matrix of n,K st
( B * A = 1. (K,n) & A * B = 1. (K,n) ) )
let K be Field; for A being Matrix of n,K holds
( A is invertible iff ex B being Matrix of n,K st
( B * A = 1. (K,n) & A * B = 1. (K,n) ) )
let A be Matrix of n,K; ( A is invertible iff ex B being Matrix of n,K st
( B * A = 1. (K,n) & A * B = 1. (K,n) ) )
thus
( A is invertible implies ex B being Matrix of n,K st
( B * A = 1. (K,n) & A * B = 1. (K,n) ) )
( ex B being Matrix of n,K st
( B * A = 1. (K,n) & A * B = 1. (K,n) ) implies A is invertible )
thus
( ex B being Matrix of n,K st
( B * A = 1. (K,n) & A * B = 1. (K,n) ) implies A is invertible )
by Th18; verum