let M be Matrix of 3,F_Real; :: thesis: ( 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) ; :: thesis: 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 ; :: thesis: verum