let M be Matrix of 3,F_Real; ( M = symmetric_3 (0,0,0,0,0,0) implies Det M = 0. F_Real )
assume A1:
M = symmetric_3 (0,0,0,0,0,0)
; Det M = 0. F_Real
reconsider z = 0 as Element of F_Real ;
M = <*<*z,z,z*>,<*z,z,z*>,<*z,z,z*>*>
by A1, PASCAL:def 3;
then
Det M = ((((((z * z) * z) - ((z * z) * z)) - ((z * z) * z)) + ((z * z) * z)) - ((z * z) * z)) + ((z * z) * z)
by MATRIX_9:46;
hence
Det M = 0. F_Real
; verum