let K be Field; :: thesis:
let V1, V2 be VectSp of K; :: thesis:
let A be Subset of V1; :: thesis:
let L be Linear_Combination of V2; :: thesis:
let f be linear-transformation of V1,V2; :: thesis:
assume A1: Carrier L c= f .: A ; :: thesis:
consider F being FinSequence of the carrier of V2 such that
A2: ( F is one-to-one & rng F = Carrier L & Sum L = Sum (L (#) F) ) by VECTSP_6:def 9;
set C = Carrier L;
set D = dom F;
defpred S₁[ set , set ] means ( $2 in A & f . $2 = F . $1 );
A3: dom f = [#] V1 by FUNCT_2:def 1;
A4: for x being set st x in dom F holds
ex y being set st
( y in the carrier of V1 & S₁[x,y] )

proof

let x be set ; :: thesis:
assume x in dom F ; :: thesis:
then F . x in rng F by FUNCT_1:def 5;
then consider y being set such that
A5: ( y in dom f & y in A & f . y = F . x ) by A1, A2, FUNCT_1:def 12;
take y ; :: thesis:
thus ( y in the carrier of V1 & S₁[x,y] ) by A5; :: thesis:

end;

consider p being Function of (dom F),the carrier of V1 such that
A6: for x being set st x in dom F holds
S₁[x,p . x] from FUNCT_2:sch 1(A4);
A7: ( dom p = dom F & dom F = Seg (len F) & rng p c= the carrier of V1 ) by FINSEQ_1:def 3, FUNCT_2:def 1, RELAT_1:def 19;
then reconsider p = p as FinSequence by FINSEQ_1:def 2;
reconsider p = p as FinSequence of V1 by A7, FINSEQ_1:def 4;
reconsider RNG = rng p as finite Subset of V1 by RELAT_1:def 19;

A8: now

let x1, x2 be set ; :: thesis:
assume A9: ( x1 in dom p & x2 in dom p & p . x1 = p . x2 ) ; :: thesis:
( f . (p . x1) = F . x1 & f . (p . x2) = F . x2 ) by A6, A7, A9;
hence x1 = x2 by A2, A7, A9, FUNCT_1:def 8; :: thesis:

end;

then A10: p is one-to-one by FUNCT_1:def 8;
defpred S₂[ set , set ] means ( ( $1 in rng p implies for x being set st x in dom F & p . x = $1 holds
$2 = L . (F . x) ) & ( not $1 in rng p implies $2 = 0. K ) );
A11: for x being set st x in the carrier of V1 holds
ex y being set st
( y in the carrier of K & S₂[x,y] )

proof

let x be set ; :: thesis:
assume x in the carrier of V1 ; :: thesis:
then reconsider v1 = x as Vector of V1 ;

per cases ;

suppose A12: not v1 in rng p ; :: thesis:

take 0. K ; :: thesis:
thus ( 0. K in the carrier of K & S₂[x, 0. K] ) by A12; :: thesis:

end;

suppose A13: v1 in rng p ; :: thesis:

then consider y being set such that
A14: ( y in dom p & p . y = v1 ) by FUNCT_1:def 5;
take L . (F . y) ; :: thesis:
( F . y = F /. y & L . (F /. y) in the carrier of K ) by A7, A14, PARTFUN1:def 8;
hence ( L . (F . y) in the carrier of K & S₂[x,L . (F . y)] ) by A7, A8, A14, A13; :: thesis:

end;

consider M being Function of V1,K such that
A15: for x being set st x in the carrier of V1 holds
S₂[x,M . x] from FUNCT_2:sch 1(A11);
reconsider M = M as Element of Funcs the carrier of V1,the carrier of K by FUNCT_2:11;
for v1 being Element of V1 st not v1 in RNG holds
M . v1 = 0. K by A15;
then reconsider M = M as Linear_Combination of V1 by VECTSP_6:def 4;
A16: Carrier M = RNG

proof

thus Carrier M c= RNG :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A17: x in Carrier M ; :: thesis:
reconsider v1 = x as Vector of V1 by A17;
M . v1 <> 0. K by A17, VECTSP_6:20;
hence x in RNG by A15; :: thesis:

end;

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume A18: y in RNG ; :: thesis:
reconsider v1 = y as Vector of V1 by A18;
consider x being set such that
A19: ( x in dom F & p . x = v1 ) by A7, A18, FUNCT_1:def 5;
F . x in Carrier L by A2, A19, FUNCT_1:def 5;
then ( L . (F . x) <> 0. K & M . v1 = L . (F . x) ) by A18, A19, A15, VECTSP_6:20;
hence y in Carrier M ; :: thesis:

end;

RNG c= A

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume A20: y in RNG ; :: thesis:
ex x being set st
( x in dom F & p . x = y ) by A7, A20, FUNCT_1:def 5;
hence y in A by A6; :: thesis:

end;

then reconsider M = M as Linear_Combination of A by A16, VECTSP_6:def 7;
take M ; :: thesis:
( len (L (#) F) = len F & len (M (#) p) = len p & rng (M (#) p) c= [#] V1 ) by RELAT_1:def 19, VECTSP_6:def 8;
then A21: ( dom (L (#) F) = dom F & dom (M (#) p) = dom F & dom (f * (M (#) p)) = dom (M (#) p) ) by A3, A7, FINSEQ_3:31, RELAT_1:46;

now

let x be set ; :: thesis:
assume A22: x in dom F ; :: thesis:
reconsider i = x as Element of NAT by A22;
A23: ( p /. i = p . i & f . (p . i) = F . i & F . i = F /. i & p . i in RNG ) by A6, A7, A22, FUNCT_1:def 5, PARTFUN1:def 8;
then A24: M . (p . i) = L . (F . i) by A22, A15;
thus (f * (M (#) p)) . x = f . ((M (#) p) . i) by A21, A22, FUNCT_1:23
.= f . ((M . (p /. i)) * (p /. i)) by A21, A22, VECTSP_6:def 8
.= (L . (F /. i)) * (F /. i) by A23, A24, MOD_2:def 5
.= (L (#) F) . x by A21, A22, VECTSP_6:def 8 ; :: thesis:

end;

then f * (M (#) p) = L (#) F by A21, FUNCT_1:9;
hence Sum L = f . (Sum (M (#) p)) by A2, MATRLIN:20
.= f . (Sum M) by A16, A10, VECTSP_6:def 9 ;
:: thesis: