Solutions_of (A,b) c= the carrier of ((width A) -VectSp_over K)
proof
let x be object ; :: 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:92, 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