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

proof

hence
Solutions_of (A,b) is Subset of ((width A) -VectSp_over K)
; :: thesis: verum
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;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