Solutions_of A,b c= the carrier of ((width A) -VectSp_over K)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Solutions_of A,b or x in the carrier of ((width A) -VectSp_over K) )
assume x in Solutions_of A,b ; :: thesis: x in the carrier of ((width A) -VectSp_over K)
then consider f being FinSequence of K such that
A1: x = f and
A2: ColVec2Mx f in Solutions_of A,(ColVec2Mx b) ;
len f = width A by A2, Th59;
then ( (width A) -tuples_on the carrier of K = the carrier of ((width A) -VectSp_over K) & f is Element of (width A) -tuples_on the carrier of K ) by FINSEQ_2:110, MATRIX13:102;
hence x in the carrier of ((width A) -VectSp_over K) by A1; :: thesis: verum

end;

hence Solutions_of A,b is Subset of ((width A) -VectSp_over K) ; :: thesis: verum