let n be Element of NAT ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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) ) ) :: thesis: ( ex B being Matrix of n,K st
( B * A = 1. (K,n) & A * B = 1. (K,n) ) implies A is invertible )

proof

assume A is invertible ; :: thesis: ex B being Matrix of n,K st
( B * A = 1. (K,n) & A * B = 1. (K,n) )
then ( (A ~) * A = 1. (K,n) & A * (A ~) = 1. (K,n) ) by Th18;
hence ex B being Matrix of n,K st
( B * A = 1. (K,n) & A * B = 1. (K,n) ) ; :: thesis: verum

end;

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; :: thesis: verum