let n be Nat; :: thesis: for K being Field
for M1, M2 being Matrix of n,K st M1 is_congruent_Matrix_of M2 & n > 0 holds
M2 is_congruent_Matrix_of M1
let K be Field; :: thesis: for M1, M2 being Matrix of n,K st M1 is_congruent_Matrix_of M2 & n > 0 holds
M2 is_congruent_Matrix_of M1
let M1, M2 be Matrix of n,K; :: thesis: ( M1 is_congruent_Matrix_of M2 & n > 0 implies M2 is_congruent_Matrix_of M1 )
assume A1: ( M1 is_congruent_Matrix_of M2 & n > 0 ) ; :: thesis: M2 is_congruent_Matrix_of M1
then consider M being Matrix of n,K such that
A2: ( M is invertible & M1 = ((M @ ) * M2) * M ) by Def6;
A3: ( len M = n & width M = n ) by MATRIX_1:25;
A4: ( len (M ~ ) = n & width (M ~ ) = n ) by MATRIX_1:25;
A5: ( len (M @ ) = n & width (M @ ) = n ) by MATRIX_1:25;
A6: ( len M2 = n & width M2 = n & len M1 = n & width M1 = n ) by MATRIX_1:25;
A7: ( len ((M @ ) * M2) = n & width ((M @ ) * M2) = n ) by MATRIX_1:25;
A8: M ~ is_reverse_of M by A2, MATRIX_6:def 4;
A9: ( len ((M ~ ) @ ) = n & width ((M ~ ) @ ) = n ) by MATRIX_1:25;
A10: M1 * (M ~ ) = ((M @ ) * M2) * (M * (M ~ )) by A2, A3, A4, A7, MATRIX_3:35
.= ((M @ ) * M2) * (1. K,n) by A8, MATRIX_6:def 2
.= (M @ ) * M2 by MATRIX_3:21 ;
A11: (((M ~ ) @ ) * M1) * (M ~ ) = ((M ~ ) @ ) * (M1 * (M ~ )) by A4, A6, A9, MATRIX_3:35
.= (((M ~ ) @ ) * (M @ )) * M2 by A5, A6, A9, A10, MATRIX_3:35
.= ((M * (M ~ )) @ ) * M2 by A1, A3, A4, MATRIX_3:24
.= ((1. K,n) @ ) * M2 by A8, MATRIX_6:def 2
.= (1. K,n) * M2 by MATRIX_6:10
.= M2 by MATRIX_3:20 ;
take M ~ ; :: according to MATRIX_8:def 6 :: thesis: ( M ~ is invertible & M2 = (((M ~ ) @ ) * M1) * (M ~ ) )
thus ( M ~ is invertible & M2 = (((M ~ ) @ ) * M1) * (M ~ ) ) by A2, A11, MATRIX_6:16; :: thesis: verum