let V be RealUnitarySpace; :: 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: x in Carrier L
then consider w being VECTOR of W such that
A4: x = w and
A5: K . w <> 0 ;
A6: w is VECTOR of V by RUSUB_1:3;
L . w <> 0 by A2, A3, A5, FUNCT_1:47;
hence x in Carrier L by A4, A6; :: thesis: verum

end;

then A7: Carrier K c= Carrier L ;
consider G being FinSequence 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 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: x in Carrier K
then consider v being VECTOR of V such that
A14: x = v and
A15: L . v <> 0 ;
K . v <> 0 by A1, A2, A3, A13, A14, A15, FUNCT_1:47;
hence x in Carrier K by A1, A13, A14; :: thesis: verum

end;

then A16: Carrier L c= Carrier K ;
then A17: Carrier K = Carrier L by A7;
then F,G are_fiberwise_equipotent by A10, A11, A8, RFINSEQ:26;
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 W by FINSEQ_2:47;
A20: len q = len (K (#) G) by A19, FINSEQ_2:44;
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 RUSUB_1:def 1;
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 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 FUNCT_2:def 1, RELAT_1:def 19;
then reconsider f9 = f as sequence of the carrier of V by A22, FUNCT_2:2, XBOOLE_1:1;
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 A27, NAT_1:11, NAT_1:13;
then i + 1 in dom q by FINSEQ_3:25;
then reconsider v9 = v as VECTOR of W by A28, FINSEQ_2:11;
f . (i + 1) = (f . i) + v9 by A25, A27, A28;
hence f9 . (i + 1) = (f9 . i) + v by RUSUB_1:6; :: thesis: verum

end;

A29: len G = len F by A18, FINSEQ_2:44;
then A30: dom G = dom F by FINSEQ_3:29;
len G = len (L (#) F) by A29, RLVECT_2:def 7;
then A31: dom (L (#) F) = dom G by FINSEQ_3:29;
A32: dom q = dom (K (#) G) by A20, FINSEQ_3:29;

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 A31, A30, PARTFUN1:def 6;
then F /. i in rng F by A31, A30, A33, FUNCT_1:def 3;
then reconsider w = F /. i as VECTOR of W by A17, A11;
( dom P = dom G & rng P = dom G ) by FUNCT_2:52, FUNCT_2:def 3;
then A35: P . i in dom G by A31, A33, FUNCT_1:def 3;
then P . i in Seg (card G) by FINSEQ_1:def 3;
then reconsider j = P . i as Element of NAT ;
A36: G /. j = G . (P . i) by A35, PARTFUN1:def 6
.= F /. i by A18, A31, A30, A33, A34, FUNCT_1:12 ;
q . i = (K (#) G) . j by A31, A21, A33, FUNCT_1:12
.= (K . w) * w by A32, A21, A35, A36, RLVECT_2:def 7
.= (L . (F /. i)) * w by A2, A3, FUNCT_1:47
.= (L . (F /. i)) * (F /. i) by RUSUB_1:7 ;
hence (L (#) F) . i = q . i by A33, RLVECT_2:def 7; :: thesis: verum

end;

then A37: L (#) F = (K (#) G) * P by A31, A21, FINSEQ_1:13;
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 A24, RUSUB_1:4;
hence ( Carrier L = Carrier K & Sum L = Sum K ) by A7, A16, A12, A9, A37, A38, A23, A26, A39, RLVECT_1:def 12; :: thesis: verum