let n, m be Nat; :: thesis: for M being Matrix of n,m,F_Real holds rng (Mx2Tran M) = [#] (Lin (lines M))
let M be Matrix of n,m,F_Real; :: thesis: rng (Mx2Tran M) = [#] (Lin (lines M))
consider X being set such that
A1: X c= dom M and
A2: lines M = rng (M | X) and
A3: M | X is one-to-one by MATRTOP1:6;
set V = m -VectSp_over F_Real;
set TM = Mx2Tran M;
A5: len M = n by MATRIX_1:def 2;
then reconsider X = X as Subset of (Seg n) by A1, FINSEQ_1:def 3;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: [#] (Lin (lines M)) c= rng (Mx2Tran M)

let y be set ; :: thesis: ( y in rng (Mx2Tran M) implies y in [#] (Lin (lines M)) )
assume y in rng (Mx2Tran M) ; :: thesis: y in [#] (Lin (lines M))
then consider x being set such that
A6: x in dom (Mx2Tran M) and
A7: (Mx2Tran M) . x = y by FUNCT_1:def 3;
reconsider x = x as Element of (TOP-REAL n) by A6;
consider L being Linear_Combination of lines M such that
A8: Sum L = y and
for i being Nat st i in X holds
L . (Line (M,i)) = Sum (Seq (x | (M " {(Line (M,i))}))) by A2, A3, A7, Th15;
Sum L in Lin (lines M) by VECTSP_7:7;
hence y in [#] (Lin (lines M)) by A8, STRUCT_0:def 5; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in [#] (Lin (lines M)) or y in rng (Mx2Tran M) )
assume y in [#] (Lin (lines M)) ; :: thesis: y in rng (Mx2Tran M)
then y in Lin (lines M) by STRUCT_0:def 5;
then consider L being Linear_Combination of lines M such that
A9: y = Sum L by VECTSP_7:7;
defpred S₁[ set , set ] means ( ( $1 in X implies $2 = L . (M . $1) ) & ( not $1 in X implies $2 = 0 ) );
A10: for i being Nat st i in Seg n holds
ex x being set st S₁[i,x]

proof

let i be Nat; :: thesis: ( i in Seg n implies ex x being set st S₁[i,x] )
assume i in Seg n ; :: thesis: ex x being set st S₁[i,x]
( i in X or not i in X ) ;
hence ex x being set st S₁[i,x] ; :: thesis: verum

end;

consider f being FinSequence such that
A11: ( dom f = Seg n & ( for j being Nat st j in Seg n holds
S₁[j,f . j] ) ) from FINSEQ_1:sch 1(A10);
A12: dom M = Seg n by A5, FINSEQ_1:def 3;
rng f c= REAL

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng f or z in REAL )
assume z in rng f ; :: thesis: z in REAL
then consider x being set such that
A13: x in dom f and
A14: f . x = z by FUNCT_1:def 3;
reconsider x = x as Nat by A13;
A15: S₁[x,f . x] by A11, A13;
M . x = Line (M,x) by A12, A11, A13, MATRIX_2:16;
then M . x in lines M by A11, A13, MATRIX13:103;
then reconsider Mx = M . x as Element of (m -VectSp_over F_Real) ;

per cases ( not x in X or x in X ) ;

suppose not x in X ; :: thesis: z in REAL

then f . x = 0 by A11, A13;
hence z in REAL by A14; :: thesis: verum

end;

suppose x in X ; :: thesis: z in REAL

thus z in REAL by A14, A15, XREAL_0:def 1; :: thesis: verum

end;

end;

end;

then reconsider f = f as FinSequence of REAL by FINSEQ_1:def 4;
len f = n by A5, A11, FINSEQ_1:def 3;
then A16: f is n -element by CARD_1:def 7;
then consider K being Linear_Combination of lines M such that
A17: Sum K = (Mx2Tran M) . f and
A18: for i being Nat st i in X holds
K . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) by A2, A3, Th15;

now

let v be Element of (m -VectSp_over F_Real); :: thesis: L . b₁ = K . b₁

per cases ( v in lines M or not v in lines M ) ;

suppose v in lines M ; :: thesis: L . b₁ = K . b₁

then consider i being set such that
A19: i in dom (M | X) and
A20: (M | X) . i = v by A2, FUNCT_1:def 3;
A21: M . i = v by A19, A20, FUNCT_1:47;
set D = dom (f | (M " {v}));
Seq (f | (M " {v})) = @ (@ (Seq (f | (M " {v})))) ;
then reconsider F = Seq (f | (M " {v})) as FinSequence of REAL ;
A22: rng (Sgm (dom (f | (M " {v})))) = dom (f | (M " {v})) by FINSEQ_1:50;
then A23: dom F = dom (Sgm (dom (f | (M " {v})))) by RELAT_1:27;
A24: i in dom M by A19, RELAT_1:57;
A25: i in X by A19, RELAT_1:57;
reconsider i = i as Nat by A19;
M . i = Line (M,i) by A24, MATRIX_2:16;
then A26: K . v = Sum (Seq (f | (M " {v}))) by A18, A25, A21;
v in {v} by TARSKI:def 1;
then i in M " {v} by A24, A21, FUNCT_1:def 7;
then i in dom (f | (M " {v})) by A11, A25, RELAT_1:57;
then consider j being set such that
A27: j in dom (Sgm (dom (f | (M " {v})))) and
A28: (Sgm (dom (f | (M " {v})))) . j = i by A22, FUNCT_1:def 3;
reconsider j = j as Element of NAT by A27;
( F . j = (f | (M " {v})) . i & i in dom (f | (M " {v})) ) by A23, A27, A28, FUNCT_1:11, FUNCT_1:12;
then A29: F . j = f . i by FUNCT_1:47;
dom (f | (M " {v})) c= dom f by RELAT_1:60;
then A30: Sgm (dom (f | (M " {v}))) is one-to-one by A11, FINSEQ_3:92;

now

let w be Element of NAT ; :: thesis: ( w in dom F & w <> j implies F . w = 0 )
assume that
A31: w in dom F and
A32: w <> j ; :: thesis: F . w = 0
A33: (Sgm (dom (f | (M " {v})))) . w in dom (f | (M " {v})) by A22, A23, A31, FUNCT_1:def 3;
then (Sgm (dom (f | (M " {v})))) . w in M " {v} by RELAT_1:57;
then M . ((Sgm (dom (f | (M " {v})))) . w) in {v} by FUNCT_1:def 7;
then A34: M . ((Sgm (dom (f | (M " {v})))) . w) = v by TARSKI:def 1;
A35: not (Sgm (dom (f | (M " {v})))) . w in X

proof

assume (Sgm (dom (f | (M " {v})))) . w in X ; :: thesis: contradiction
then A36: (Sgm (dom (f | (M " {v})))) . w in dom (M | X) by A12, RELAT_1:57;
then v = (M | X) . ((Sgm (dom (f | (M " {v})))) . w) by A34, FUNCT_1:47;
then i = (Sgm (dom (f | (M " {v})))) . w by A3, A19, A20, A36, FUNCT_1:def 4;
hence contradiction by A23, A30, A27, A28, A31, A32, FUNCT_1:def 4; :: thesis: verum

end;

F . w = (f | (M " {v})) . ((Sgm (dom (f | (M " {v})))) . w) by A31, FUNCT_1:12;
then A37: F . w = f . ((Sgm (dom (f | (M " {v})))) . w) by A33, FUNCT_1:47;
(Sgm (dom (f | (M " {v})))) . w in dom f by A33, RELAT_1:57;
hence F . w = 0 by A11, A37, A35; :: thesis: verum

end;

then A38: F has_onlyone_value_in j by A23, A27, ENTROPY1:def 2;
f . i = L . v by A11, A25, A21;
hence L . v = K . v by A26, A29, A38, ENTROPY1:13; :: thesis: verum

end;

suppose A39: not v in lines M ; :: thesis: L . b₁ = K . b₁

Carrier L c= lines M by VECTSP_6:def 4;
then not v in Carrier L by A39;
then A40: L . v = 0. F_Real by VECTSP_6:2;
Carrier K c= lines M by VECTSP_6:def 4;
then not v in Carrier K by A39;
hence L . v = K . v by A40, VECTSP_6:2; :: thesis: verum

end;

end;

end;

then A41: Sum K = Sum L by VECTSP_6:def 7;
( dom (Mx2Tran M) = [#] (TOP-REAL n) & f is Point of (TOP-REAL n) ) by A16, Lm3, FUNCT_2:def 1;
hence y in rng (Mx2Tran M) by A9, A17, A41, FUNCT_1:def 3; :: thesis: verum