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:
set C = Carrier L;
consider F being FinSequence of the carrier of V2 such that
A2: F is one-to-one and
A3: rng F = Carrier L and
A4: Sum L = Sum (L (#) F) by VECTSP_6:def 6;
defpred S₁[ object , object ] means ( $2 in A & f . $2 = F . $1 );
set D = dom F;
A5: for x being object st x in dom F holds
ex y being object st
( y in the carrier of V1 & S₁[x,y] )

let x be object ; :: thesis:
assume x in dom F ; :: thesis:
then F . x in rng F by FUNCT_1:def 3;
then consider y being object such that
y in dom f and
A6: ( y in A & f . y = F . x ) by A1, A3, FUNCT_1:def 6;
take y ; :: thesis:
thus ( y in the carrier of V1 & S₁[x,y] ) by A6; :: thesis:

end;

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

let x1, x2 be object ; :: thesis:
assume that
A11: ( x1 in dom p & x2 in dom p ) and
A12: p . x1 = p . x2 ; :: thesis:
( f . (p . x1) = F . x1 & f . (p . x2) = F . x2 ) by A7, A9, A11;
hence x1 = x2 by A2, A9, A11, A12, FUNCT_1:def 4; :: thesis:

end;

then A13: p is one-to-one by FUNCT_1:def 4;
reconsider RNG = rng p as finite Subset of V1 by RELAT_1:def 19;
defpred S₂[ object , object ] 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 ) );
A14: for x being object st x in the carrier of V1 holds
ex y being object st
( y in the carrier of K & S₂[x,y] )

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

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

end;

then consider y being object such that
A17: ( y in dom p & p . y = v1 ) by FUNCT_1:def 3;
take L . (F . y) ; :: thesis:
L . (F /. y) in the carrier of K ;
hence ( L . (F . y) in the carrier of K & S₂[x,L . (F . y)] ) by A9, A10, A16, A17, PARTFUN1:def 6; :: thesis:

end;

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

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

end;

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A21: y in RNG ; :: thesis:
reconsider v1 = y as Vector of V1 by A21;
consider x being object such that
A22: x in dom F and
A23: p . x = v1 by A9, A21, FUNCT_1:def 3;
F . x in Carrier L by A3, A22, FUNCT_1:def 3;
then A24: L . (F . x) <> 0. K by VECTSP_6:2;
M . v1 = L . (F . x) by A18, A21, A22, A23;
hence y in Carrier M by A24; :: thesis:

end;

end;

let x be object ; :: thesis:
assume A28: x in dom F ; :: thesis:
reconsider i = x as Element of NAT by A28;
A29: F . i = F /. i by A28, PARTFUN1:def 6;
p . i in RNG by A9, A28, FUNCT_1:def 3;
then A30: M . (p . i) = L . (F . i) by A18, A28;
A31: ( p /. i = p . i & f . (p . i) = F . i ) by A7, A9, A28, PARTFUN1:def 6;
thus (f * (M (#) p)) . x = f . ((M (#) p) . i) by A25, A28, FUNCT_1:13
.= f . ((M . (p /. i)) * (p /. i)) by A25, A28, VECTSP_6:def 5
.= (L . (F /. i)) * (F /. i) by A31, A29, A30, MOD_2:def 2
.= (L (#) F) . x by A26, A28, VECTSP_6:def 5 ; :: thesis:

end;