let K be Field; :: thesis: for A being Matrix of K
for b, f being FinSequence of K st ColVec2Mx f in Solutions_of A,(ColVec2Mx b) holds
len f = width A
let A be Matrix of K; :: thesis: for b, f being FinSequence of K st ColVec2Mx f in Solutions_of A,(ColVec2Mx b) holds
len f = width A
let b, f be FinSequence of K; :: thesis: ( ColVec2Mx f in Solutions_of A,(ColVec2Mx b) implies len f = width A )
assume A1: ColVec2Mx f in Solutions_of A,(ColVec2Mx b) ; :: thesis: len f = width A
consider g being FinSequence of K such that
A2: ( ColVec2Mx f = ColVec2Mx g & len g = width A ) by A1, Th58;
( len (ColVec2Mx f) = len f & len (ColVec2Mx g) = len g ) by MATRIX_1:def 3;
hence len f = width A by A2; :: thesis: verum