let K be Fanoian Field; :: thesis: for n being Nat
for M1 being Matrix of n,K st M1 is symmetric & M1 is antisymmetric holds
M1 = 0. (K,n,n)
let n be Nat; :: thesis: for M1 being Matrix of n,K st M1 is symmetric & M1 is antisymmetric holds
M1 = 0. (K,n,n)
let M1 be Matrix of n,K; :: thesis: ( M1 is symmetric & M1 is antisymmetric implies M1 = 0. (K,n,n) )
assume ( M1 is symmetric & M1 is antisymmetric ) ; :: thesis: M1 = 0. (K,n,n)
then A1: ( M1 @ = M1 & M1 @ = - M1 ) ;
for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = (0. (K,n,n)) * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = (0. (K,n,n)) * (i,j) )
assume A2: [i,j] in Indices M1 ; :: thesis: M1 * (i,j) = (0. (K,n,n)) * (i,j)
then M1 * (i,j) = - (M1 * (i,j)) by A1, MATRIX_3:def 2;
then (M1 * (i,j)) + (M1 * (i,j)) = 0. K by RLVECT_1:5;
then ((1_ K) * (M1 * (i,j))) + ((1_ K) * (M1 * (i,j))) = 0. K ;
then ( (1_ K) + (1_ K) <> 0. K & ((1_ K) + (1_ K)) * (M1 * (i,j)) = 0. K ) by VECTSP_1:def 7, VECTSP_1:def 19;
then A3: M1 * (i,j) = 0. K by VECTSP_1:12;
[i,j] in Indices (0. (K,n,n)) by A2, MATRIX_0:26;
hence M1 * (i,j) = (0. (K,n,n)) * (i,j) by A3, MATRIX_3:1; :: thesis: verum

end;

hence M1 = 0. (K,n,n) by MATRIX_0:27; :: thesis: verum