let n be Nat; :: thesis: for K being Field
for M1 being Matrix of n,K holds
( ( M1 is invertible & (M1 @ ) * M1 = 1. K,n ) iff M1 is Orthogonal )
let K be Field; :: thesis: for M1 being Matrix of n,K holds
( ( M1 is invertible & (M1 @ ) * M1 = 1. K,n ) iff M1 is Orthogonal )
let M1 be Matrix of n,K; :: thesis: ( ( M1 is invertible & (M1 @ ) * M1 = 1. K,n ) iff M1 is Orthogonal )
A1: ( width M1 = n & len M1 = n & width (M1 ~ ) = n & len (M1 ~ ) = n ) by MATRIX_1:25;
A2: ( width (M1 @ ) = n & len (M1 @ ) = n ) by MATRIX_1:25;
thus ( M1 is invertible & (M1 @ ) * M1 = 1. K,n implies M1 is Orthogonal ) :: thesis: ( M1 is Orthogonal implies ( M1 is invertible & (M1 @ ) * M1 = 1. K,n ) )

proof

assume A3: ( M1 is invertible & (M1 @ ) * M1 = 1. K,n ) ; :: thesis: M1 is Orthogonal
then A4: M1 ~ is_reverse_of M1 by Def4;
then ((M1 ~ ) * M1) * (M1 ~ ) = ((M1 @ ) * M1) * (M1 ~ ) by A3, Def2;
then (M1 ~ ) * (M1 * (M1 ~ )) = ((M1 @ ) * M1) * (M1 ~ ) by A1, MATRIX_3:35;
then (M1 ~ ) * (M1 * (M1 ~ )) = (M1 @ ) * (M1 * (M1 ~ )) by A1, A2, MATRIX_3:35;
then (M1 ~ ) * (1. K,n) = (M1 @ ) * (M1 * (M1 ~ )) by A4, Def2;
then (M1 ~ ) * (1. K,n) = (M1 @ ) * (1. K,n) by A4, Def2;
then M1 ~ = (M1 @ ) * (1. K,n) by MATRIX_3:21;
then M1 ~ = M1 @ by MATRIX_3:21;
hence M1 is Orthogonal by A3, Def7; :: thesis: verum

end;

assume A5: M1 is Orthogonal ; :: thesis: ( M1 is invertible & (M1 @ ) * M1 = 1. K,n )
then ( M1 is invertible & M1 @ = M1 ~ ) by Def7;
then ( (M1 @ ) * M1 = (M1 ~ ) * M1 & M1 ~ is_reverse_of M1 ) by Def4;
hence ( M1 is invertible & (M1 @ ) * M1 = 1. K,n ) by A5, Def2, Def7; :: thesis: verum