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 B2: 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 B2, MATRIX_6:def 4; :: thesis: verum

end;