let V be RealUnitarySpace; :: thesis: for A, B being Subset of V holds Lin (A \/ B) = (Lin A) + (Lin B)
let A, B be Subset of V; :: thesis: Lin (A \/ B) = (Lin A) + (Lin B)
( Lin A is Subspace of Lin (A \/ B) & Lin B is Subspace of Lin (A \/ B) ) by Th7, XBOOLE_1:7;
then A1: (Lin A) + (Lin B) is Subspace of Lin (A \/ B) by Lm5;

now

let v be VECTOR of V; :: thesis: ( v in Lin (A \/ B) implies v in (Lin A) + (Lin B) )
assume v in Lin (A \/ B) ; :: thesis: v in (Lin A) + (Lin B)
then consider l being Linear_Combination of A \/ B such that
A2: v = Sum l by Th1;
set C = (Carrier l) /\ A;
set D = (Carrier l) \ A;

A3: now

let x be set ; :: thesis: ( x in the carrier of V implies ( ( x in (Carrier l) /\ A implies l . x in REAL ) & ( not x in (Carrier l) /\ A implies 0 in REAL ) ) )
assume x in the carrier of V ; :: thesis: ( ( x in (Carrier l) /\ A implies l . x in REAL ) & ( not x in (Carrier l) /\ A implies 0 in REAL ) )
then reconsider v = x as VECTOR of V ;
for f being Function of the carrier of V,REAL holds f . v in REAL ;
hence ( x in (Carrier l) /\ A implies l . x in REAL ) ; :: thesis: ( not x in (Carrier l) /\ A implies 0 in REAL )
assume not x in (Carrier l) /\ A ; :: thesis: 0 in REAL
thus 0 in REAL ; :: thesis: verum

end;

defpred S₁[ set ] means $1 in (Carrier l) /\ A;
deffunc H₁( set ) -> set = l . $1;
deffunc H₂( set ) -> Element of NAT = 0 ;
A4: for x being set st x in the carrier of V holds
( ( S₁[x] implies H₁(x) in REAL ) & ( not S₁[x] implies H₂(x) in REAL ) ) by A3;
consider f being Function of the carrier of V,REAL such that
A5: for x being set 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(A4);
reconsider f = f as Element of Funcs the carrier of V,REAL by FUNCT_2:11;

A6: now

let x be set ; :: thesis: ( x in the carrier of V implies ( ( x in (Carrier l) \ A implies l . x in REAL ) & ( not x in (Carrier l) \ A implies 0 in REAL ) ) )
assume x in the carrier of V ; :: thesis: ( ( x in (Carrier l) \ A implies l . x in REAL ) & ( not x in (Carrier l) \ A implies 0 in REAL ) )
then reconsider v = x as VECTOR of V ;
for g being Function of the carrier of V,REAL holds g . v in REAL ;
hence ( x in (Carrier l) \ A implies l . x in REAL ) ; :: thesis: ( not x in (Carrier l) \ A implies 0 in REAL )
assume not x in (Carrier l) \ A ; :: thesis: 0 in REAL
thus 0 in REAL ; :: thesis: verum

end;

defpred S₂[ set ] means $1 in (Carrier l) \ A;
A7: for x being set st x in the carrier of V holds
( ( S₂[x] implies H₁(x) in REAL ) & ( not S₂[x] implies H₂(x) in REAL ) ) by A6;
consider g being Function of the carrier of V,REAL such that
A8: for x being set 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(A7);
reconsider g = g as Element of Funcs the carrier of V,REAL by FUNCT_2:11;
reconsider C = (Carrier l) /\ A as finite Subset of V ;
for u being VECTOR of V st not u in C holds
f . u = 0 by A5;
then reconsider f = f as Linear_Combination of V by RLVECT_2:def 5;
A9: Carrier f c= C

proof

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

end;

C c= A by XBOOLE_1:17;
then Carrier f c= A by A9, XBOOLE_1:1;
then reconsider f = f as Linear_Combination of A by RLVECT_2:def 8;
reconsider D = (Carrier l) \ A as finite Subset of V ;
for u being VECTOR of V st not u in D holds
g . u = 0 by A8;
then reconsider g = g as Linear_Combination of V by RLVECT_2:def 5;
A11: Carrier g c= D

proof

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

end;

D c= B

proof

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

end;

then Carrier g c= B by A11, XBOOLE_1:1;
then reconsider g = g as Linear_Combination of B by RLVECT_2:def 8;
l = f + g

proof

let v be VECTOR of V; :: according to RLVECT_2:def 11 :: thesis: l . v = (f + g) . v

now

per cases ( v in C or not v in C ) ;

suppose A13: v in C ; :: thesis: (f + g) . v = l . v

A14: now

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

end;

thus (f + g) . v = (f . v) + (g . v) by RLVECT_2:def 12
.= (l . v) + (g . v) by A5, A13
.= (l . v) + 0 by A8, A14
.= l . v ; :: thesis: verum

end;

suppose A15: not v in C ; :: thesis: l . v = (f + g) . v

now

per cases ( v in Carrier l or not v in Carrier l ) ;

suppose A16: v in Carrier l ; :: thesis: (f + g) . v = l . v

A17: now

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

end;

thus (f + g) . v = (f . v) + (g . v) by RLVECT_2:def 12
.= 0 + (g . v) by A5, A15
.= l . v by A8, A17 ; :: thesis: verum

end;

suppose A18: not v in Carrier l ; :: thesis: (f + g) . v = l . v

then A19: ( not v in C & not v in D ) by XBOOLE_0:def 4, XBOOLE_0:def 5;
thus (f + g) . v = (f . v) + (g . v) by RLVECT_2:def 12
.= 0 + (g . v) by A5, A19
.= 0 + 0 by A8, A19
.= l . v by A18 ; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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

end;

then A20: v = (Sum f) + (Sum g) by A2, RLVECT_3:1;
( Sum f in Lin A & Sum g in Lin B ) by Th1;
hence v in (Lin A) + (Lin B) by A20, RUSUB_2:1; :: thesis: verum

end;

then Lin (A \/ B) is Subspace of (Lin A) + (Lin B) by RUSUB_1:23;
hence Lin (A \/ B) = (Lin A) + (Lin B) by A1, RUSUB_1:20; :: thesis: verum