let X be non empty addLoopStr ; :: thesis:
let A, B be Subset of X; :: thesis:
let l1 be Linear_Combination of A; :: thesis:
let l2 be Linear_Combination of B; :: thesis:
assume A1: A misses B ; :: thesis:
A2: ( Carrier l1 c= A & Carrier l2 c= B ) by RLVECT_2:def 6;
defpred S₁[ object , object ] means ( ( $1 in Carrier l1 implies $2 = l1 . $1 ) & ( $1 in Carrier l2 implies $2 = l2 . $1 ) & ( not $1 in Carrier l1 & not $1 in Carrier l2 implies $2 = 0 ) );

A4: now :: thesis:

let x be object ; :: thesis:
assume x in the carrier of X ; :: thesis:
thus ex y being object st
( y in REAL & S₁[x,y] ) :: thesis:

proof

per cases by A1, A2, XBOOLE_0:3;

suppose A5: ( x in Carrier l1 & not x in Carrier l2 ) ; :: thesis:

take y = l1 . x; :: thesis:
thus ( y in REAL & S₁[x,y] ) by A5, FUNCT_2:5; :: thesis:

end;

suppose A6: ( not x in Carrier l1 & x in Carrier l2 ) ; :: thesis:

take y = l2 . x; :: thesis:
thus ( y in REAL & S₁[x,y] ) by A6, FUNCT_2:5; :: thesis:

end;

suppose A7: ( not x in Carrier l1 & not x in Carrier l2 ) ; :: thesis:

take y = 0 ; :: thesis:
thus ( y in REAL & S₁[x,y] ) by A7, XREAL_0:def 1; :: thesis:

end;

end;

end;

end;

consider l being Function of the carrier of X,REAL such that
A8: for x being object st x in the carrier of X holds
S₁[x,l . x] from FUNCT_2:sch 1(A4);
reconsider l = l as Element of Funcs ( the carrier of X,REAL) by FUNCT_2:8;
reconsider T = (Carrier l1) \/ (Carrier l2) as finite Subset of X ;
for x being Element of X st not x in T holds
l . x = 0

proof

let x be Element of X; :: thesis:
assume not x in T ; :: thesis:
then ( not x in Carrier l1 & not x in Carrier l2 ) by XBOOLE_0:def 3;
hence l . x = 0 by A8; :: thesis:

end;

then reconsider l = l as Linear_Combination of X by RLVECT_2:def 3;

now :: thesis:

let x be object ; :: thesis:
assume x in Carrier l ; :: thesis:
then consider p being Element of X such that
A9: ( x = p & l . p <> 0 ) ;
( x in Carrier l1 or x in Carrier l2 ) by A8, A9;
hence x in (Carrier l1) \/ (Carrier l2) by XBOOLE_0:def 3; :: thesis:

end;

then A10: Carrier l c= (Carrier l1) \/ (Carrier l2) ;

now :: thesis:

let x be object ; :: thesis:
assume x in (Carrier l1) \/ (Carrier l2) ; :: thesis:

per cases by XBOOLE_0:def 3;

suppose A11: x in Carrier l1 ; :: thesis:

then consider p being Element of X such that
A12: ( x = p & l1 . p <> 0 ) ;
l . x <> 0 by A8, A11, A12;
hence x in Carrier l by A12; :: thesis:

end;

suppose A13: x in Carrier l2 ; :: thesis:

then consider p being Element of X such that
A14: ( x = p & l2 . p <> 0 ) ;
l . x <> 0 by A8, A13, A14;
hence x in Carrier l by A14; :: thesis:

end;

end;

end;

then A15: (Carrier l1) \/ (Carrier l2) c= Carrier l ;
then A16: Carrier l = (Carrier l1) \/ (Carrier l2) by A10;
then reconsider l = l as Linear_Combination of A \/ B by A2, RLVECT_2:def 6, XBOOLE_1:13;
take l ; :: thesis:
thus Carrier l = (Carrier l1) \/ (Carrier l2) by A10, A15; :: thesis:
for v being Element of X holds l . v = (l1 . v) + (l2 . v)

proof

let v be Element of X; :: thesis:

per cases by A10, XBOOLE_0:def 3;

suppose A17: v in Carrier l1 ; :: thesis:

then not v in Carrier l2 by A1, A2, XBOOLE_0:3;
then ( l . v = l1 . v & l2 . v = 0 ) by A8, A17;
hence l . v = (l1 . v) + (l2 . v) ; :: thesis:

end;

suppose A18: v in Carrier l2 ; :: thesis:

then not v in Carrier l1 by A1, A2, XBOOLE_0:3;
then ( l . v = l2 . v & l1 . v = 0 ) by A8, A18;
hence l . v = (l1 . v) + (l2 . v) ; :: thesis:

end;

suppose A19: not v in Carrier l ; :: thesis:

then ( not v in Carrier l1 & not v in Carrier l2 ) by A16, XBOOLE_0:def 3;
then ( l1 . v = 0 & l2 . v = 0 ) ;
hence l . v = (l1 . v) + (l2 . v) by A19; :: thesis:

end;

end;

end;

hence l = l1 + l2 by RLVECT_2:def 10; :: thesis: