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

per cases ;

suppose dom F = {} ; :: thesis:

then rng F = {} by RELAT_1:65;
hence Carrier L c= A by A6, XBOOLE_1:2; :: thesis:

end;

suppose dom F <> {} ; :: thesis:

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);
((Carrier L) /\ A) \/ ((Carrier L) /\ B) = (Carrier L) /\ (A \/ B) by XBOOLE_1:23
.= Carrier L by A1, XBOOLE_1:28 ;
then A7: (F " ((Carrier L) /\ A)) \/ (F " ((Carrier L) /\ B)) = F " (Carrier L) by RELAT_1:175
.= dom F by A6, RELAT_1:169 ;
A8: D = Seg (len F) by FINSEQ_1:def 3;
A misses B

proof

assume A meets B ; :: thesis:
then consider x being set such that
A9: ( x in A & x in B ) by XBOOLE_0:3;
reconsider x = x as Vector of V1 by A9;
dom f = the carrier of V1 by FUNCT_2:def 1;
then ( f . x in f .: A & f . x in f .: B ) by A9, FUNCT_1:def 12;
then 0. V2 in f .: B by A4, TARSKI:def 1;
hence contradiction by A3, VECTSP_7:3; :: thesis:

end;

then A10: (Carrier L) /\ A misses (Carrier L) /\ B by XBOOLE_1:76;
then A11: F " ((Carrier L) /\ A) misses F " ((Carrier L) /\ B) by FUNCT_1:141;
A12: (card (F " ((Carrier L) /\ A))) + (card (F " ((Carrier L) /\ B))) = card (Seg (len F)) by A7, A8, A10, CARD_2:53, FUNCT_1:141
.= len F by FINSEQ_1:78 ;
set SS = (Sgm (F " ((Carrier L) /\ B))) ^ (Sgm (F " ((Carrier L) /\ A)));
A13: ( F " ((Carrier L) /\ A) c= D & F " ((Carrier L) /\ B) c= D ) by RELAT_1:167;
then A14: ( Sgm (F " ((Carrier L) /\ A)) is one-to-one & rng (Sgm (F " ((Carrier L) /\ A))) = F " ((Carrier L) /\ A) & len (Sgm (F " ((Carrier L) /\ A))) = card (F " ((Carrier L) /\ A)) & Sgm (F " ((Carrier L) /\ B)) is one-to-one & rng (Sgm (F " ((Carrier L) /\ B))) = F " ((Carrier L) /\ B) & len (Sgm (F " ((Carrier L) /\ B))) = card (F " ((Carrier L) /\ B)) ) by A8, FINSEQ_1:def 13, FINSEQ_3:44, FINSEQ_3:99;
then A15: ( (Sgm (F " ((Carrier L) /\ B))) ^ (Sgm (F " ((Carrier L) /\ A))) is one-to-one & len ((Sgm (F " ((Carrier L) /\ B))) ^ (Sgm (F " ((Carrier L) /\ A)))) = len F ) by A12, A11, FINSEQ_1:35, FINSEQ_3:98;
then A16: dom ((Sgm (F " ((Carrier L) /\ B))) ^ (Sgm (F " ((Carrier L) /\ A)))) = D by FINSEQ_3:31;
A17: card D = card D ;
rng ((Sgm (F " ((Carrier L) /\ B))) ^ (Sgm (F " ((Carrier L) /\ A)))) = D by A7, A14, FINSEQ_1:44;
then reconsider SS = (Sgm (F " ((Carrier L) /\ B))) ^ (Sgm (F " ((Carrier L) /\ A))) as Function of D,D by A16, FUNCT_2:3;
SS is onto by A15, A17, STIRL2_1:70;
then reconsider SS = SS as Permutation of D by A15;
reconsider SA = Sgm (F " ((Carrier L) /\ A)), SB = Sgm (F " ((Carrier L) /\ B)) as FinSequence of D by A13, A14, FINSEQ_1:def 4;
rng F c= the carrier of V1 by RELAT_1:def 19;
then reconsider F' = F as Function of D,the carrier of V1 by FUNCT_2:4;
reconsider FS = F' * SS, FSA = F' * SA, FSB = F' * SB as FinSequence of V1 by FINSEQ_2:51;
FS = FSB ^ FSA by FINSEQOP:10;
then L (#) FS = (L (#) FSB) ^ (L (#) FSA) by VECTSP_6:37;
then A18: f * (L (#) FS) = (f * (L (#) FSB)) ^ (f * (L (#) FSA)) by FINSEQOP:10;
A19: len (f * (L (#) FSA)) = len (f * (L (#) FSA)) ;

now

let k be Element of NAT ; :: thesis:
let v be Element of V2; :: thesis:
assume A20: ( k in dom (f * (L (#) FSA)) & v = (f * (L (#) FSA)) . k ) ; :: thesis:
( rng (L (#) FSA) c= [#] V1 & dom f = [#] V1 & len (L (#) FSA) = len FSA ) by FUNCT_2:def 1, RELAT_1:def 19, VECTSP_6:def 8;
then A21: ( dom (f * (L (#) FSA)) = dom (L (#) FSA) & dom FSA = dom SA & dom (L (#) FSA) = dom FSA ) by A13, A14, FINSEQ_3:31, RELAT_1:46;
A22: FSA /. k = FSA . k by A20, A21, PARTFUN1:def 8
.= F . (SA . k) by A20, A21, FUNCT_1:22 ;
SA . k in F " ((Carrier L) /\ A) by A14, A20, A21, FUNCT_1:def 5;
then F . (SA . k) in (Carrier L) /\ A by FUNCT_1:def 13;
then ( FSA /. k in A & dom f = [#] V1 ) by A22, FUNCT_2:def 1, XBOOLE_0:def 4;
then f . (FSA /. k) in f .: A by FUNCT_1:def 12;
then A23: f . (FSA /. k) = 0. V2 by A4, TARSKI:def 1;
thus (f * (L (#) FSA)) . k = f . ((L (#) FSA) . k) by A20, FUNCT_1:22
.= f . ((L . (FSA /. k)) * (FSA /. k)) by A20, A21, VECTSP_6:def 8
.= (L . (FSA /. k)) * (0. V2) by A23, MOD_2:def 5
.= 0. V2 by VECTSP_1:59
.= (0. K) * v by VECTSP_1:59 ; :: thesis:

end;

then A24: Sum (f * (L (#) FSA)) = (0. K) * (Sum (f * (L (#) FSA))) by A19, VECTSP_3:9;
A25: rng FSB c= (Carrier L) /\ B

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume A26: y in rng FSB ; :: thesis:
consider x being set such that
A27: ( x in dom FSB & FSB . x = y ) by A26, FUNCT_1:def 5;
A28: ( FSB . x = F . (SB . x) & x in dom SB ) by A27, FUNCT_1:21, FUNCT_1:22;
then SB . x in F " ((Carrier L) /\ B) by A14, FUNCT_1:def 5;
hence y in (Carrier L) /\ B by A27, A28, FUNCT_1:def 13; :: thesis:

end;

(Carrier L) /\ B c= rng FSB

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume A29: y in (Carrier L) /\ B ; :: thesis:
y in rng F by A6, A29, XBOOLE_0:def 4;
then consider x being set such that
A30: ( x in dom F & y = F . x ) by FUNCT_1:def 5;
x in F " ((Carrier L) /\ B) by A29, A30, FUNCT_1:def 13;
then consider z being set such that
A31: ( z in dom SB & SB . z = x ) by A14, FUNCT_1:def 5;
( FSB . z = y & z in dom FSB ) by A30, A31, FUNCT_1:21, FUNCT_1:23;
hence y in rng FSB by FUNCT_1:def 5; :: thesis:

end;

then A32: (Carrier L) /\ B = rng FSB by A25, XBOOLE_0:def 10;
A34: (Carrier L) /\ ((Carrier L) /\ B) = (Carrier L) /\ B by XBOOLE_1:18, XBOOLE_1:28;
(f | B) | ((Carrier L) /\ B) = f | ((Carrier L) /\ B) by RELAT_1:103, XBOOLE_1:18;
then A35: ( f | ((Carrier L) /\ B) is one-to-one & FSB is one-to-one ) by A2, A5, A14, FUNCT_1:84;
consider Lf being Linear_Combination of V2 such that
A36: Carrier Lf = f .: ((Carrier L) /\ (rng FSB)) and
A37: f * (L (#) FSB) = Lf (#) (f * FSB) and
A38: for v1 being Vector of V1 st v1 in (Carrier L) /\ (rng FSB) holds
L . v1 = Lf . (f . v1) by A35, A32, A34, Th43, XBOOLE_1:18;
Carrier Lf c= f .: B by A34, A32, A36, RELAT_1:156, XBOOLE_1:18;
then A39: Lf is Linear_Combination of f .: B by VECTSP_6:def 7;
A40: Carrier Lf = rng (f * FSB) by A36, A34, A32, RELAT_1:160;
aa: f * FSB = f * ((id (rng FSB)) * FSB) by RELAT_1:79
.= (f * (id (rng FSB))) * FSB by RELAT_1:55
.= (f | ((Carrier L) /\ B)) * FSB by A32, RELAT_1:94 ;
f . (0. V1) = 0. V2 by RANKNULL:9;
then A42: 0. V2 = f . (Sum (L (#) FS)) by A6, VECTSP_9:5
.= Sum (f * (L (#) FS)) by MATRLIN:20
.= (Sum (f * (L (#) FSB))) + (Sum (f * (L (#) FSA))) by A18, RLVECT_1:58
.= (Sum (f * (L (#) FSB))) + (0. V2) by A24, VECTSP_1:59
.= Sum (Lf (#) (f * FSB)) by A37, RLVECT_1:def 7
.= Sum Lf by A40, aa, A35, VECTSP_6:def 9 ;
thus Carrier L c= A :: thesis:

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A43: x in Carrier L ; :: thesis:
reconsider v1 = x as Vector of V1 by A43;
A44: ( x in A or x in B ) by A1, A43, XBOOLE_0:def 3;
assume not x in A ; :: thesis:
then v1 in (Carrier L) /\ (rng FSB) by A34, A43, A44, A32, XBOOLE_0:def 4;
then ( L . v1 = Lf . (f . v1) & not f . v1 in Carrier Lf ) by A38, A42, A3, A39, VECTSP_7:def 1;
then L . v1 = 0. K ;
hence contradiction by A43, VECTSP_6:20; :: thesis:

end;