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 ) by Def5, Def6;
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 )
A2: (1_ K) + (1_ K) <> 0. K by VECTSP_1:def 29;
assume A3: [i,j] in Indices M1 ; :: thesis: M1 * i,j = (0. K,n,n) * i,j
then A4: [i,j] in Indices (0. K,n,n) by MATRIX_1:27;
M1 * i,j = - (M1 * i,j) by A1, A3, MATRIX_3:def 2;
then (M1 * i,j) + (M1 * i,j) = 0. K by RLVECT_1:16;
then ((1_ K) * (M1 * i,j)) + (M1 * i,j) = 0. K by VECTSP_1:def 19;
then ((1_ K) * (M1 * i,j)) + ((1_ K) * (M1 * i,j)) = 0. K by VECTSP_1:def 19;
then ((1_ K) + (1_ K)) * (M1 * i,j) = 0. K by VECTSP_1:def 18;
then M1 * i,j = 0. K by A2, VECTSP_1:44;
hence M1 * i,j = (0. K,n,n) * i,j by A4, MATRIX_3:3; :: thesis: verum

end;

hence M1 = 0. K,n,n by MATRIX_1:28; :: thesis: verum