let V be RealLinearSpace; :: thesis: for W being Subspace of V
for L being Linear_Combination of V st Carrier L c= the carrier of W holds
for K being Linear_Combination of W st K = L | the carrier of W holds
( Carrier L = Carrier K & Sum L = Sum K )

let W be Subspace of V; :: thesis: for L being Linear_Combination of V st Carrier L c= the carrier of W holds
for K being Linear_Combination of W st K = L | the carrier of W holds
( Carrier L = Carrier K & Sum L = Sum K )

let L be Linear_Combination of V; :: thesis: ( Carrier L c= the carrier of W implies for K being Linear_Combination of W st K = L | the carrier of W holds
( Carrier L = Carrier K & Sum L = Sum K ) )

assume A1: Carrier L c= the carrier of W ; :: thesis: for K being Linear_Combination of W st K = L | the carrier of W holds
( Carrier L = Carrier K & Sum L = Sum K )

let K be Linear_Combination of W; :: thesis: ( K = L | the carrier of W implies ( Carrier L = Carrier K & Sum L = Sum K ) )
assume A2: K = L | the carrier of W ; :: thesis: ( Carrier L = Carrier K & Sum L = Sum K )
A3: dom K = the carrier of W by FUNCT_2:def 1;
now :: thesis: for x being object st x in Carrier K holds
x in Carrier L
let x be object ; :: thesis: ( x in Carrier K implies x in Carrier L )
assume x in Carrier K ; :: thesis:
then consider w being VECTOR of W such that
A4: x = w and
A5: K . w <> 0 by Th3;
A6: w is VECTOR of V by RLSUB_1:10;
L . w <> 0 by ;
hence x in Carrier L by A4, A6, Th3; :: thesis: verum
end;
then A7: Carrier K c= Carrier L ;
consider G being FinSequence of the carrier of W such that
A8: ( G is one-to-one & rng G = Carrier K ) and
A9: Sum K = Sum (K (#) G) by RLVECT_2:def 8;
consider F being FinSequence of the carrier of V such that
A10: F is one-to-one and
A11: rng F = Carrier L and
A12: Sum L = Sum (L (#) F) by RLVECT_2:def 8;
now :: thesis: for x being object st x in Carrier L holds
x in Carrier K
let x be object ; :: thesis: ( x in Carrier L implies x in Carrier K )
assume A13: x in Carrier L ; :: thesis:
then consider v being VECTOR of V such that
A14: x = v and
A15: L . v <> 0 by Th3;
K . v <> 0 by ;
hence x in Carrier K by A1, A13, A14, Th3; :: thesis: verum
end;
then A16: Carrier L c= Carrier K ;
then A17: Carrier K = Carrier L by ;
then F,G are_fiberwise_equipotent by ;
then consider P being Permutation of (dom G) such that
A18: F = G * P by RFINSEQ:4;
len (K (#) G) = len G by RLVECT_2:def 7;
then A19: dom (K (#) G) = dom G by FINSEQ_3:29;
then reconsider q = (K (#) G) * P as FinSequence of the carrier of W by FINSEQ_2:47;
A20: len q = len (K (#) G) by ;
then len q = len G by RLVECT_2:def 7;
then A21: dom q = dom G by FINSEQ_3:29;
set p = L (#) F;
A22: the carrier of W c= the carrier of V by RLSUB_1:def 2;
rng q c= the carrier of W by FINSEQ_1:def 4;
then rng q c= the carrier of V by A22;
then reconsider q9 = q as FinSequence of the carrier of V by FINSEQ_1:def 4;
consider f being sequence of the carrier of W such that
A23: Sum q = f . (len q) and
A24: f . 0 = 0. W and
A25: for i being 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 12;
( dom f = NAT & rng f c= the carrier of W ) by ;
then reconsider f9 = f as sequence of the carrier of V by ;
A26: for i being Nat
for v being VECTOR of V st i < len q9 & v = q9 . (i + 1) holds
f9 . (i + 1) = (f9 . i) + v
proof
let i be Nat; :: thesis: for v being VECTOR of V st i < len q9 & v = q9 . (i + 1) holds
f9 . (i + 1) = (f9 . i) + v

let v be VECTOR of V; :: thesis: ( i < len q9 & v = q9 . (i + 1) implies f9 . (i + 1) = (f9 . i) + v )
assume that
A27: i < len q9 and
A28: v = q9 . (i + 1) ; :: thesis: f9 . (i + 1) = (f9 . i) + v
( 1 <= i + 1 & i + 1 <= len q ) by ;
then i + 1 in dom q by FINSEQ_3:25;
then reconsider v9 = v as VECTOR of W by ;
f . (i + 1) = (f . i) + v9 by ;
hence f9 . (i + 1) = (f9 . i) + v by RLSUB_1:13; :: thesis: verum
end;
A29: len G = len F by ;
then A30: dom G = dom F by FINSEQ_3:29;
len G = len (L (#) F) by ;
then A31: dom (L (#) F) = dom G by FINSEQ_3:29;
A32: dom q = dom (K (#) G) by ;
now :: thesis: for i being Nat st i in dom (L (#) F) holds
(L (#) F) . i = q . i
let i be Nat; :: thesis: ( i in dom (L (#) F) implies (L (#) F) . i = q . i )
set v = F /. i;
set j = P . i;
assume A33: i in dom (L (#) F) ; :: thesis: (L (#) F) . i = q . i
then A34: F /. i = F . i by ;
then F /. i in rng F by ;
then reconsider w = F /. i as VECTOR of W by ;
( dom P = dom G & rng P = dom G ) by ;
then A35: P . i in dom G by ;
then reconsider j = P . i as Element of NAT ;
A36: G /. j = G . (P . i) by
.= F /. i by ;
q . i = (K (#) G) . j by
.= (K . w) * w by
.= (L . (F /. i)) * w by
.= (L . (F /. i)) * (F /. i) by RLSUB_1:14 ;
hence (L (#) F) . i = q . i by ; :: thesis: verum
end;
then A37: L (#) F = (K (#) G) * P by ;
len G = len (K (#) G) by RLVECT_2:def 7;
then dom G = dom (K (#) G) by FINSEQ_3:29;
then reconsider P = P as Permutation of (dom (K (#) G)) ;
q = (K (#) G) * P ;
then A38: Sum (K (#) G) = Sum q by RLVECT_2:7;
A39: f9 . (len q9) is Element of V ;
f9 . 0 = 0. V by ;
hence ( Carrier L = Carrier K & Sum L = Sum K ) by ; :: thesis: verum