let n, m be Nat; :: thesis:
let K be Field; :: thesis:
let M, M1 be Matrix of m,n,K; :: thesis:
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:
set V = n -VectSp_over K;
defpred S₁[ 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 S₁[k,x]

let k be Nat; :: thesis:
assume A4: k in Seg (len M) ; :: thesis:
len M = m by MATRIX_1:def 3;
then consider a being Element of K such that
A5: Line M1,k = a * (Line M,k) by A2, A4;
take a ; :: thesis:
thus S₁[k,a] by A5; :: thesis:

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
S₁[k,p . k] from FINSEQ_1:sch 5(A3);
defpred S₂[ set , set ] 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 set st x in the carrier of (n -VectSp_over K) holds
ex y being set st
( y in the carrier of K & S₂[x,y] )

let x be set ; :: thesis:
assume A9: x in the carrier of (n -VectSp_over K) ; :: thesis:
reconsider v = x as Element of (n -VectSp_over K) by A9;

per cases ;

suppose A10: v in lines M ; :: thesis:

then consider j being Nat such that
A11: ( j in Seg m & v = Line M,j ) by Th103;
len M = m by MATRIX_1:def 3;
then ( p . j in rng p & rng p c= the carrier of K ) by A6, A11, FINSEQ_1:def 4, FUNCT_1:def 5;
then reconsider pj = p . j as Element of the carrier of K ;
take pj ; :: thesis:
thus pj in the carrier of K ; :: thesis:
let w be Vector of (n -VectSp_over K); :: thesis:
assume A12: w = x ; :: thesis:
thus ( not w in lines M implies pj = 0. K ) by A10, A12; :: thesis:
thus ( w in lines M implies for k being Nat st k in Seg m & w = Line M,k holds
pj = p . k ) :: thesis:

assume w in lines M ; :: thesis:
let k be Nat; :: thesis:
assume A13: ( k in Seg m & w = Line M,k ) ; :: thesis:
len M = m by MATRIX_1:def 3;
then ( dom M = Seg m & M . k = Line M,k & M . j = Line M,j ) by A11, A13, FINSEQ_1:def 3, MATRIX_2:10;
hence pj = p . k by A1, A11, A12, A13, FUNCT_1:def 8; :: thesis:

end;

suppose A14: not v in lines M ; :: thesis:

take 0K = 0. K; :: thesis:
thus 0K in the carrier of K ; :: thesis:
let w be Vector of (n -VectSp_over K); :: thesis:
assume A15: w = x ; :: thesis:
thus ( not w in lines M implies 0K = 0. K ) ; :: thesis:
thus ( w in lines M implies for k being Nat st k in Seg m & w = Line M,k holds
0K = p . k ) by A14, A15; :: thesis:

end;

consider l being Function of the carrier of (n -VectSp_over K),the carrier of K such that
A16: for x being set st x in the carrier of (n -VectSp_over K) holds
S₂[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:11;
for v being Vector of (n -VectSp_over K) st not v in lines M holds
L . v = 0. K by A16;
then reconsider L = L as Linear_Combination of n -VectSp_over K by VECTSP_6:def 4;
Carrier L c= lines M

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in Carrier L ; :: thesis:
then consider v being Vector of (n -VectSp_over K) such that
A17: ( x = v & L . v <> 0. K ) by VECTSP_6:19;
thus x in lines M by A16, A17; :: thesis:

end;

then reconsider L = L as Linear_Combination of lines M by VECTSP_6:def 7;
set MX = MX2FinS M;
set LM = L (#) (MX2FinS M);
A18: ( len M = m & len (L (#) (MX2FinS M)) = len M & len M1 = m ) by MATRIX_1:def 3, VECTSP_6:def 8;

let k be Nat; :: thesis:
assume A19: ( 1 <= k & k <= m ) ; :: thesis:
k in NAT by ORDINAL1:def 13;
then A20: k in Seg m by A19;
then consider a being Element of K such that
A21: ( p . k = a & Line M1,k = a * (Line M,k) ) by A7, A18;
A22: Line M,k in lines M by A20, Th103;
then reconsider LMk = Line M,k as Element of n -tuples_on the carrier of K by Th102;
( dom (L (#) (MX2FinS M)) = Seg m & dom (MX2FinS M) = Seg m ) by A18, FINSEQ_1:def 3;
then ( (L (#) (MX2FinS M)) . k = (L . ((MX2FinS M) /. k)) * ((MX2FinS M) /. k) & (MX2FinS M) /. k = M . k & L . LMk = p . k & LMk = M . k ) by A16, A20, A22, MATRIX_2:10, PARTFUN1:def 8, VECTSP_6:def 8;
then ( (L (#) (MX2FinS M)) . k = a * LMk & M1 . k = Line M1,k ) by A20, A21, Th102, MATRIX_2:10;
hence M1 . k = (L (#) (MX2FinS M)) . k by A21; :: thesis:

end;

then M1 = L (#) (MX2FinS M) by A18, FINSEQ_1:18;
hence ex L being Linear_Combination of lines M st L (#) (MX2FinS M) = M1 ; :: thesis: