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

end;

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