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