let V be RealLinearSpace; :: thesis:
let W be Subspace of V; :: thesis:
defpred S₁[ 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 & S₁[x] ) ) from XFAMILY:sch 1();
( W /\ ((0). V) = (0). V & (0). V in Subspaces V ) by Def3, Th18;
then reconsider X = X as non empty set by A1;
defpred S₂[ 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 S₂[x,y] ) from RELSET_1:sch 2();
defpred S₃[ set , set ] means [$1,$2] in R;

let x, y, z be Element of X; :: thesis:
assume that
A3: [x,y] in R and
A4: [y,z] in R ; :: thesis:
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 A6, A7, A9, RLSUB_1:27;
hence [x,z] in R by A2, A5, A8; :: thesis:

end;

then A10: for x, y, z being Element of X st S₃[x,y] & S₃[y,z] holds
S₃[x,z] ;

A11: now :: thesis:

let x be Element of X; :: thesis:
x in Subspaces V by A1;
hence x is strict Subspace of V by Def3; :: thesis:

end;

now :: thesis:

let x be Element of X; :: thesis:
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:

end;

then A12: for x being Element of X holds S₃[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:
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:

now :: thesis:

per cases ;

suppose A15: Y = {} ; :: thesis:

set y = the Element of X;
take y9 = the Element of X; :: thesis:
let x be Element of X; :: thesis:
assume x in Y ; :: thesis:
hence [x,y9] in R by A15; :: thesis:

end;

suppose A16: Y <> {} ; :: thesis:

defpred S₄[ 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 S₄[x,y]

proof

let x be object ; :: thesis:
assume x in Y ; :: thesis:
then consider W1 being strict Subspace of V such that
A18: x = W1 and
W /\ W1 = (0). V by A1, A13;
reconsider y = the carrier of W1 as set ;
take y ; :: thesis:
take W1 ; :: thesis:
thus ( x = W1 & y = the carrier of W1 ) by A18; :: thesis:

end;

consider f being Function such that
A19: dom f = Y and
A20: for x being object st x in Y holds
S₄[x,f . x] from CLASSES1:sch 1(A17);
set Z = union (rng f);

now :: thesis:

let x be object ; :: thesis:
assume x in union (rng f) ; :: thesis:
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 A22, FUNCT_1:def 3;
consider W1 being strict Subspace of V such that
y = W1 and
A25: f . y = the carrier of W1 by A19, A20, A23;
the carrier of W1 c= the carrier of V by RLSUB_1:def 2;
hence x in the carrier of V by A21, A24, A25; :: thesis:

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:

proof

let v1, v2 be VECTOR of V; :: thesis:
assume that
A27: v1 in Z and
A28: v2 in Z ; :: thesis:
consider Y1 being set such that
A29: v1 in Y1 and
A30: Y1 in rng f by A27, TARSKI:def 4;
consider y1 being object such that
A31: y1 in dom f and
A32: f . y1 = Y1 by A30, FUNCT_1:def 3;
consider Y2 being set such that
A33: v2 in Y2 and
A34: Y2 in rng f by A28, TARSKI:def 4;
consider y2 being object such that
A35: y2 in dom f and
A36: f . y2 = Y2 by A34, FUNCT_1:def 3;
consider W1 being strict Subspace of V such that
A37: y1 = W1 and
A38: f . y1 = the carrier of W1 by A19, A20, A31;
consider W2 being strict Subspace of V such that
A39: y2 = W2 and
A40: f . y2 = the carrier of W2 by A19, A20, A35;
reconsider y1 = y1, y2 = y2 as Element of X by A13, A19, A31, A35;

now :: thesis:

per cases in R or [y2,y1] in R ) by A14, A19, A31, A35;

suppose [y1,y2] in R ; :: thesis:

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 A37, A39, RLSUB_1:def 2;
then A41: v1 in W2 by A29, A32, A38, STRUCT_0:def 5;
v2 in W2 by A33, A36, A40, STRUCT_0:def 5;
then v1 + v2 in W2 by A41, RLSUB_1:20;
then A42: v1 + v2 in the carrier of W2 by STRUCT_0:def 5;
f . y2 in rng f by A35, FUNCT_1:def 3;
hence v1 + v2 in Z by A40, A42, TARSKI:def 4; :: thesis:

end;

suppose [y2,y1] in R ; :: thesis:

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 A37, A39, RLSUB_1:def 2;
then A43: v2 in W1 by A33, A36, A40, STRUCT_0:def 5;
v1 in W1 by A29, A32, A38, STRUCT_0:def 5;
then v1 + v2 in W1 by A43, RLSUB_1:20;
then A44: v1 + v2 in the carrier of W1 by STRUCT_0:def 5;
f . y1 in rng f by A31, FUNCT_1:def 3;
hence v1 + v2 in Z by A38, A44, TARSKI:def 4; :: thesis:

end;

hence v1 + v2 in Z ; :: thesis:

end;

let a be Real; :: thesis:
let v1 be VECTOR of V; :: thesis:
assume v1 in Z ; :: thesis:
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 A46, FUNCT_1:def 3;
consider W1 being strict Subspace of V such that
y1 = W1 and
A49: f . y1 = the carrier of W1 by A19, A20, A47;
v1 in W1 by A45, A48, A49, STRUCT_0:def 5;
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 A47, FUNCT_1:def 3;
hence a * v1 in Z by A49, A50, TARSKI:def 4; :: thesis:

end;

set z = the Element of rng f;
A51: rng f <> {} by A16, A19, RELAT_1:42;
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 A19, A20, A52;
then Z <> {} by A51, A53, ORDERS_1:6;
then consider E being strict Subspace of V such that
A54: Z = the carrier of E by A26, RLSUB_1:35;

now :: thesis:

let u be VECTOR of V; :: thesis:
thus ( u in W /\ E implies u in (0). V ) :: thesis:

proof

assume A55: u in W /\ E ; :: thesis:
then A56: u in W by Th3;
u in E by A55, Th3;
then u in Z by A54, STRUCT_0:def 5;
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 A58, FUNCT_1:def 3;
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 A19, A20, A59;
u in W1 by A57, A60, A63, STRUCT_0:def 5;
hence u in (0). V by A62, A56, A61, Th3; :: thesis:

end;

assume u in (0). V ; :: thesis:
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:

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 A1, A64;
take y = y9; :: thesis:
let x be Element of X; :: thesis:
assume A65: x in Y ; :: thesis:
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:

let u be VECTOR of V; :: thesis:
assume u in W1 ; :: thesis:
then A68: u in the carrier of W1 by STRUCT_0:def 5;
the carrier of W1 in rng f by A19, A65, A67, FUNCT_1:def 3;
then u in Z by A68, TARSKI:def 4;
hence u in E by A54, STRUCT_0:def 5; :: thesis:

end;

then W1 is strict Subspace of E by RLSUB_1:29;
hence [x,y] in R by A2, A66; :: thesis:

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:

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 S₃[x,y] holds
S₃[y,x] ) holds
ex y being Element of X st
for x being Element of X st x in Y holds
S₃[x,y] ;

