let n be Element of NAT ; :: thesis: for K being Field
for A, B being Matrix of n,K holds
( A is invertible & B = A ~ iff ( B * A = 1. (K,n) & A * B = 1. (K,n) ) )
let K be Field; :: thesis: for A, B being Matrix of n,K holds
( A is invertible & B = A ~ iff ( B * A = 1. (K,n) & A * B = 1. (K,n) ) )
let A, B be Matrix of n,K; :: thesis: ( A is invertible & B = A ~ iff ( B * A = 1. (K,n) & A * B = 1. (K,n) ) )

hereby :: thesis: ( B * A = 1. (K,n) & A * B = 1. (K,n) implies ( A is invertible & B = A ~ ) )

assume ( A is invertible & B = A ~ ) ; :: thesis: ( B * A = 1. (K,n) & A * B = 1. (K,n) )
then B is_reverse_of A by MATRIX_6:def 4;
hence ( B * A = 1. (K,n) & A * B = 1. (K,n) ) by MATRIX_6:def 2; :: thesis: verum

end;

hereby :: thesis: verum

assume ( B * A = 1. (K,n) & A * B = 1. (K,n) ) ; :: thesis: ( A is invertible & B = A ~ )
then A1: B is_reverse_of A by MATRIX_6:def 2;
hence A is invertible by MATRIX_6:def 3; :: thesis: B = A ~
hence B = A ~ by A1, MATRIX_6:def 4; :: thesis: verum

end;