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;
A4: len M = n by MATRIX_0: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 object ; :: 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 object such that
A5: x in dom (Mx2Tran M) and
A6: (Mx2Tran M) . x = y by FUNCT_1:def 3;
reconsider x = x as Element of (TOP-REAL n) by A5;
consider L being Linear_Combination of lines M such that
A7: 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, A6, Th15;
Sum L in Lin (lines M) by VECTSP_7:7;
hence y in [#] (Lin (lines M)) by A7; :: thesis: verum

end;

let y be object ; :: 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) ;
then consider L being Linear_Combination of lines M such that
A8: y = Sum L by VECTSP_7:7;
defpred S₁[ set , object ] means ( ( $1 in X implies $2 = L . (M . $1) ) & ( not $1 in X implies $2 = 0 ) );
A9: for i being Nat st i in Seg n holds
ex x being object st S₁[i,x]

proof

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

end;

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

proof

let z be object ; :: 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 object such that
A12: x in dom f and
A13: f . x = z by FUNCT_1:def 3;
reconsider x = x as Nat by A12;
A14: S₁[x,f . x] by A10, A12;
M . x = Line (M,x) by A11, A10, A12, MATRIX_0:60;
then M . x in lines M by A10, A12, 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 = In (0,REAL) by A10, A12;
hence z in REAL by A13; :: thesis: verum

end;

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

thus z in REAL by A13, A14, 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 A4, A10, FINSEQ_1:def 3;
then A15: f is n -element by CARD_1:def 7;
then consider K being Linear_Combination of lines M such that
A16: Sum K = (Mx2Tran M) . f and
A17: 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 :: thesis: for v being Element of (m -VectSp_over F_Real) holds L . v = K . v

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 object such that
A18: i in dom (M | X) and
A19: (M | X) . i = v by A2, FUNCT_1:def 3;
A20: M . i = v by A18, A19, 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 ;
A21: rng (Sgm (dom (f | (M " {v})))) = dom (f | (M " {v})) by FINSEQ_1:50;
then A22: dom F = dom (Sgm (dom (f | (M " {v})))) by RELAT_1:27;
A23: i in dom M by A18, RELAT_1:57;
A24: i in X by A18;
reconsider i = i as Nat by A18;
M . i = Line (M,i) by A23, MATRIX_0:60;
then A25: K . v = Sum (Seq (f | (M " {v}))) by A17, A24, A20;
v in {v} by TARSKI:def 1;
then i in M " {v} by A23, A20, FUNCT_1:def 7;
then i in dom (f | (M " {v})) by A10, A24, RELAT_1:57;
then consider j being object such that
A26: j in dom (Sgm (dom (f | (M " {v})))) and
A27: (Sgm (dom (f | (M " {v})))) . j = i by A21, FUNCT_1:def 3;
reconsider j = j as Element of NAT by A26;
( F . j = (f | (M " {v})) . i & i in dom (f | (M " {v})) ) by A22, A26, A27, FUNCT_1:11, FUNCT_1:12;
then A28: F . j = f . i by FUNCT_1:47;
A29: Sgm (dom (f | (M " {v}))) is one-to-one by FINSEQ_3:92;

now :: thesis: for w being Nat st w in dom F & w <> j holds
F . w = 0

let w be Nat; :: thesis: ( w in dom F & w <> j implies F . w = 0 )
assume that
A30: w in dom F and
A31: w <> j ; :: thesis: F . w = 0
A32: (Sgm (dom (f | (M " {v})))) . w in dom (f | (M " {v})) by A21, A22, A30, 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 A33: M . ((Sgm (dom (f | (M " {v})))) . w) = v by TARSKI:def 1;
A34: not (Sgm (dom (f | (M " {v})))) . w in X

proof

assume (Sgm (dom (f | (M " {v})))) . w in X ; :: thesis: contradiction
then A35: (Sgm (dom (f | (M " {v})))) . w in dom (M | X) by A11, RELAT_1:57;
then v = (M | X) . ((Sgm (dom (f | (M " {v})))) . w) by A33, FUNCT_1:47;
then i = (Sgm (dom (f | (M " {v})))) . w by A3, A18, A19, A35, FUNCT_1:def 4;
hence contradiction by A22, A29, A26, A27, A30, A31, FUNCT_1:def 4; :: thesis: verum

end;

F . w = (f | (M " {v})) . ((Sgm (dom (f | (M " {v})))) . w) by A30, FUNCT_1:12;
then A36: F . w = f . ((Sgm (dom (f | (M " {v})))) . w) by A32, FUNCT_1:47;
(Sgm (dom (f | (M " {v})))) . w in dom f by A32, RELAT_1:57;
hence F . w = 0 by A10, A36, A34; :: thesis: verum

end;

then A37: F has_onlyone_value_in j by A22, A26, ENTROPY1:def 2;
f . i = L . v by A10, A24, A20;
hence L . v = K . v by A25, A28, A37, ENTROPY1:13; :: thesis: verum

end;

suppose A38: 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 A38;
then A39: 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 A38;
hence L . v = K . v by A39, VECTSP_6:2; :: thesis: verum

end;

end;

end;

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