let V be RealLinearSpace; :: thesis:
let A, B be Subset of V; :: thesis:

now :: thesis:

let v be object ; :: thesis:
assume v in Z_Lin (A \/ B) ; :: thesis:
then consider l being Linear_Combination of A \/ B such that
A1: ( v = Sum l & rng l c= INT ) ;
deffunc H₂( object ) -> set = l . $1;
set D = (Carrier l) \ A;
set C = (Carrier l) /\ A;
defpred S₁[ object ] means $1 in (Carrier l) /\ A;
defpred S₂[ object ] means $1 in (Carrier l) \ A;
A2: for x being object st x in the carrier of V holds
( ( S₁[x] implies H₂(x) in REAL ) & ( not S₁[x] implies H₁(x) in REAL ) ) by XREAL_0:def 1;
consider f being Function of the carrier of V,REAL such that
A3: for x being object st x in the carrier of V holds
( ( S₁[x] implies f . x = H₂(x) ) & ( not S₁[x] implies f . x = H₁(x) ) ) from FUNCT_2:sch 5(A2);
reconsider C = (Carrier l) /\ A as finite Subset of V ;
reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
for u being VECTOR of V st not u in C holds
f . u = 0 by A3;
then reconsider f = f as Linear_Combination of V by RLVECT_2:def 3;
A4: rng f c= INT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A5: y in rng f ; :: thesis:
consider x being object such that
A6: ( x in the carrier of V & y = f . x ) by A5, FUNCT_2:11;
reconsider z = x as VECTOR of V by A6;

per cases ;

suppose not z in C ; :: thesis:

then f . z = 0 by A3;
hence y in INT by A6, NUMBERS:17; :: thesis:

end;

suppose z in C ; :: thesis:

then f . z = l . z by A3;
then f . z in rng l by FUNCT_2:4;
hence y in INT by A6, A1; :: thesis:

end;

A7: Carrier f c= C

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in Carrier f ; :: thesis:
then A8: ex u being VECTOR of V st
( x = u & f . u <> 0 ) ;
assume not x in C ; :: thesis:
hence contradiction by A3, A8; :: thesis:

end;

C c= A by XBOOLE_1:17;
then Carrier f c= A by A7;
then reconsider f = f as Linear_Combination of A by RLVECT_2:def 6;
A9: for x being object st x in the carrier of V holds
( ( S₂[x] implies H₂(x) in REAL ) & ( not S₂[x] implies H₁(x) in REAL ) ) by XREAL_0:def 1;
consider g being Function of the carrier of V,REAL such that
A10: for x being object st x in the carrier of V holds
( ( S₂[x] implies g . x = H₂(x) ) & ( not S₂[x] implies g . x = H₁(x) ) ) from FUNCT_2:sch 5(A9);
reconsider D = (Carrier l) \ A as finite Subset of V ;
reconsider g = g as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
for u being VECTOR of V st not u in D holds
g . u = 0 by A10;
then reconsider g = g as Linear_Combination of V by RLVECT_2:def 3;
A11: rng g c= INT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A12: y in rng g ; :: thesis:
consider x being object such that
A13: ( x in the carrier of V & y = g . x ) by A12, FUNCT_2:11;
reconsider z = x as VECTOR of V by A13;

per cases ;

suppose not z in D ; :: thesis:

then g . z = 0 by A10;
hence y in INT by A13, NUMBERS:17; :: thesis:

end;

suppose z in D ; :: thesis:

then g . z = l . z by A10;
then g . z in rng l by FUNCT_2:4;
hence y in INT by A13, A1; :: thesis:

end;

A14: D c= B

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in D ; :: thesis:
then A15: ( x in Carrier l & not x in A ) by XBOOLE_0:def 5;
Carrier l c= A \/ B by RLVECT_2:def 6;
hence x in B by A15, XBOOLE_0:def 3; :: thesis:

end;

Carrier g c= D

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in Carrier g ; :: thesis:
then A16: ex u being VECTOR of V st
( x = u & g . u <> 0 ) ;
assume not x in D ; :: thesis:
hence contradiction by A10, A16; :: thesis:

end;

then Carrier g c= B by A14;
then reconsider g = g as Linear_Combination of B by RLVECT_2:def 6;
l = f + g

proof

let v be VECTOR of V; :: according to RLVECT_2:def 9 :: thesis:

now :: thesis:

per cases ;

suppose A17: v in C ; :: thesis:

A18: now :: thesis:

assume v in D ; :: thesis:
then not v in A by XBOOLE_0:def 5;
hence contradiction by A17, XBOOLE_0:def 4; :: thesis:

end;

thus (f + g) . v = (f . v) + (g . v) by RLVECT_2:def 10
.= (l . v) + (g . v) by A3, A17
.= (l . v) + z0 by A10, A18
.= l . v ; :: thesis:

end;

suppose A19: not v in C ; :: thesis:

now :: thesis:

per cases ;

suppose A20: v in Carrier l ; :: thesis:

A21: now :: thesis:

assume not v in D ; :: thesis:
then ( not v in Carrier l or v in A ) by XBOOLE_0:def 5;
hence contradiction by A19, A20, XBOOLE_0:def 4; :: thesis:

end;

thus (f + g) . v = (f . v) + (g . v) by RLVECT_2:def 10
.= z0 + (g . v) by A3, A19
.= l . v by A10, A21 ; :: thesis:

end;

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

then A23: not v in D by XBOOLE_0:def 5;
A24: not v in C by A22, XBOOLE_0:def 4;
thus (f + g) . v = (f . v) + (g . v) by RLVECT_2:def 10
.= z0 + (g . v) by A3, A24
.= z0 + z0 by A10, A23
.= l . v by A22 ; :: thesis:

end;

hence l . v = (f + g) . v ; :: thesis:

end;

hence l . v = (f + g) . v ; :: thesis:

end;

then A25: v = (Sum f) + (Sum g) by A1, RLVECT_3:1;
( Sum f in Z_Lin A & Sum g in Z_Lin B ) by A4, A11;
hence v in (Z_Lin A) + (Z_Lin B) by A25; :: thesis:

end;

then A26: Z_Lin (A \/ B) c= (Z_Lin A) + (Z_Lin B) ;
A27: ( Z_Lin A c= Z_Lin (A \/ B) & Z_Lin B c= Z_Lin (A \/ B) ) by Th13, XBOOLE_1:7;

now :: thesis:

let x be object ; :: thesis:
assume x in (Z_Lin A) + (Z_Lin B) ; :: thesis:
then consider u, v being Element of V such that
A28: ( x = u + v & u in Z_Lin A & v in Z_Lin B ) ;
thus x in Z_Lin (A \/ B) by A28, A27, Th9; :: thesis:

end;

then (Z_Lin A) + (Z_Lin B) c= Z_Lin (A \/ B) ;
hence Z_Lin (A \/ B) = (Z_Lin A) + (Z_Lin B) by A26, XBOOLE_0:def 10; :: thesis: