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 ColVec2Mx f in Solutions_of (A,(ColVec2Mx b)) ; :: thesis: len f = width A
then A1: ex g being FinSequence of K st
( ColVec2Mx f = ColVec2Mx g & len g = width A ) by Th58;
len (ColVec2Mx f) = len f by MATRIX_0:def 2;
hence len f = width A by A1, MATRIX_0:def 2; :: thesis: verum