let n be Nat; :: thesis: for K being Field
for M1, M2 being Matrix of n,K st n > 0 & M1 is Orthogonal & M2 is Orthogonal holds
(M1 ~) * M2 is Orthogonal

let K be Field; :: thesis: for M1, M2 being Matrix of n,K st n > 0 & M1 is Orthogonal & M2 is Orthogonal holds
(M1 ~) * M2 is Orthogonal

let M1, M2 be Matrix of n,K; :: thesis: ( n > 0 & M1 is Orthogonal & M2 is Orthogonal implies (M1 ~) * M2 is Orthogonal )
assume that
A1: n > 0 and
A2: M1 is Orthogonal and
A3: M2 is Orthogonal ; :: thesis: (M1 ~) * M2 is Orthogonal
A4: M1 is invertible by A2;
then A5: M1 ~ is invertible ;
A6: M2 is invertible by A3;
then A7: (M1 ~) * M2 is invertible by ;
((M1 ~) * M2) ~ = (M2 ~) * ((M1 ~) ~) by A6, A5, Th36;
then A8: ((M1 ~) * M2) ~ = (M2 ~) * M1 by ;
A9: len M2 = n by MATRIX_0:24;
A10: ( width (M1 ~) = n & width M2 = n ) by MATRIX_0:24;
A11: ( width M1 = n & len M1 = n ) by MATRIX_0:24;
( M1 @ = M1 ~ & M2 @ = M2 ~ ) by A2, A3;
then ((M1 ~) * M2) @ = (M2 ~) * ((M1 @) @) by
.= (M2 ~) * M1 by ;
hence (M1 ~) * M2 is Orthogonal by A7, A8; :: thesis: verum