let K be Field; :: thesis: for V1, V2 being VectSp of K
for A, B being Subset of V1
for L being Linear_Combination of V1 st Carrier L c= A \/ B & Sum L = 0. V1 holds
for f being additive homogeneous Function of V1,V2 st f | B is one-to-one & f .: B is linearly-independent Subset of V2 & f .: A c= {(0. V2)} holds
Carrier L c= A
let V1, V2 be VectSp of K; :: thesis: for A, B being Subset of V1
for L being Linear_Combination of V1 st Carrier L c= A \/ B & Sum L = 0. V1 holds
for f being additive homogeneous Function of V1,V2 st f | B is one-to-one & f .: B is linearly-independent Subset of V2 & f .: A c= {(0. V2)} holds
Carrier L c= A
let A, B be Subset of V1; :: thesis: for L being Linear_Combination of V1 st Carrier L c= A \/ B & Sum L = 0. V1 holds
for f being additive homogeneous Function of V1,V2 st f | B is one-to-one & f .: B is linearly-independent Subset of V2 & f .: A c= {(0. V2)} holds
Carrier L c= A
let L be Linear_Combination of V1; :: thesis: ( Carrier L c= A \/ B & Sum L = 0. V1 implies for f being additive homogeneous Function of V1,V2 st f | B is one-to-one & f .: B is linearly-independent Subset of V2 & f .: A c= {(0. V2)} holds
Carrier L c= A )
assume that
A1: Carrier L c= A \/ B and
A2: Sum L = 0. V1 ; :: thesis: for f being additive homogeneous Function of V1,V2 st f | B is one-to-one & f .: B is linearly-independent Subset of V2 & f .: A c= {(0. V2)} holds
Carrier L c= A
consider F being FinSequence of V1 such that
A3: F is one-to-one and
A4: rng F = Carrier L and
A5: 0. V1 = Sum (L (#) F) by A2, VECTSP_6:def 6;
let f be additive homogeneous Function of V1,V2; :: thesis: ( f | B is one-to-one & f .: B is linearly-independent Subset of V2 & f .: A c= {(0. V2)} implies Carrier L c= A )
assume that
A6: f | B is one-to-one and
A7: f .: B is linearly-independent Subset of V2 and
A8: f .: A c= {(0. V2)} ; :: thesis: Carrier L c= A

per cases ( dom F = {} or dom F <> {} ) ;

suppose dom F = {} ; :: thesis: Carrier L c= A

then rng F = {} by RELAT_1:42;
hence Carrier L c= A by A4; :: thesis: verum

end;

suppose dom F <> {} ; :: thesis: Carrier L c= A

then reconsider D = dom F as non empty finite set ;
set C = Carrier L;
set FA = F " ((Carrier L) /\ A);
set FB = F " ((Carrier L) /\ B);
set SS = (Sgm (F " ((Carrier L) /\ B))) ^ (Sgm (F " ((Carrier L) /\ A)));
A9: (Carrier L) /\ ((Carrier L) /\ B) = (Carrier L) /\ B by XBOOLE_1:18, XBOOLE_1:28;
rng F c= the carrier of V1 by RELAT_1:def 19;
then reconsider F9 = F as Function of D, the carrier of V1 by FUNCT_2:2;
A10: D = Seg (len F) by FINSEQ_1:def 3;
A16: F " ((Carrier L) /\ A) c= D by RELAT_1:132;
then a10: F " ((Carrier L) /\ A) is included_in_Seg by A10, FINSEQ_1:def 13;
then A11: Sgm (F " ((Carrier L) /\ A)) is one-to-one by FINSEQ_3:92;
A14: F " ((Carrier L) /\ B) c= D by RELAT_1:132;
then a11: F " ((Carrier L) /\ B) is included_in_Seg by A10, FINSEQ_1:def 13;
then A12: ( len (Sgm (F " ((Carrier L) /\ A))) = card (F " ((Carrier L) /\ A)) & len (Sgm (F " ((Carrier L) /\ B))) = card (F " ((Carrier L) /\ B)) ) by a10, FINSEQ_3:39;
A13: Sgm (F " ((Carrier L) /\ B)) is one-to-one by a11, FINSEQ_3:92;
F " ((Carrier L) /\ B) is included_in_Seg by A10, A14, FINSEQ_1:def 13;
then A15: rng (Sgm (F " ((Carrier L) /\ B))) = F " ((Carrier L) /\ B) by FINSEQ_1:def 14;
A17: rng (Sgm (F " ((Carrier L) /\ A))) = F " ((Carrier L) /\ A) by a10, FINSEQ_1:def 14;
then reconsider SA = Sgm (F " ((Carrier L) /\ A)), SB = Sgm (F " ((Carrier L) /\ B)) as FinSequence of D by A16, A14, A15, FINSEQ_1:def 4;
A misses B

proof

assume A meets B ; :: thesis: contradiction
then consider x being object such that
A18: x in A and
A19: x in B by XBOOLE_0:3;
reconsider x = x as Vector of V1 by A18;
dom f = the carrier of V1 by FUNCT_2:def 1;
then ( f . x in f .: A & f . x in f .: B ) by A18, A19, FUNCT_1:def 6;
then 0. V2 in f .: B by A8, TARSKI:def 1;
hence contradiction by A7, VECTSP_7:2; :: thesis: verum

end;

then A20: (Carrier L) /\ A misses (Carrier L) /\ B by XBOOLE_1:76;
then F " ((Carrier L) /\ A) misses F " ((Carrier L) /\ B) by FUNCT_1:71;
then A21: (Sgm (F " ((Carrier L) /\ B))) ^ (Sgm (F " ((Carrier L) /\ A))) is one-to-one by A11, A17, A13, A15, FINSEQ_3:91;
((Carrier L) /\ A) \/ ((Carrier L) /\ B) = (Carrier L) /\ (A \/ B) by XBOOLE_1:23
.= Carrier L by A1, XBOOLE_1:28 ;
then A22: (F " ((Carrier L) /\ A)) \/ (F " ((Carrier L) /\ B)) = F " (Carrier L) by RELAT_1:140
.= dom F by A4, RELAT_1:134 ;
then (card (F " ((Carrier L) /\ A))) + (card (F " ((Carrier L) /\ B))) = card (Seg (len F)) by A10, A20, CARD_2:40, FUNCT_1:71
.= len F by FINSEQ_1:57 ;
then len ((Sgm (F " ((Carrier L) /\ B))) ^ (Sgm (F " ((Carrier L) /\ A)))) = len F by A12, FINSEQ_1:22;
then A23: dom ((Sgm (F " ((Carrier L) /\ B))) ^ (Sgm (F " ((Carrier L) /\ A)))) = D by FINSEQ_3:29;
rng ((Sgm (F " ((Carrier L) /\ B))) ^ (Sgm (F " ((Carrier L) /\ A)))) = D by A22, A17, A15, FINSEQ_1:31;
then reconsider SS = (Sgm (F " ((Carrier L) /\ B))) ^ (Sgm (F " ((Carrier L) /\ A))) as Function of D,D by A23, FUNCT_2:1;
card D = card D ;
then SS is onto by A21, FINSEQ_4:63;
then reconsider SS = SS as Permutation of D by A21;
reconsider FS = F9 * SS, FSA = F9 * SA, FSB = F9 * SB as FinSequence of V1 by FINSEQ_2:47;
A24: (Carrier L) /\ B c= rng FSB

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (Carrier L) /\ B or y in rng FSB )
assume A25: y in (Carrier L) /\ B ; :: thesis: y in rng FSB
y in rng F by A4, A25, XBOOLE_0:def 4;
then consider x being object such that
A26: ( x in dom F & y = F . x ) by FUNCT_1:def 3;
x in F " ((Carrier L) /\ B) by A25, A26, FUNCT_1:def 7;
then consider z being object such that
A27: ( z in dom SB & SB . z = x ) by A15, FUNCT_1:def 3;
( FSB . z = y & z in dom FSB ) by A26, A27, FUNCT_1:11, FUNCT_1:13;
hence y in rng FSB by FUNCT_1:def 3; :: thesis: verum

end;

rng FSB c= (Carrier L) /\ B

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng FSB or y in (Carrier L) /\ B )
assume y in rng FSB ; :: thesis: y in (Carrier L) /\ B
then consider x being object such that
A28: x in dom FSB and
A29: FSB . x = y by FUNCT_1:def 3;
x in dom SB by A28, FUNCT_1:11;
then A30: SB . x in F " ((Carrier L) /\ B) by A15, FUNCT_1:def 3;
FSB . x = F . (SB . x) by A28, FUNCT_1:12;
hence y in (Carrier L) /\ B by A29, A30, FUNCT_1:def 7; :: thesis: verum

end;

then A31: (Carrier L) /\ B = rng FSB by A24;

A32: now :: thesis: for k being Nat
for v being Element of V2 st k in dom (f * (L (#) FSA)) & v = (f * (L (#) FSA)) . k holds
(f * (L (#) FSA)) . k = (0. K) * v

len (L (#) FSA) = len FSA by VECTSP_6:def 5;
then A33: dom (L (#) FSA) = dom FSA by FINSEQ_3:29;
A34: dom f = [#] V1 by FUNCT_2:def 1;
( rng (L (#) FSA) c= [#] V1 & dom f = [#] V1 ) by FUNCT_2:def 1, RELAT_1:def 19;
then A35: dom (f * (L (#) FSA)) = dom (L (#) FSA) by RELAT_1:27;
let k be Nat; :: thesis: for v being Element of V2 st k in dom (f * (L (#) FSA)) & v = (f * (L (#) FSA)) . k holds
(f * (L (#) FSA)) . k = (0. K) * v
let v be Element of V2; :: thesis: ( k in dom (f * (L (#) FSA)) & v = (f * (L (#) FSA)) . k implies (f * (L (#) FSA)) . k = (0. K) * v )
assume that
A36: k in dom (f * (L (#) FSA)) and
v = (f * (L (#) FSA)) . k ; :: thesis: (f * (L (#) FSA)) . k = (0. K) * v
dom FSA = dom SA by A17, RELAT_1:27, RELAT_1:132;
then SA . k in F " ((Carrier L) /\ A) by A17, A36, A35, A33, FUNCT_1:def 3;
then A37: F . (SA . k) in (Carrier L) /\ A by FUNCT_1:def 7;
FSA /. k = FSA . k by A36, A35, A33, PARTFUN1:def 6
.= F . (SA . k) by A36, A35, A33, FUNCT_1:12 ;
then FSA /. k in A by A37, XBOOLE_0:def 4;
then f . (FSA /. k) in f .: A by A34, FUNCT_1:def 6;
then A38: f . (FSA /. k) = 0. V2 by A8, TARSKI:def 1;
thus (f * (L (#) FSA)) . k = f . ((L (#) FSA) . k) by A36, FUNCT_1:12
.= f . ((L . (FSA /. k)) * (FSA /. k)) by A36, A35, VECTSP_6:def 5
.= (L . (FSA /. k)) * (0. V2) by A38, MOD_2:def 2
.= 0. V2 by VECTSP_1:14
.= (0. K) * v by VECTSP_1:14 ; :: thesis: verum

end;

len (f * (L (#) FSA)) = len (f * (L (#) FSA)) ;
then A39: Sum (f * (L (#) FSA)) = (0. K) * (Sum (f * (L (#) FSA))) by A32, RLVECT_2:66;
FS = FSB ^ FSA by FINSEQOP:9;
then L (#) FS = (L (#) FSB) ^ (L (#) FSA) by VECTSP_6:13;
then A40: f * (L (#) FS) = (f * (L (#) FSB)) ^ (f * (L (#) FSA)) by FINSEQOP:9;
(f | B) | ((Carrier L) /\ B) = f | ((Carrier L) /\ B) by RELAT_1:74, XBOOLE_1:18;
then A41: f | ((Carrier L) /\ B) is one-to-one by A6, FUNCT_1:52;
then consider Lf being Linear_Combination of V2 such that
A42: Carrier Lf = f .: ((Carrier L) /\ (rng FSB)) and
A43: f * (L (#) FSB) = Lf (#) (f * FSB) and
A44: for v1 being Vector of V1 st v1 in (Carrier L) /\ (rng FSB) holds
L . v1 = Lf . (f . v1) by A31, A9, Th43, XBOOLE_1:18;
A45: Carrier Lf = rng (f * FSB) by A31, A9, A42, RELAT_1:127;
A46: f * FSB = f * ((id (rng FSB)) * FSB) by RELAT_1:53
.= (f * (id (rng FSB))) * FSB by RELAT_1:36
.= (f | ((Carrier L) /\ B)) * FSB by A31, RELAT_1:65 ;
Carrier Lf c= f .: B by A31, A9, A42, RELAT_1:123, XBOOLE_1:18;
then A47: Lf is Linear_Combination of f .: B by VECTSP_6:def 4;
f . (0. V1) = 0. V2 by RANKNULL:9;
then A48: 0. V2 = f . (Sum (L (#) FS)) by A5, VECTSP_9:1
.= Sum (f * (L (#) FS)) by MATRLIN:16
.= (Sum (f * (L (#) FSB))) + (Sum (f * (L (#) FSA))) by A40, RLVECT_1:41
.= (Sum (f * (L (#) FSB))) + (0. V2) by A39, VECTSP_1:14
.= Sum (Lf (#) (f * FSB)) by A43, RLVECT_1:def 4
.= Sum Lf by A3, A13, A41, A45, A46, VECTSP_6:def 6 ;
thus Carrier L c= A :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier L or x in A )
assume A49: x in Carrier L ; :: thesis: x in A
reconsider v1 = x as Vector of V1 by A49;
assume A50: not x in A ; :: thesis: contradiction
( x in A or x in B ) by A1, A49, XBOOLE_0:def 3;
then v1 in (Carrier L) /\ (rng FSB) by A31, A9, A49, A50, XBOOLE_0:def 4;
then A51: L . v1 = Lf . (f . v1) by A44;
not f . v1 in Carrier Lf by A7, A47, A48, VECTSP_7:def 1;
then L . v1 = 0. K by A51;
hence contradiction by A49, VECTSP_6:2; :: thesis: verum

end;

end;

end;