let n be Nat; :: thesis: for K being Field holds Solutions_of ((0. (K,n,0)),(0. (K,n,0))) =
let K be Field; :: thesis: Solutions_of ((0. (K,n,0)),(0. (K,n,0))) =
per cases ( n = 0 or n > 0 ) ;
suppose n = 0 ; :: thesis: Solutions_of ((0. (K,n,0)),(0. (K,n,0))) =
hence Solutions_of ((0. (K,n,0)),(0. (K,n,0))) = by Th51; :: thesis: verum
end;
suppose A1: n > 0 ; :: thesis: Solutions_of ((0. (K,n,0)),(0. (K,n,0))) =
set B = 0. (K,n,0);
set A = 0. (K,n,0);
reconsider E = {} as Matrix of 0 , 0 ,K by MATRIX_0:13;
A2: width (0. (K,n,0)) = 0 by ;
then A3: for i, j being Nat st [i,j] in Indices (0. (K,n,0)) holds
(0. (K,n,0)) * (i,j) = ((0. (K,n,0)) * E) * (i,j) by ZFMISC_1:90;
A4: Solutions_of ((0. (K,n,0)),(0. (K,n,0))) c=
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Solutions_of ((0. (K,n,0)),(0. (K,n,0))) or x in )
assume x in Solutions_of ((0. (K,n,0)),(0. (K,n,0))) ; :: thesis:
then reconsider X = x as Matrix of 0 , 0 ,K by ;
len X = 0 by MATRIX_0:def 2;
then X = {} ;
hence x in by TARSKI:def 1; :: thesis: verum
end;
A5: len E = 0 ;
A6: width E = 0 by MATRIX_0:24;
then A7: width ((0. (K,n,0)) * E) = 0 by ;
A8: len (0. (K,n,0)) = n by ;
then len ((0. (K,n,0)) * E) = n by ;
then (0. (K,n,0)) * E = 0. (K,n,0) by ;
then E in Solutions_of ((0. (K,n,0)),(0. (K,n,0))) by A2, A5, A6;
hence Solutions_of ((0. (K,n,0)),(0. (K,n,0))) = by ; :: thesis: verum
end;
end;