now :: thesis:

let x, y be Element of X; :: thesis:
assume ( [x,y] in R & [y,x] in R ) ; :: thesis:
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:

end;

then A70: for x, y being Element of X st S₃[x,y] & S₃[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 S₃[x,y] from ORDERS_1:sch 1(A12, A70, A10, A69);
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:

proof

assume not RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) = L + W ; :: thesis:
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:

let x be object ; :: thesis:
assume x in { (a * v) where a is Real : verum } ; :: thesis:
then ex a being Real st x = a * v ;
hence x in the carrier of V ; :: thesis:

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:

proof

let v1, v2 be VECTOR of V; :: thesis:
assume v1 in A ; :: thesis:
then consider a1 being Real such that
A77: v1 = a1 * v ;
assume v2 in A ; :: thesis:
then consider a2 being Real such that
A78: v2 = a2 * v ;
v1 + v2 = (a1 + a2) * v by A77, A78, RLVECT_1:def 6;
hence v1 + v2 in A ; :: thesis:

end;

let a be Real; :: thesis:
let v1 be VECTOR of V; :: thesis:
assume v1 in A ; :: thesis:
then consider a1 being Real such that
A79: v1 = a1 * v ;
a * v1 = (a * a1) * v by A79, RLVECT_1:def 7;
hence a * v1 in A ; :: thesis:

end;

then consider Z being strict Subspace of V such that
A80: the carrier of Z = A by A76, RLSUB_1:35;
A81: not v in L + W by A74, Th1;

now :: thesis:

let u be VECTOR of V; :: thesis:
thus ( u in Z /\ (W + L) implies u in (0). V ) :: thesis:

proof

assume A82: u in Z /\ (W + L) ; :: thesis:
then u in Z by Th3;
then u in A by A80, STRUCT_0:def 5;
then consider a being Real such that
A83: u = a * v ;

now :: thesis:

u in W + L by A82, Th3;
then (a ") * (a * v) in W + L by A83, RLSUB_1:21;
then A84: ((a ") * a) * v in W + L by RLVECT_1:def 7;
assume a <> 0 ; :: thesis:
then 1 * v in W + L by A84, XCMPLX_0:def 7;
then 1 * v in L + W by Lm1;
hence contradiction by A81, RLVECT_1:def 8; :: thesis:

end;

then u = 0. V by A83, RLVECT_1:10;
hence u in (0). V by RLSUB_1:17; :: thesis:

end;

assume u in (0). V ; :: thesis:
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:

end;

then A85: Z /\ (W + L) = (0). V by RLSUB_1:31;

now :: thesis:

let u be VECTOR of V; :: thesis:
thus ( u in (Z + L) /\ W implies u in (0). V ) :: thesis:

proof

assume A86: u in (Z + L) /\ W ; :: thesis:
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 A86, Th3;
then A91: u in W + L by Th2;
( v1 = u - v2 & v2 in W + L ) by A88, A89, Lm14, Th2;
then v1 in W + L by A91, RLSUB_1:23;
then v1 in Z /\ (W + L) by A87, Th3;
then v1 in the carrier of ((0). V) by A85, STRUCT_0:def 5;
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:

end;

assume u in (0). V ; :: thesis:
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:

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 A1, A92;
L is Subspace of Z + L by Th7;
then A93: [x,x1] in R by A2, A72;
v in A by A76, RLVECT_1:def 8;
then v in Z by A80, STRUCT_0:def 5;
then Z + L <> L by A75, Th2;
hence contradiction by A71, A72, A93; :: thesis:

end;

thus L /\ W = (0). V by A73, Th14; :: thesis: