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

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;

end;

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;(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