let V be RealLinearSpace; :: thesis: for W being Subspace of V ex C being strict Subspace of V st V is_the_direct_sum_of C,W
let W be Subspace of V; :: thesis: ex C being strict Subspace of V st V is_the_direct_sum_of C,W
defpred S1[ set ] means ex W1 being strict Subspace of V st
( \$1 = W1 & W /\ W1 = (0). V );
consider X being set such that
A1: for x being set holds
( x in X iff ( x in Subspaces V & S1[x] ) ) from ( W /\ ((0). V) = (0). V & (0). V in Subspaces V ) by ;
then reconsider X = X as non empty set by A1;
defpred S2[ set , set ] means ex W1, W2 being strict Subspace of V st
( \$1 = W1 & \$2 = W2 & W1 is Subspace of W2 );
consider R being Relation of X such that
A2: for x, y being Element of X holds
( [x,y] in R iff S2[x,y] ) from defpred S3[ set , set ] means [\$1,\$2] in R;
now :: thesis: for x, y, z being Element of X st [x,y] in R & [y,z] in R holds
[x,z] in R
let x, y, z be Element of X; :: thesis: ( [x,y] in R & [y,z] in R implies [x,z] in R )
assume that
A3: [x,y] in R and
A4: [y,z] in R ; :: thesis: [x,z] in R
consider W1, W2 being strict Subspace of V such that
A5: x = W1 and
A6: ( y = W2 & W1 is Subspace of W2 ) by A2, A3;
consider W3, W4 being strict Subspace of V such that
A7: y = W3 and
A8: z = W4 and
A9: W3 is Subspace of W4 by A2, A4;
W1 is strict Subspace of W4 by ;
hence [x,z] in R by A2, A5, A8; :: thesis: verum
end;
then A10: for x, y, z being Element of X st S3[x,y] & S3[y,z] holds
S3[x,z] ;
A11: now :: thesis: for x being Element of X holds x is strict Subspace of V
let x be Element of X; :: thesis: x is strict Subspace of V
x in Subspaces V by A1;
hence x is strict Subspace of V by Def3; :: thesis: verum
end;
now :: thesis: for x being Element of X holds [x,x] in R
let x be Element of X; :: thesis: [x,x] in R
reconsider W = x as strict Subspace of V by A11;
W is Subspace of W by RLSUB_1:25;
hence [x,x] in R by A2; :: thesis: verum
end;
then A12: for x being Element of X holds S3[x,x] ;
for Y being set st Y c= X & ( for x, y being Element of X st x in Y & y in Y & not [x,y] in R holds
[y,x] in R ) holds
ex y being Element of X st
for x being Element of X st x in Y holds
[x,y] in R
proof
let Y be set ; :: thesis: ( Y c= X & ( for x, y being Element of X st x in Y & y in Y & not [x,y] in R holds
[y,x] in R ) implies ex y being Element of X st
for x being Element of X st x in Y holds
[x,y] in R )

assume that
A13: Y c= X and
A14: for x, y being Element of X st x in Y & y in Y & not [x,y] in R holds
[y,x] in R ; :: thesis: ex y being Element of X st
for x being Element of X st x in Y holds
[x,y] in R

now :: thesis: ex y9 being Element of X st
for x being Element of X st x in Y holds
[x,y9] in R
per cases ( Y = {} or Y <> {} ) ;
suppose A15: Y = {} ; :: thesis: ex y9 being Element of X st
for x being Element of X st x in Y holds
[x,y9] in R

set y = the Element of X;
take y9 = the Element of X; :: thesis: for x being Element of X st x in Y holds
[x,y9] in R

let x be Element of X; :: thesis: ( x in Y implies [x,y9] in R )
assume x in Y ; :: thesis: [x,y9] in R
hence [x,y9] in R by A15; :: thesis: verum
end;
suppose A16: Y <> {} ; :: thesis: ex y being Element of X st
for x being Element of X st x in Y holds
[x,y] in R

defpred S4[ object , object ] means ex W1 being strict Subspace of V st
( \$1 = W1 & \$2 = the carrier of W1 );
A17: for x being object st x in Y holds
ex y being object st S4[x,y]
proof
let x be object ; :: thesis: ( x in Y implies ex y being object st S4[x,y] )
assume x in Y ; :: thesis: ex y being object st S4[x,y]
then consider W1 being strict Subspace of V such that
A18: x = W1 and
W /\ W1 = (0). V by ;
reconsider y = the carrier of W1 as set ;
take y ; :: thesis: S4[x,y]
take W1 ; :: thesis: ( x = W1 & y = the carrier of W1 )
thus ( x = W1 & y = the carrier of W1 ) by A18; :: thesis: verum
end;
consider f being Function such that
A19: dom f = Y and
A20: for x being object st x in Y holds
S4[x,f . x] from set Z = union (rng f);
now :: thesis: for x being object st x in union (rng f) holds
x in the carrier of V
let x be object ; :: thesis: ( x in union (rng f) implies x in the carrier of V )
assume x in union (rng f) ; :: thesis: x in the carrier of V
then consider Y9 being set such that
A21: x in Y9 and
A22: Y9 in rng f by TARSKI:def 4;
consider y being object such that
A23: y in dom f and
A24: f . y = Y9 by ;
consider W1 being strict Subspace of V such that
y = W1 and
A25: f . y = the carrier of W1 by ;
the carrier of W1 c= the carrier of V by RLSUB_1:def 2;
hence x in the carrier of V by ; :: thesis: verum
end;
then reconsider Z = union (rng f) as Subset of V by TARSKI:def 3;
A26: Z is linearly-closed
proof
thus for v1, v2 being VECTOR of V st v1 in Z & v2 in Z holds
v1 + v2 in Z :: according to RLSUB_1:def 1 :: thesis: for b1 being object
for b2 being Element of the carrier of V holds
( not b2 in Z or b1 * b2 in Z )
proof
let v1, v2 be VECTOR of V; :: thesis: ( v1 in Z & v2 in Z implies v1 + v2 in Z )
assume that
A27: v1 in Z and
A28: v2 in Z ; :: thesis: v1 + v2 in Z
consider Y1 being set such that
A29: v1 in Y1 and
A30: Y1 in rng f by ;
consider y1 being object such that
A31: y1 in dom f and
A32: f . y1 = Y1 by ;
consider Y2 being set such that
A33: v2 in Y2 and
A34: Y2 in rng f by ;
consider y2 being object such that
A35: y2 in dom f and
A36: f . y2 = Y2 by ;
consider W1 being strict Subspace of V such that
A37: y1 = W1 and
A38: f . y1 = the carrier of W1 by ;
consider W2 being strict Subspace of V such that
A39: y2 = W2 and
A40: f . y2 = the carrier of W2 by ;
reconsider y1 = y1, y2 = y2 as Element of X by A13, A19, A31, A35;
now :: thesis: v1 + v2 in Z
per cases ( [y1,y2] in R or [y2,y1] in R ) by A14, A19, A31, A35;
suppose [y1,y2] in R ; :: thesis: v1 + v2 in Z
then ex W3, W4 being strict Subspace of V st
( y1 = W3 & y2 = W4 & W3 is Subspace of W4 ) by A2;
then the carrier of W1 c= the carrier of W2 by ;
then A41: v1 in W2 by ;
v2 in W2 by ;
then v1 + v2 in W2 by ;
then A42: v1 + v2 in the carrier of W2 by STRUCT_0:def 5;
f . y2 in rng f by ;
hence v1 + v2 in Z by ; :: thesis: verum
end;
suppose [y2,y1] in R ; :: thesis: v1 + v2 in Z
then ex W3, W4 being strict Subspace of V st
( y2 = W3 & y1 = W4 & W3 is Subspace of W4 ) by A2;
then the carrier of W2 c= the carrier of W1 by ;
then A43: v2 in W1 by ;
v1 in W1 by ;
then v1 + v2 in W1 by ;
then A44: v1 + v2 in the carrier of W1 by STRUCT_0:def 5;
f . y1 in rng f by ;
hence v1 + v2 in Z by ; :: thesis: verum
end;
end;
end;
hence v1 + v2 in Z ; :: thesis: verum
end;
let a be Real; :: thesis: for b1 being Element of the carrier of V holds
( not b1 in Z or a * b1 in Z )

let v1 be VECTOR of V; :: thesis: ( not v1 in Z or a * v1 in Z )
assume v1 in Z ; :: thesis: a * v1 in Z
then consider Y1 being set such that
A45: v1 in Y1 and
A46: Y1 in rng f by TARSKI:def 4;
consider y1 being object such that
A47: y1 in dom f and
A48: f . y1 = Y1 by ;
consider W1 being strict Subspace of V such that
y1 = W1 and
A49: f . y1 = the carrier of W1 by ;
v1 in W1 by ;
then a * v1 in W1 by RLSUB_1:21;
then A50: a * v1 in the carrier of W1 by STRUCT_0:def 5;
f . y1 in rng f by ;
hence a * v1 in Z by ; :: thesis: verum
end;
set z = the Element of rng f;
A51: rng f <> {} by ;
then consider z1 being object such that
A52: z1 in dom f and
A53: f . z1 = the Element of rng f by FUNCT_1:def 3;
ex W3 being strict Subspace of V st
( z1 = W3 & f . z1 = the carrier of W3 ) by ;
then Z <> {} by ;
then consider E being strict Subspace of V such that
A54: Z = the carrier of E by ;
now :: thesis: for u being VECTOR of V holds
( ( u in W /\ E implies u in (0). V ) & ( u in (0). V implies u in W /\ E ) )
let u be VECTOR of V; :: thesis: ( ( u in W /\ E implies u in (0). V ) & ( u in (0). V implies u in W /\ E ) )
thus ( u in W /\ E implies u in (0). V ) :: thesis: ( u in (0). V implies u in W /\ E )
proof
assume A55: u in W /\ E ; :: thesis: u in (0). V
then A56: u in W by Th3;
u in E by ;
then u in Z by ;
then consider Y1 being set such that
A57: u in Y1 and
A58: Y1 in rng f by TARSKI:def 4;
consider y1 being object such that
A59: y1 in dom f and
A60: f . y1 = Y1 by ;
A61: ex W2 being strict Subspace of V st
( y1 = W2 & W /\ W2 = (0). V ) by A1, A13, A19, A59;
consider W1 being strict Subspace of V such that
A62: y1 = W1 and
A63: f . y1 = the carrier of W1 by ;
u in W1 by ;
hence u in (0). V by A62, A56, A61, Th3; :: thesis: verum
end;
assume u in (0). V ; :: thesis: u in W /\ E
then u in the carrier of ((0). V) by STRUCT_0:def 5;
then u in {(0. V)} by RLSUB_1:def 3;
then u = 0. V by TARSKI:def 1;
hence u in W /\ E by RLSUB_1:17; :: thesis: verum
end;
then A64: W /\ E = (0). V by RLSUB_1:31;
E in Subspaces V by Def3;
then reconsider y9 = E as Element of X by ;
take y = y9; :: thesis: for x being Element of X st x in Y holds
[x,y] in R

