let V be RealLinearSpace; :: thesis: for A, B being Subset of V holds Z_Lin (A \/ B) = (Z_Lin A) + (Z_Lin B)
let A, B be Subset of V; :: thesis: Z_Lin (A \/ B) = (Z_Lin A) + (Z_Lin B)

now

let v be set ; :: thesis: ( v in Z_Lin (A \/ B) implies v in (Z_Lin A) + (Z_Lin B) )
assume v in Z_Lin (A \/ B) ; :: thesis: v in (Z_Lin A) + (Z_Lin B)
then consider l being Linear_Combination of A \/ B such that
A1: ( v = Sum l & rng l c= INT ) ;
deffunc H₂( set ) -> Element of REAL = l . $1;
set D = (Carrier l) \ A;
set C = (Carrier l) /\ A;
defpred S₁[ set ] means $1 in (Carrier l) /\ A;
defpred S₂[ set ] means $1 in (Carrier l) \ A;
A2: 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 ) ) ;
consider f being Function of the carrier of V,REAL such that
A3: 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(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:11;
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 5;
B3: rng f c= INT

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in INT )
assume AD: y in rng f ; :: thesis: y in INT
consider x being set such that
R1: ( x in the carrier of V & y = f . x ) by AD, FUNCT_2:17;
reconsider z = x as VECTOR of V by R1;

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

suppose not z in C ; :: thesis: y in INT

then f . z = 0 by A3;
hence y in INT by R1, NUMBERS:17, TARSKI:def 3; :: thesis: verum

end;

suppose z in C ; :: thesis: y in INT

then f . z = l . z by A3;
then f . z in rng l by FUNCT_2:6;
hence y in INT by R1, A1; :: thesis: verum

end;

end;

end;

A4: 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 A5: ex u being VECTOR of V st
( x = u & f . u <> 0 ) ;
assume not x in C ; :: thesis: contradiction
hence contradiction by A3, A5; :: thesis: verum

end;

C c= A by XBOOLE_1:17;
then Carrier f c= A by A4, XBOOLE_1:1;
then reconsider f = f as Linear_Combination of A by RLVECT_2:def 8;
A6: 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 ) ) ;
consider g being Function of the carrier of V,REAL such that
A7: 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(A6);
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:11;
for u being VECTOR of V st not u in D holds
g . u = 0 by A7;
then reconsider g = g as Linear_Combination of V by RLVECT_2:def 5;
B7: rng g c= INT

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng g or y in INT )
assume AD: y in rng g ; :: thesis: y in INT
consider x being set such that
R1: ( x in the carrier of V & y = g . x ) by AD, FUNCT_2:17;
reconsider z = x as VECTOR of V by R1;

per cases ( not z in D or z in D ) ;

suppose not z in D ; :: thesis: y in INT

then g . z = 0 by A7;
hence y in INT by R1, NUMBERS:17, TARSKI:def 3; :: thesis: verum

end;

suppose z in D ; :: thesis: y in INT

then g . z = l . z by A7;
then g . z in rng l by FUNCT_2:6;
hence y in INT by R1, A1; :: thesis: verum

end;

end;

end;

A8: 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 A9: ( x in Carrier l & not x in A ) by XBOOLE_0:def 5;
Carrier l c= A \/ B by RLVECT_2:def 8;
hence x in B by A9, XBOOLE_0:def 3; :: thesis: verum

end;

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 A10: ex u being VECTOR of V st
( x = u & g . u <> 0 ) ;
assume not x in D ; :: thesis: contradiction
hence contradiction by A7, A10; :: thesis: verum

end;

then Carrier g c= B by A8, 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 A11: v in C ; :: thesis: (f + g) . v = l . v

A12: now

assume v in D ; :: thesis: contradiction
then not v in A by XBOOLE_0:def 5;
hence contradiction by A11, 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 A3, A11
.= (l . v) + z0 by A7, A12
.= l . v ; :: thesis: verum

end;

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

now

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

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

A15: 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 A13, A14, XBOOLE_0:def 4; :: thesis: verum

end;

thus (f + g) . v = (f . v) + (g . v) by RLVECT_2:def 12
.= z0 + (g . v) by A3, A13
.= l . v by A7, A15 ; :: thesis: verum

end;

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

then A17: not v in D by XBOOLE_0:def 5;
A18: not v in C by A16, XBOOLE_0:def 4;
thus (f + g) . v = (f . v) + (g . v) by RLVECT_2:def 12
.= z0 + (g . v) by A3, A18
.= z0 + z0 by A7, A17
.= l . v by A16 ; :: 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 A19: v = (Sum f) + (Sum g) by A1, RLVECT_3:1;
( Sum f in Z_Lin A & Sum g in Z_Lin B ) by B3, B7;
hence v in (Z_Lin A) + (Z_Lin B) by A19; :: thesis: verum

end;

then A20: Z_Lin (A \/ B) c= (Z_Lin A) + (Z_Lin B) by TARSKI:def 3;
XX1: ( Z_Lin A c= Z_Lin (A \/ B) & Z_Lin B c= Z_Lin (A \/ B) ) by Th23, XBOOLE_1:7;

now

let x be set ; :: thesis: ( x in (Z_Lin A) + (Z_Lin B) implies x in Z_Lin (A \/ B) )
assume x in (Z_Lin A) + (Z_Lin B) ; :: thesis: x in Z_Lin (A \/ B)
then consider u, v being Element of V such that
A21: ( x = u + v & u in Z_Lin A & v in Z_Lin B ) ;
thus x in Z_Lin (A \/ B) by A21, XX1, LM010; :: thesis: verum

end;

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