let K be Ring; for V being VectSp of K
for A1, A2 being Subset of V
for l being Linear_Combination of A1 \/ A2 st A1 /\ A2 = {} holds
ex l1 being Linear_Combination of A1 ex l2 being Linear_Combination of A2 st l = l1 + l2
let V be VectSp of K; for A1, A2 being Subset of V
for l being Linear_Combination of A1 \/ A2 st A1 /\ A2 = {} holds
ex l1 being Linear_Combination of A1 ex l2 being Linear_Combination of A2 st l = l1 + l2
let A1, A2 be Subset of V; for l being Linear_Combination of A1 \/ A2 st A1 /\ A2 = {} holds
ex l1 being Linear_Combination of A1 ex l2 being Linear_Combination of A2 st l = l1 + l2
let l be Linear_Combination of A1 \/ A2; ( A1 /\ A2 = {} implies ex l1 being Linear_Combination of A1 ex l2 being Linear_Combination of A2 st l = l1 + l2 )
assume A1:
A1 /\ A2 = {}
; ex l1 being Linear_Combination of A1 ex l2 being Linear_Combination of A2 st l = l1 + l2
A2:
A1 misses A2
by A1;
defpred S1[ object , object ] means ( not $1 is Vector of V or ( $1 in A1 & $2 = l . $1 ) or ( not $1 in A1 & $2 = 0. K ) );
A3:
for x being object st x in the carrier of V holds
ex y being object st
( y in the carrier of K & S1[x,y] )
ex l1 being Function of the carrier of V, the carrier of K st
for x being object st x in the carrier of V holds
S1[x,l1 . x]
from FUNCT_2:sch 1(A3);
then consider l1 being Function of the carrier of V, the carrier of K such that
A4:
for x being object st x in the carrier of V holds
S1[x,l1 . x]
;
reconsider l1 = l1 as Element of Funcs ( the carrier of V, the carrier of K) by FUNCT_2:8;
reconsider l1 = l1 as Linear_Combination of V by A5, VECTSP_6:def 1;
for x being object st x in Carrier l1 holds
x in A1
then AX1:
l1 is Linear_Combination of A1
by TARSKI:def 3, VECTSP_6:def 4;
defpred S2[ object , object ] means ( not $1 is Vector of V or ( $1 in A2 & $2 = l . $1 ) or ( not $1 in A2 & $2 = 0. K ) );
A7:
for x being object st x in the carrier of V holds
ex y being object st
( y in the carrier of K & S2[x,y] )
ex l2 being Function of the carrier of V, the carrier of K st
for x being object st x in the carrier of V holds
S2[x,l2 . x]
from FUNCT_2:sch 1(A7);
then consider l2 being Function of the carrier of V, the carrier of K such that
A8:
for x being object st x in the carrier of V holds
S2[x,l2 . x]
;
reconsider l2 = l2 as Element of Funcs ( the carrier of V, the carrier of K) by FUNCT_2:8;
reconsider l2 = l2 as Linear_Combination of V by A9, VECTSP_6:def 1;
for x being object st x in Carrier l2 holds
x in A2
then AX2:
l2 is Linear_Combination of A2
by TARSKI:def 3, VECTSP_6:def 4;
for v being Vector of V holds l . v = (l1 + l2) . v
hence
ex l1 being Linear_Combination of A1 ex l2 being Linear_Combination of A2 st l = l1 + l2
by AX1, AX2, VECTSP_6:def 7; verum