let x be Element of X; :: thesis: ( x in Y implies [x,y] in R )
assume A65: x in Y ; :: thesis: [x,y] in R
then consider W1 being strict Subspace of V such that
A66: x = W1 and
A67: f . x = the carrier of W1 by A20;
now :: thesis: for u being VECTOR of V st u in W1 holds
u in E
let u be VECTOR of V; :: thesis: ( u in W1 implies u in E )
assume u in W1 ; :: thesis: u in E
then A68: u in the carrier of W1 by STRUCT_0:def 5;
the carrier of W1 in rng f by ;
then u in Z by ;
hence u in E by ; :: thesis: verum
end;
then W1 is strict Subspace of E by RLSUB_1:29;
hence [x,y] in R by ; :: thesis: verum
end;
end;
end;
hence ex y being Element of X st
for x being Element of X st x in Y holds
[x,y] in R ; :: thesis: verum
end;
then A69: for Y being set st Y c= X & ( for x, y being Element of X st x in Y & y in Y & not S3[x,y] holds
S3[y,x] ) holds
ex y being Element of X st
for x being Element of X st x in Y holds
S3[x,y] ;
now :: thesis: for x, y being Element of X st [x,y] in R & [y,x] in R holds
x = y
let x, y be Element of X; :: thesis: ( [x,y] in R & [y,x] in R implies x = y )
assume ( [x,y] in R & [y,x] in R ) ; :: thesis: x = y
then ( ex W1, W2 being strict Subspace of V st
( x = W1 & y = W2 & W1 is Subspace of W2 ) & ex W3, W4 being strict Subspace of V st
( y = W3 & x = W4 & W3 is Subspace of W4 ) ) by A2;
hence x = y by RLSUB_1:26; :: thesis: verum
end;
then A70: for x, y being Element of X st S3[x,y] & S3[y,x] holds
x = y ;
consider x being Element of X such that
A71: for y being Element of X st x <> y holds
not S3[x,y] from consider L being strict Subspace of V such that
A72: x = L and
A73: W /\ L = (0). V by A1;
take L ; :: thesis:
thus RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) = L + W :: according to RLSUB_2:def 4 :: thesis: L /\ W = (0). V
proof
assume not RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) = L + W ; :: thesis: contradiction
then consider v being VECTOR of V such that
A74: for v1, v2 being VECTOR of V holds
( not v1 in L or not v2 in W or v <> v1 + v2 ) by Lm13;
( v = (0. V) + v & 0. V in W ) by RLSUB_1:17;
then A75: not v in L by A74;
set A = { (a * v) where a is Real : verum } ;
A76: 1 * v in { (a * v) where a is Real : verum } ;
now :: thesis: for x being object st x in { (a * v) where a is Real : verum } holds
x in the carrier of V
let x be object ; :: thesis: ( x in { (a * v) where a is Real : verum } implies x in the carrier of V )
assume x in { (a * v) where a is Real : verum } ; :: thesis: x in the carrier of V
then ex a being Real st x = a * v ;
hence x in the carrier of V ; :: thesis: verum
end;
then reconsider A = { (a * v) where a is Real : verum } as Subset of V by TARSKI:def 3;
A is linearly-closed
proof
thus for v1, v2 being VECTOR of V st v1 in A & v2 in A holds
v1 + v2 in A :: according to RLSUB_1:def 1 :: thesis: for b1 being object
for b2 being Element of the carrier of V holds
( not b2 in A or b1 * b2 in A )
proof
let v1, v2 be VECTOR of V; :: thesis: ( v1 in A & v2 in A implies v1 + v2 in A )
assume v1 in A ; :: thesis: ( not v2 in A or v1 + v2 in A )
then consider a1 being Real such that
A77: v1 = a1 * v ;
assume v2 in A ; :: thesis: v1 + v2 in A
then consider a2 being Real such that
A78: v2 = a2 * v ;
v1 + v2 = (a1 + a2) * v by ;
hence v1 + v2 in A ; :: thesis: verum
end;
let a be Real; :: thesis: for b1 being Element of the carrier of V holds
( not b1 in A or a * b1 in A )

