let X be non empty addLoopStr ; :: thesis:
let A, B be Subset of X; :: thesis:
let l be Linear_Combination of A \/ B; :: thesis:
reconsider T1 = (Carrier l) \ B as finite Subset of X ;
defpred S₁[ object , object ] means ( ( $1 in T1 implies $2 = l . $1 ) & ( not $1 in T1 implies $2 = 0 ) );

A1: 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 ;

suppose A2: x in T1 ; :: thesis:

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

end;

suppose A3: not x in T1 ; :: thesis:

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

end;

end;

end;

end;

consider l1 being Function of the carrier of X,REAL such that
A4: for x being object st x in the carrier of X holds
S₁[x,l1 . x] from FUNCT_2:sch 1(A1);
reconsider l1 = l1 as Element of Funcs ( the carrier of X,REAL) by FUNCT_2:8;
for x being Element of X st not x in T1 holds
l1 . x = 0 by A4;
then reconsider l1 = l1 as Linear_Combination of X by RLVECT_2:def 3;

now :: thesis:

let x be object ; :: thesis:
assume x in Carrier l1 ; :: thesis:
then ex v being Element of X st
( x = v & l1 . v <> 0 ) ;
hence x in T1 by A4; :: thesis:

end;

then A5: Carrier l1 c= T1 ;

now :: thesis:

let x be object ; :: thesis:
assume A6: x in T1 ; :: thesis:
then x in Carrier l by XBOOLE_0:def 5;
then l . x <> 0 by RLVECT_2:19;
then l1 . x <> 0 by A4, A6;
hence x in Carrier l1 by A6; :: thesis:

end;

then A7: T1 c= Carrier l1 ;
then A8: T1 = Carrier l1 by A5;
( T1 c= Carrier l & Carrier l c= A \/ B ) by RLVECT_2:def 6, XBOOLE_1:36;
then ( T1 c= A \/ B & T1 misses B ) by XBOOLE_1:79;
then reconsider l1 = l1 as Linear_Combination of A by A8, RLVECT_2:def 6, XBOOLE_1:73;
take l1 ; :: thesis:
thus Carrier l1 = (Carrier l) \ B by A5, A7; :: thesis:
thus for x being Element of X st x in Carrier l1 holds
l1 . x = l . x by A4, A5; :: thesis: