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;