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;

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;

then A17: Carrier K = Carrier L by A7, XBOOLE_0:def 10;

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 the carrier 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 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 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

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;

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, RLSUB_1:11;

hence ( Carrier L = Carrier K & Sum L = Sum K ) by A7, A16, A12, A9, A37, A38, A23, A26, A39, RLVECT_1:def 12, XBOOLE_0:def 10; :: thesis: verum

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

then A7:
Carrier K c= Carrier L
;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 by Th3;

A6: w is VECTOR of V by RLSUB_1:10;

L . w <> 0 by A2, A3, A5, FUNCT_1:47;

hence x in Carrier L by A4, A6, Th3; :: thesis: verum

end;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 by Th3;

A6: w is VECTOR of V by RLSUB_1:10;

L . w <> 0 by A2, A3, A5, FUNCT_1:47;

hence x in Carrier L by A4, A6, Th3; :: thesis: verum

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

then A16:
Carrier L c= Carrier K
;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 by Th3;

K . v <> 0 by A1, A2, A3, A13, A14, A15, FUNCT_1:47;

hence x in Carrier K by A1, A13, A14, Th3; :: thesis: verum

end;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 by Th3;

K . v <> 0 by A1, A2, A3, A13, A14, A15, FUNCT_1:47;

hence x in Carrier K by A1, A13, A14, Th3; :: thesis: verum

then A17: Carrier K = Carrier L by A7, XBOOLE_0:def 10;

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 the carrier 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 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 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

A29:
len G = len F
by A18, FINSEQ_2:44;
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 RLSUB_1:13; :: thesis: verum

end;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 RLSUB_1:13; :: thesis: verum

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

then A37:
L (#) F = (K (#) G) * P
by A31, A21, FINSEQ_1:13;(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 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 RLSUB_1:14 ;

hence (L (#) F) . i = q . i by A33, RLVECT_2:def 7; :: thesis: verum

end;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 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 RLSUB_1:14 ;

hence (L (#) F) . i = q . i by A33, RLVECT_2:def 7; :: thesis: verum

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, RLSUB_1:11;

hence ( Carrier L = Carrier K & Sum L = Sum K ) by A7, A16, A12, A9, A37, A38, A23, A26, A39, RLVECT_1:def 12, XBOOLE_0:def 10; :: thesis: verum