let n be Nat; :: thesis: for K being Field
for M1 being Matrix of n,K st M1 is symmetric holds
(M1 @) * M1 is symmetric
let K be Field; :: thesis: for M1 being Matrix of n,K st M1 is symmetric holds
(M1 @) * M1 is symmetric
let M1 be Matrix of n,K; :: thesis: ( M1 is symmetric implies (M1 @) * M1 is symmetric )
assume A1: M1 is symmetric ; :: thesis: (M1 @) * M1 is symmetric

per cases ( n > 0 or n = 0 ) by NAT_1:3;

suppose A2: n > 0 ; :: thesis: (M1 @) * M1 is symmetric

A3: ( width M1 = n & len M1 = n ) by MATRIX_0:24;
((M1 @) * M1) @ = (M1 * M1) @ by A1, MATRIX_6:def 5
.= (M1 @) * (M1 @) by A2, A3, MATRIX_3:22
.= (M1 @) * M1 by A1, MATRIX_6:def 5 ;
hence (M1 @) * M1 is symmetric by MATRIX_6:def 5; :: thesis: verum

end;

suppose n = 0 ; :: thesis: (M1 @) * M1 is symmetric

then ((M1 @) * M1) @ = (M1 @) * M1 by MATRIX_0:45;
hence (M1 @) * M1 is symmetric by MATRIX_6:def 5; :: thesis: verum

end;

end;