let K be Field; :: thesis: for V2, V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for v1 being Element of V1
for A being Matrix of len b1, len b2,K st len b1 > 0 & len b2 > 0 holds
( v1 in ker (Mx2Tran A,b1,b2) iff v1 |-- b1 in Space_of_Solutions_of (A @ ) )
let V2, V1 be finite-dimensional VectSp of K; :: thesis: for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for v1 being Element of V1
for A being Matrix of len b1, len b2,K st len b1 > 0 & len b2 > 0 holds
( v1 in ker (Mx2Tran A,b1,b2) iff v1 |-- b1 in Space_of_Solutions_of (A @ ) )
let b1 be OrdBasis of V1; :: thesis: for b2 being OrdBasis of V2
for v1 being Element of V1
for A being Matrix of len b1, len b2,K st len b1 > 0 & len b2 > 0 holds
( v1 in ker (Mx2Tran A,b1,b2) iff v1 |-- b1 in Space_of_Solutions_of (A @ ) )
let b2 be OrdBasis of V2; :: thesis: for v1 being Element of V1
for A being Matrix of len b1, len b2,K st len b1 > 0 & len b2 > 0 holds
( v1 in ker (Mx2Tran A,b1,b2) iff v1 |-- b1 in Space_of_Solutions_of (A @ ) )
let v1 be Element of V1; :: thesis: for A being Matrix of len b1, len b2,K st len b1 > 0 & len b2 > 0 holds
( v1 in ker (Mx2Tran A,b1,b2) iff v1 |-- b1 in Space_of_Solutions_of (A @ ) )
let A be Matrix of len b1, len b2,K; :: thesis: ( len b1 > 0 & len b2 > 0 implies ( v1 in ker (Mx2Tran A,b1,b2) iff v1 |-- b1 in Space_of_Solutions_of (A @ ) ) )
assume A1: ( len b1 > 0 & len b2 > 0 ) ; :: thesis: ( v1 in ker (Mx2Tran A,b1,b2) iff v1 |-- b1 in Space_of_Solutions_of (A @ ) )
set AT = A @ ;
set SA = Space_of_Solutions_of (A @ );
set M = Mx2Tran A,b1,b2;
A2: ( len A = len b1 & width A = len b2 ) by A1, MATRIX_1:24;
then A3: ( len (A @ ) = len b2 & width (A @ ) = len b1 & ( width (A @ ) = 0 implies len (A @ ) = 0 ) ) by A1, MATRIX_2:12;
set L = LineVec2Mx (v1 |-- b1);
A4: ( width (LineVec2Mx (v1 |-- b1)) = len (v1 |-- b1) & len (v1 |-- b1) = len b1 & len ((len b2) |-> (0. K)) = len b2 ) by FINSEQ_1:def 18, MATRIX_1:24, MATRLIN:def 9;
then A5: ( len (ColVec2Mx (v1 |-- b1)) = len (v1 |-- b1) & width (ColVec2Mx (v1 |-- b1)) = 1 & width (ColVec2Mx ((len b2) |-> (0. K))) = 1 & width ((LineVec2Mx (v1 |-- b1)) * A) = width A & width (LineVec2Mx ((len b2) |-> (0. K))) = len b2 ) by A1, A2, MATRIX_1:24, MATRIX_3:def 4;
thus ( v1 in ker (Mx2Tran A,b1,b2) implies v1 |-- b1 in Space_of_Solutions_of (A @ ) ) :: thesis: ( v1 |-- b1 in Space_of_Solutions_of (A @ ) implies v1 in ker (Mx2Tran A,b1,b2) )

proof

assume A6: v1 in ker (Mx2Tran A,b1,b2) ; :: thesis: v1 |-- b1 in Space_of_Solutions_of (A @ )
(Mx2Tran A,b1,b2) . v1 = 0. V2 by A6, RANKNULL:10;
then (LineVec2Mx (v1 |-- b1)) * A = LineVec2Mx ((0. V2) |-- b2) by Th32, A1
.= LineVec2Mx ((len b2) |-> (0. K)) by Th20 ;
then ColVec2Mx ((len b2) |-> (0. K)) = (A @ ) * (ColVec2Mx (v1 |-- b1)) by A4, A1, A2, MATRIX_3:24;
then ColVec2Mx (v1 |-- b1) in Solutions_of (A @ ),(ColVec2Mx ((len b2) |-> (0. K))) by A3, A4, A5;
then v1 |-- b1 in Solutions_of (A @ ),((len b2) |-> (0. K)) ;
then v1 |-- b1 in the carrier of (Space_of_Solutions_of (A @ )) by A3, MATRIX15:def 5;
hence v1 |-- b1 in Space_of_Solutions_of (A @ ) by STRUCT_0:def 5; :: thesis: verum

end;

assume v1 |-- b1 in Space_of_Solutions_of (A @ ) ; :: thesis: v1 in ker (Mx2Tran A,b1,b2)
then v1 |-- b1 in the carrier of (Space_of_Solutions_of (A @ )) by STRUCT_0:def 5;
then v1 |-- b1 in Solutions_of (A @ ),((len b2) |-> (0. K)) by A3, MATRIX15:def 5;
then ex f being FinSequence of K st
( f = v1 |-- b1 & ColVec2Mx f in Solutions_of (A @ ),(ColVec2Mx ((len b2) |-> (0. K))) ) ;
then ex X being Matrix of K st
( X = ColVec2Mx (v1 |-- b1) & len X = width (A @ ) & width X = width (ColVec2Mx ((len b2) |-> (0. K))) & ColVec2Mx ((len b2) |-> (0. K)) = (A @ ) * X ) ;
then ColVec2Mx ((len b2) |-> (0. K)) = ((LineVec2Mx (v1 |-- b1)) * A) @ by A4, A1, A2, MATRIX_3:24;
then (LineVec2Mx (v1 |-- b1)) * A = LineVec2Mx ((len b2) |-> (0. K)) by A1, A2, A5, MATRIX_2:14
.= LineVec2Mx ((0. V2) |-- b2) by Th20 ;
then LineVec2Mx ((0. V2) |-- b2) = LineVec2Mx (((Mx2Tran A,b1,b2) . v1) |-- b2) by Th32, A1;
then (0. V2) |-- b2 = Line (LineVec2Mx (((Mx2Tran A,b1,b2) . v1) |-- b2)),1 by MATRIX15:25
.= ((Mx2Tran A,b1,b2) . v1) |-- b2 by MATRIX15:25 ;
then (Mx2Tran A,b1,b2) . v1 = 0. V2 by MATRLIN:39;
hence v1 in ker (Mx2Tran A,b1,b2) by RANKNULL:10; :: thesis: verum