let V be Z_Module; :: 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)

now :: thesis: for v being VECTOR of V st v in Lin (A \/ B) holds
v in (Lin A) + (Lin B)

deffunc H₁( object ) -> Element of NAT = 0 ;
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 Z_Linear_Combination of A \/ B such that
A1: v = Sum l by Th64;
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 INT ) & ( not S₁[x] implies H₁(x) in INT ) ) by INT_1:def 2;
consider f being Function of the carrier of V,INT 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,INT) 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 Z_Linear_Combination of V by Def18;
A4: Carrier f c= C

proof

let x be object ; :: 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;
then reconsider f = f as Z_Linear_Combination of A by Def21;
A6: for x being object st x in the carrier of V holds
( ( S₂[x] implies H₂(x) in INT ) & ( not S₂[x] implies H₁(x) in INT ) ) by INT_1:def 2;
consider g being Function of the carrier of V,INT such that
A7: 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(A6);
reconsider D = (Carrier l) \ A as finite Subset of V ;
reconsider g = g as Element of Funcs ( the carrier of V,INT) by FUNCT_2:8;
for u being VECTOR of V st not u in D holds
g . u = 0 by A7;
then reconsider g = g as Z_Linear_Combination of V by Def18;
A8: D c= B

proof

let x be object ; :: 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 Def21;
hence x in B by A9, XBOOLE_0:def 3; :: thesis: verum

end;

Carrier g c= D

proof

let x be object ; :: 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;
then reconsider g = g as Z_Linear_Combination of B by Def21;
l = f + g

proof

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

now :: thesis: (f + g) . v = l . v

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

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

A12: now :: thesis: not v in D

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;

A13: g . v = 0 by A7, A12;
thus (f + g) . v = (f . v) + (g . v) by Def25
.= l . v by A3, A11, A13 ; :: thesis: verum

end;

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

now :: thesis: (f + g) . v = l . v

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

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

A16: now :: thesis: v in D

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

end;

A17: f . v = 0 by A3, A14;
thus (f + g) . v = (f . v) + (g . v) by Def25
.= l . v by A7, A16, A17 ; :: thesis: verum

end;

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

then A19: not v in D by XBOOLE_0:def 5;
A20: not v in C by A18, XBOOLE_0:def 4;
A21: g . v = 0 by A7, A19;
thus (f + g) . v = (f . v) + (g . v) by Def25
.= 0 by A3, A20, A21
.= 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 A22: v = (Sum f) + (Sum g) by A1, Th52;
( Sum f in Lin A & Sum g in Lin B ) by Th64;
hence v in (Lin A) + (Lin B) by A22, ZMODUL01:92; :: thesis: verum

end;

then A23: Lin (A \/ B) is Submodule of (Lin A) + (Lin B) by ZMODUL01:44;
( Lin A is Submodule of Lin (A \/ B) & Lin B is Submodule of Lin (A \/ B) ) by Th70, XBOOLE_1:7;
then (Lin A) + (Lin B) is Submodule of Lin (A \/ B) by Lm4;
hence Lin (A \/ B) = (Lin A) + (Lin B) by A23, ZMODUL01:41; :: thesis: verum