let v1 be VECTOR of V; :: thesis: ( not v1 in A or a * v1 in A )
assume v1 in A ; :: thesis: a * v1 in A
then consider a1 being Real such that
A79: v1 = a1 * v ;
a * v1 = (a * a1) * v by ;
hence a * v1 in A ; :: thesis: verum
end;
then consider Z being strict Subspace of V such that
A80: the carrier of Z = A by ;
A81: not v in L + W by ;
now :: thesis: for u being VECTOR of V holds
( ( u in Z /\ (W + L) implies u in (0). V ) & ( u in (0). V implies u in Z /\ (W + L) ) )
let u be VECTOR of V; :: thesis: ( ( u in Z /\ (W + L) implies u in (0). V ) & ( u in (0). V implies u in Z /\ (W + L) ) )
thus ( u in Z /\ (W + L) implies u in (0). V ) :: thesis: ( u in (0). V implies u in Z /\ (W + L) )
proof
assume A82: u in Z /\ (W + L) ; :: thesis: u in (0). V
then u in Z by Th3;
then u in A by ;
then consider a being Real such that
A83: u = a * v ;
now :: thesis: not a <> 0
u in W + L by ;
then (a ") * (a * v) in W + L by ;
then A84: ((a ") * a) * v in W + L by RLVECT_1:def 7;
assume a <> 0 ; :: thesis: contradiction
then 1 * v in W + L by ;
then 1 * v in L + W by Lm1;
hence contradiction by A81, RLVECT_1:def 8; :: thesis: verum
end;
then u = 0. V by ;
hence u in (0). V by RLSUB_1:17; :: thesis: verum
end;
assume u in (0). V ; :: thesis: u in Z /\ (W + L)
then u in the carrier of ((0). V) by STRUCT_0:def 5;
then u in {(0. V)} by RLSUB_1:def 3;
then u = 0. V by TARSKI:def 1;
hence u in Z /\ (W + L) by RLSUB_1:17; :: thesis: verum
end;
then A85: Z /\ (W + L) = (0). V by RLSUB_1:31;
now :: thesis: for u being VECTOR of V holds
( ( u in (Z + L) /\ W implies u in (0). V ) & ( u in (0). V implies u in (Z + L) /\ W ) )
let u be VECTOR of V; :: thesis: ( ( u in (Z + L) /\ W implies u in (0). V ) & ( u in (0). V implies u in (Z + L) /\ W ) )
thus ( u in (Z + L) /\ W implies u in (0). V ) :: thesis: ( u in (0). V implies u in (Z + L) /\ W )
proof
assume A86: u in (Z + L) /\ W ; :: thesis: u in (0). V
then u in Z + L by Th3;
then consider v1, v2 being VECTOR of V such that
A87: v1 in Z and
A88: v2 in L and
A89: u = v1 + v2 by Th1;
A90: u in W by ;
then A91: u in W + L by Th2;
( v1 = u - v2 & v2 in W + L ) by ;
then v1 in W + L by ;
then v1 in Z /\ (W + L) by ;
then v1 in the carrier of ((0). V) by ;
then v1 in {(0. V)} by RLSUB_1:def 3;
then v1 = 0. V by TARSKI:def 1;
then v2 = u by A89;
hence u in (0). V by A73, A88, A90, Th3; :: thesis: verum
end;
assume u in (0). V ; :: thesis: u in (Z + L) /\ W
then u in the carrier of ((0). V) by STRUCT_0:def 5;
then u in {(0. V)} by RLSUB_1:def 3;
then u = 0. V by TARSKI:def 1;
hence u in (Z + L) /\ W by RLSUB_1:17; :: thesis: verum
end;
then (Z + L) /\ W = (0). V by RLSUB_1:31;
then A92: W /\ (Z + L) = (0). V by Th14;
Z + L in Subspaces V by Def3;
then reconsider x1 = Z + L as Element of X by ;
L is Subspace of Z + L by Th7;
then A93: [x,x1] in R by ;
v in A by ;
then v in Z by ;
then Z + L <> L by ;
hence contradiction by A71, A72, A93; :: thesis: verum
end;
thus L /\ W = (0). V by ; :: thesis: verum