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 homogeneous additive 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 homogeneous additive 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 homogeneous additive 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 homogeneous additive 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 homogeneous additive 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 9;
let f be homogeneous additive 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:65;
hence Carrier L c= A by A4, XBOOLE_1:2; :: 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:4;
A10: D = Seg (len F) by FINSEQ_1:def 3;
then A11: Sgm (F " ((Carrier L) /\ A)) is one-to-one by FINSEQ_3:99, RELAT_1:167;
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:44, RELAT_1:167;
A13: Sgm (F " ((Carrier L) /\ B)) is one-to-one by A10, FINSEQ_3:99, RELAT_1:167;
A14: F " ((Carrier L) /\ B) c= D by RELAT_1:167;
then A15: rng (Sgm (F " ((Carrier L) /\ B))) = F " ((Carrier L) /\ B) by A10, FINSEQ_1:def 13;
A16: F " ((Carrier L) /\ A) c= D by RELAT_1:167;
then A17: rng (Sgm (F " ((Carrier L) /\ A))) = F " ((Carrier L) /\ A) by A10, FINSEQ_1:def 13;
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 set 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 12;
then 0. V2 in f .: B by A8, TARSKI:def 1;
hence contradiction by A7, VECTSP_7:3; :: 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:141;
then A21: (Sgm (F " ((Carrier L) /\ B))) ^ (Sgm (F " ((Carrier L) /\ A))) is one-to-one by A11, A17, A13, A15, FINSEQ_3:98;
((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:175
.= dom F by A4, RELAT_1:169 ;
then (card (F " ((Carrier L) /\ A))) + (card (F " ((Carrier L) /\ B))) = card (Seg (len F)) by A10, A20, CARD_2:53, FUNCT_1:141
.= len F by FINSEQ_1:78 ;
then len ((Sgm (F " ((Carrier L) /\ B))) ^ (Sgm (F " ((Carrier L) /\ A)))) = len F by A12, FINSEQ_1:35;
then A23: dom ((Sgm (F " ((Carrier L) /\ B))) ^ (Sgm (F " ((Carrier L) /\ A)))) = D by FINSEQ_3:31;
rng ((Sgm (F " ((Carrier L) /\ B))) ^ (Sgm (F " ((Carrier L) /\ A)))) = D by A22, A17, A15, FINSEQ_1:44;
then reconsider SS = (Sgm (F " ((Carrier L) /\ B))) ^ (Sgm (F " ((Carrier L) /\ A))) as Function of D,D by A23, FUNCT_2:3;
card D = card D ;
then SS is onto by A21, STIRL2_1:70;
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:51;
A24: (Carrier L) /\ B c= rng FSB

proof

let y be set ; :: 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 set such that
A26: ( x in dom F & y = F . x ) by FUNCT_1:def 5;
x in F " ((Carrier L) /\ B) by A25, A26, FUNCT_1:def 13;
then consider z being set such that
A27: ( z in dom SB & SB . z = x ) by A15, FUNCT_1:def 5;
( FSB . z = y & z in dom FSB ) by A26, A27, FUNCT_1:21, FUNCT_1:23;
hence y in rng FSB by FUNCT_1:def 5; :: thesis: verum

end;

rng FSB c= (Carrier L) /\ B

proof

let y be set ; :: 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 set such that
A28: x in dom FSB and
A29: FSB . x = y by FUNCT_1:def 5;
x in dom SB by A28, FUNCT_1:21;
then A30: SB . x in F " ((Carrier L) /\ B) by A15, FUNCT_1:def 5;
FSB . x = F . (SB . x) by A28, FUNCT_1:22;
hence y in (Carrier L) /\ B by A29, A30, FUNCT_1:def 13; :: thesis: verum

end;

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

A32: now

len (L (#) FSA) = len FSA by VECTSP_6:def 8;
then A33: dom (L (#) FSA) = dom FSA by FINSEQ_3:31;
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:46;
let k be Element of 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:46, RELAT_1:167;
then SA . k in F " ((Carrier L) /\ A) by A17, A36, A35, A33, FUNCT_1:def 5;
then A37: F . (SA . k) in (Carrier L) /\ A by FUNCT_1:def 13;
FSA /. k = FSA . k by A36, A35, A33, PARTFUN1:def 8
.= F . (SA . k) by A36, A35, A33, FUNCT_1:22 ;
then FSA /. k in A by A37, XBOOLE_0:def 4;
then f . (FSA /. k) in f .: A by A34, FUNCT_1:def 12;
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:22
.= f . ((L . (FSA /. k)) * (FSA /. k)) by A36, A35, VECTSP_6:def 8
.= (L . (FSA /. k)) * (0. V2) by A38, MOD_2:def 3
.= 0. V2 by VECTSP_1:59
.= (0. K) * v by VECTSP_1:59 ; :: 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, VECTSP_3:9;
FS = FSB ^ FSA by FINSEQOP:10;
then L (#) FS = (L (#) FSB) ^ (L (#) FSA) by VECTSP_6:37;
then A40: f * (L (#) FS) = (f * (L (#) FSB)) ^ (f * (L (#) FSA)) by FINSEQOP:10;
(f | B) | ((Carrier L) /\ B) = f | ((Carrier L) /\ B) by RELAT_1:103, XBOOLE_1:18;
then A41: f | ((Carrier L) /\ B) is one-to-one by A6, FUNCT_1:84;
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:160;
A46: 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 A31, RELAT_1:94 ;
Carrier Lf c= f .: B by A31, A9, A42, RELAT_1:156, XBOOLE_1:18;
then A47: Lf is Linear_Combination of f .: B by VECTSP_6:def 7;
f . (0. V1) = 0. V2 by RANKNULL:9;
then A48: 0. V2 = f . (Sum (L (#) FS)) by A5, VECTSP_9:5
.= Sum (f * (L (#) FS)) by MATRLIN:20
.= (Sum (f * (L (#) FSB))) + (Sum (f * (L (#) FSA))) by A40, RLVECT_1:58
.= (Sum (f * (L (#) FSB))) + (0. V2) by A39, VECTSP_1:59
.= Sum (Lf (#) (f * FSB)) by A43, RLVECT_1:def 7
.= Sum Lf by A3, A13, A41, A45, A46, VECTSP_6:def 9 ;
thus Carrier L c= A :: thesis: verum

proof

let x be set ; :: 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:20; :: thesis: verum

end;

end;

end;