let m, n be Nat; :: thesis: for K being Field
for M, M1 being Matrix of m,n,K st M is without_repeated_line & ( for i being Nat st i in Seg m holds
ex a being Element of K st Line (M1,i) = a * (Line (M,i)) ) holds
ex L being Linear_Combination of lines M st L (#) (MX2FinS M) = M1
let K be Field; :: thesis: for M, M1 being Matrix of m,n,K st M is without_repeated_line & ( for i being Nat st i in Seg m holds
ex a being Element of K st Line (M1,i) = a * (Line (M,i)) ) holds
ex L being Linear_Combination of lines M st L (#) (MX2FinS M) = M1
let M, M1 be Matrix of m,n,K; :: thesis: ( M is without_repeated_line & ( for i being Nat st i in Seg m holds
ex a being Element of K st Line (M1,i) = a * (Line (M,i)) ) implies ex L being Linear_Combination of lines M st L (#) (MX2FinS M) = M1 )
assume that
A1: M is without_repeated_line and
A2: for i being Nat st i in Seg m holds
ex a being Element of K st Line (M1,i) = a * (Line (M,i)) ; :: thesis: ex L being Linear_Combination of lines M st L (#) (MX2FinS M) = M1
set V = n -VectSp_over K;
defpred S1[ set , set ] means for i being Nat st $1 = i holds
ex a being Element of K st
( a = $2 & Line (M1,i) = a * (Line (M,i)) );
A3: for k being Nat st k in Seg (len M) holds
ex x being Element of K st S1[k,x]
proof
A4: len M = m by MATRIX_0:def 2;
let k be Nat; :: thesis: ( k in Seg (len M) implies ex x being Element of K st S1[k,x] )
assume k in Seg (len M) ; :: thesis: ex x being Element of K st S1[k,x]
then consider a being Element of K such that
A5: Line (M1,k) = a * (Line (M,k)) by A2, A4;
take a ; :: thesis: S1[k,a]
thus S1[k,a] by A5; :: thesis: verum
end;
consider p being FinSequence of K such that
A6: dom p = Seg (len M) and
A7: for k being Nat st k in Seg (len M) holds
S1[k,p . k] from FINSEQ_1:sch 5(A3);
 defpred S2[ object , object ] means for v being Vector of (n -VectSp_over K) st $1 = v holds
( ( not v in lines M implies $2 = 0. K ) & ( v in lines M implies for k being Nat st k in Seg m & v = Line (M,k) holds
$2 = p . k ) );
A8: for x being object st x in the carrier of (n -VectSp_over K) holds
ex y being object st
( y in the carrier of K & S2[x,y] )
proof
let x be object ; :: thesis: ( x in the carrier of (n -VectSp_over K) implies ex y being object st
( y in the carrier of K & S2[x,y] ) )
assume x in the carrier of (n -VectSp_over K) ; :: thesis: ex y being object st
( y in the carrier of K & S2[x,y] )
then reconsider v = x as Element of (n -VectSp_over K) ;
per cases ( v in lines M or not v in lines M ) ;
suppose A9: v in lines M ; :: thesis: ex y being object st
( y in the carrier of K & S2[x,y] )
A10: rng p c= the carrier of K by FINSEQ_1:def 4;
consider j being Nat such that
A11: j in Seg m and
A12: v = Line (M,j) by A9, Th103;
len M = m by MATRIX_0:def 2;
then p . j in rng p by A6, A11, FUNCT_1:def 3;
then reconsider pj = p . j as Element of the carrier of K by A10;
take pj ; :: thesis: ( pj in the carrier of K & S2[x,pj] )
thus pj in the carrier of K ; :: thesis: S2[x,pj]
let w be Vector of (n -VectSp_over K); :: thesis: ( x = w implies ( ( not w in lines M implies pj = 0. K ) & ( w in lines M implies for k being Nat st k in Seg m & w = Line (M,k) holds
pj = p . k ) ) )
assume A13: w = x ; :: thesis: ( ( not w in lines M implies pj = 0. K ) & ( w in lines M implies for k being Nat st k in Seg m & w = Line (M,k) holds
pj = p . k ) )
thus ( not w in lines M implies pj = 0. K ) by A9, A13; :: thesis: ( w in lines M implies for k being Nat st k in Seg m & w = Line (M,k) holds
pj = p . k )
thus ( w in lines M implies for k being Nat st k in Seg m & w = Line (M,k) holds
pj = p . k ) :: thesis: verum
proof
len M = m by MATRIX_0:def 2;
then A14: dom M = Seg m by FINSEQ_1:def 3;
A15: M . j = Line (M,j) by A11, MATRIX_0:52;
assume w in lines M ; :: thesis: for k being Nat st k in Seg m & w = Line (M,k) holds
pj = p . k
let k be Nat; :: thesis: ( k in Seg m & w = Line (M,k) implies pj = p . k )
assume that
A16: k in Seg m and
A17: w = Line (M,k) ; :: thesis: pj = p . k
M . k = Line (M,k) by A16, MATRIX_0:52;
hence pj = p . k by A1, A11, A12, A13, A16, A17, A14, A15; :: thesis: verum
end;
end;
suppose A18: not v in lines M ; :: thesis: ex y being object st
( y in the carrier of K & S2[x,y] )
take 0K = 0. K; :: thesis: ( 0K in the carrier of K & S2[x,0K] )
thus 0K in the carrier of K ; :: thesis: S2[x,0K]
let w be Vector of (n -VectSp_over K); :: thesis: ( x = w implies ( ( not w in lines M implies 0K = 0. K ) & ( w in lines M implies for k being Nat st k in Seg m & w = Line (M,k) holds
0K = p . k ) ) )
assume A19: w = x ; :: thesis: ( ( not w in lines M implies 0K = 0. K ) & ( w in lines M implies for k being Nat st k in Seg m & w = Line (M,k) holds
0K = p . k ) )
thus ( not w in lines M implies 0K = 0. K ) ; :: thesis: ( w in lines M implies for k being Nat st k in Seg m & w = Line (M,k) holds
0K = p . k )
thus ( w in lines M implies for k being Nat st k in Seg m & w = Line (M,k) holds
0K = p . k ) by A18, A19; :: thesis: verum
end;
end;
end;
consider l being Function of the carrier of (n -VectSp_over K), the carrier of K such that
A20: for x being object st x in the carrier of (n -VectSp_over K) holds
S2[x,l . x] from FUNCT_2:sch 1(A8);
 reconsider L = l as Element of Funcs ( the carrier of (n -VectSp_over K), the carrier of K) by FUNCT_2:8;
for v being Vector of (n -VectSp_over K) st not v in lines M holds
L . v = 0. K by A20;
then reconsider L = L as Linear_Combination of n -VectSp_over K by VECTSP_6:def 1;
A21: Carrier L c= lines M
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier L or x in lines M )
assume x in Carrier L ; :: thesis: x in lines M
then ex v being Vector of (n -VectSp_over K) st
( x = v & L . v <> 0. K ) by VECTSP_6:1;
hence x in lines M by A20; :: thesis: verum
end;
set MX = MX2FinS M;
A22: len M = m by MATRIX_0:def 2;
reconsider L = L as Linear_Combination of lines M by A21, VECTSP_6:def 4;
set LM = L (#) (MX2FinS M);
A23: len (L (#) (MX2FinS M)) = len M by VECTSP_6:def 5;
A24: now :: thesis: for k being Nat st 1 <= k & k <= m holds
M1 . k = (L (#) (MX2FinS M)) . k
let k be Nat; :: thesis: ( 1 <= k & k <= m implies M1 . k = (L (#) (MX2FinS M)) . k )
assume that
A25: 1 <= k and
A26: k <= m ; :: thesis: M1 . k = (L (#) (MX2FinS M)) . k
A27: k in Seg m by A25, A26;
then consider a being Element of K such that
A28: p . k = a and
A29: Line (M1,k) = a * (Line (M,k)) by A7, A22;
dom (MX2FinS M) = Seg m by A22, FINSEQ_1:def 3;
then A30: (MX2FinS M) /. k = M . k by A27, PARTFUN1:def 6;
A31: Line (M,k) in lines M by A27, Th103;
then reconsider LMk = Line (M,k) as Element of n -tuples_on the carrier of K by Th102;
A32: LMk = M . k by A27, MATRIX_0:52;
dom (L (#) (MX2FinS M)) = Seg m by A22, A23, FINSEQ_1:def 3;
then A33: (L (#) (MX2FinS M)) . k = (L . ((MX2FinS M) /. k)) * ((MX2FinS M) /. k) by A27, VECTSP_6:def 5;
L . LMk = p . k by A20, A27, A31;
then (L (#) (MX2FinS M)) . k = a * LMk by A28, A33, A30, A32, Th102;
hence M1 . k = (L (#) (MX2FinS M)) . k by A27, A29, MATRIX_0:52; :: thesis: verum
end;
len M1 = m by MATRIX_0:def 2;
hence ex L being Linear_Combination of lines M st L (#) (MX2FinS M) = M1 by A22, A23, A24, FINSEQ_1:14; :: thesis: verum