let M, N be Matrix of 3,F_Real; :: thesis: ( N is symmetric implies ((M @) * N) * M is symmetric )
assume A1: N is symmetric ; :: thesis: ((M @) * N) * M is symmetric
A2: ( len N = 3 & width N = 3 & len M = 3 & width M = 3 ) by MATRIX_0:24;
then A3: ( width (M @) = len N & width N = len M ) by MATRIX_0:29;
( width (M @) = len N & width N <> 0 ) by A2, MATRIX_0:29;
then A4: ((M @) * N) @ = (N @) * ((M @) @) by MATRIX_3:22
.= (N @) * M by A2, MATRIX_0:57 ;
( width ((M @) * N) = len M & width M <> 0 ) by MATRIX_0:24, A2;
then (((M @) * N) * M) @ = (M @) * (((M @) * N) @) by MATRIX_3:22
.= (M @) * (N * M) by A4, A1, MATRIX_6:def 5
.= ((M @) * N) * M by A3, MATRIX_3:33 ;
hence ((M @) * N) * M is symmetric by MATRIX_6:def 5; :: thesis: verum