let V be RealLinearSpace; :: thesis:
let W be Subspace of V; :: thesis:
let L be Linear_Combination of V; :: thesis:
assume A1: Carrier L c= the carrier of W ; :: thesis:
let K be Linear_Combination of W; :: thesis:
assume A2: K = L | the carrier of W ; :: thesis:
A3: the carrier of W c= the carrier of V by RLSUB_1:def 2;
A4: dom K = the carrier of W by FUNCT_2:def 1;

now

let x be set ; :: thesis:
assume x in Carrier K ; :: thesis:
then consider w being VECTOR of W such that
A5: x = w and
A6: K . w <> 0 by Th3;
( L . w <> 0 & w is VECTOR of V ) by A2, A4, A6, FUNCT_1:70, RLSUB_1:18;
hence x in Carrier L by A5, Th3; :: thesis:

end;

then A7: Carrier K c= Carrier L by TARSKI:def 3;

now

let x be set ; :: thesis:
assume A8: x in Carrier L ; :: thesis:
then consider v being VECTOR of V such that
A9: x = v and
A10: L . v <> 0 by Th3;
K . v <> 0 by A1, A2, A4, A8, A9, A10, FUNCT_1:70;
hence x in Carrier K by A1, A8, A9, Th3; :: thesis:

end;

then A11: Carrier L c= Carrier K by TARSKI:def 3;
then A12: Carrier K = Carrier L by A7, XBOOLE_0:def 10;
consider F being FinSequence of the carrier of V such that
A13: F is one-to-one and
A14: rng F = Carrier L and
A15: Sum L = Sum (L (#) F) by RLVECT_2:def 10;
consider G being FinSequence of the carrier of W such that
A16: G is one-to-one and
A17: rng G = Carrier K and
A18: Sum K = Sum (K (#) G) by RLVECT_2:def 10;
F,G are_fiberwise_equipotent by A12, A13, A14, A16, A17, RFINSEQ:39;
then consider P being Permutation of (dom G) such that
A19: F = G * P by RFINSEQ:17;
set p = L (#) F;
len G = len F by A19, FINSEQ_2:48;
then ( dom G = dom F & len G = len (L (#) F) ) by FINSEQ_3:31, RLVECT_2:def 9;
then A20: ( dom (L (#) F) = dom G & dom G = dom F ) by FINSEQ_3:31;
len (K (#) G) = len G by RLVECT_2:def 9;
then A21: dom (K (#) G) = dom G by FINSEQ_3:31;
then reconsider q = (K (#) G) * P as FinSequence of the carrier of W by FINSEQ_2:51;
len q = len (K (#) G) by A21, FINSEQ_2:48;
then ( dom q = dom (K (#) G) & len q = len G ) by FINSEQ_3:31, RLVECT_2:def 9;
then A22: ( dom q = dom (K (#) G) & dom q = dom G ) by FINSEQ_3:31;

now

let i be Nat; :: thesis:
assume A23: i in dom (L (#) F) ; :: thesis:
set v = F /. i;
A24: F /. i = F . i by A20, A23, PARTFUN1:def 8;
set j = P . i;
( dom P = dom G & rng P = dom G ) by FUNCT_2:67, FUNCT_2:def 3;
then A25: P . i in dom G by A20, A23, FUNCT_1:def 5;
then reconsider j = P . i as Element of NAT ;
A26: G /. j = G . (P . i) by A25, PARTFUN1:def 8
.= F /. i by A19, A20, A23, A24, FUNCT_1:22 ;
F /. i in rng F by A20, A23, A24, FUNCT_1:def 5;
then reconsider w = F /. i as VECTOR of W by A12, A14;
q . i = (K (#) G) . j by A20, A22, A23, FUNCT_1:22
.= (K . w) * w by A22, A25, A26, RLVECT_2:def 9
.= (L . (F /. i)) * w by A2, A4, FUNCT_1:70
.= (L . (F /. i)) * (F /. i) by RLSUB_1:22 ;
hence (L (#) F) . i = q . i by A23, RLVECT_2:def 9; :: thesis:

end;

then A27: L (#) F = (K (#) G) * P by A20, A22, FINSEQ_1:17;
len G = len (K (#) G) by RLVECT_2:def 9;
then dom G = dom (K (#) G) by FINSEQ_3:31;
then reconsider P = P as Permutation of (dom (K (#) G)) ;
q = (K (#) G) * P ;
then A28: Sum (K (#) G) = Sum q by RLVECT_2:9;
rng q c= the carrier of W by FINSEQ_1:def 4;
then rng q c= the carrier of V by A3, XBOOLE_1:1;
then reconsider q' = q as FinSequence of the carrier of V by FINSEQ_1:def 4;
consider f being Function of NAT ,the carrier of W such that
A29: Sum q = f . (len q) and
A30: f . 0 = 0. W and
A31: for i being Element of NAT
for w being VECTOR of W st i < len q & w = q . (i + 1) holds
f . (i + 1) = (f . i) + w by RLVECT_1:def 13;
( dom f = NAT & rng f c= the carrier of W ) by FUNCT_2:def 1, RELAT_1:def 19;
then reconsider f' = f as Function of NAT ,the carrier of V by A3, FUNCT_2:4, XBOOLE_1:1;
A32: f' . 0 = 0. V by A30, RLSUB_1:19;
A33: for i being Element of NAT
for v being VECTOR of V st i < len q' & v = q' . (i + 1) holds
f' . (i + 1) = (f' . i) + v

proof

let i be Element of NAT ; :: thesis:
let v be VECTOR of V; :: thesis:
assume A34: ( i < len q' & v = q' . (i + 1) ) ; :: thesis:
then ( 1 <= i + 1 & i + 1 <= len q ) by NAT_1:11, NAT_1:13;
then i + 1 in dom q by FINSEQ_3:27;
then reconsider v' = v as VECTOR of W by A34, FINSEQ_2:13;
f . (i + 1) = (f . i) + v' by A31, A34;
hence f' . (i + 1) = (f' . i) + v by RLSUB_1:21; :: thesis:

end;

f' . (len q') is Element of V ;
hence ( Carrier L = Carrier K & Sum L = Sum K ) by A7, A11, A15, A18, A27, A28, A29, A32, A33, RLVECT_1:def 13, XBOOLE_0:def 10; :: thesis: