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 that
A1: M1 is_congruent_Matrix_of M2 and
A2: n > 0 ; :: thesis: M2 is_congruent_Matrix_of M1
consider M being Matrix of n,K such that
A3: M is invertible and
A4: M1 = ((M @) * M2) * M by A1;
A5: M ~ is_reverse_of M by A3, MATRIX_6:def 4;
take M ~ ; :: according to MATRIX_8:def 6 :: thesis: ( M ~ is invertible & M2 = (((M ~) @) * M1) * (M ~) )
A6: width (M ~) = n by MATRIX_0:24;
A7: ( len (M @) = n & width (M @) = n ) by MATRIX_0:24;
A8: width M = n by MATRIX_0:24;
A9: len (M ~) = n by MATRIX_0:24;
( len M = n & width ((M @) * M2) = n ) by MATRIX_0:24;
then A10: M1 * (M ~) = ((M @) * M2) * (M * (M ~)) by A4, A8, A9, MATRIX_3:33
.= ((M @) * M2) * (1. (K,n)) by A5, MATRIX_6:def 2
.= (M @) * M2 by MATRIX_3:19 ;
A11: len M2 = n by MATRIX_0:24;
A12: width ((M ~) @) = n by MATRIX_0:24;
( len M1 = n & width M1 = n ) by MATRIX_0:24;
then (((M ~) @) * M1) * (M ~) = ((M ~) @) * (M1 * (M ~)) by A9, A12, MATRIX_3:33
.= (((M ~) @) * (M @)) * M2 by A7, A11, A12, A10, MATRIX_3:33
.= ((M * (M ~)) @) * M2 by A2, A8, A9, A6, MATRIX_3:22
.= ((1. (K,n)) @) * M2 by A5, MATRIX_6:def 2
.= (1. (K,n)) * M2 by MATRIX_6:10
.= M2 by MATRIX_3:18 ;
hence ( M ~ is invertible & M2 = (((M ~) @) * M1) * (M ~) ) by A3; :: thesis: verum