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