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 ;
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 ;
then A3: M1 * (i,j) = 0. K by VECTSP_1:12;
[i,j] in Indices (0. (K,n,n)) by ;
hence M1 * (i,j) = (0. (K,n,n)) * (i,j) by ; :: thesis: verum
end;
hence M1 = 0. (K,n,n) by MATRIX_0:27; :: thesis: verum