defpred S₁[ set , set ] means ex W1, W2 being strict Subspace of V st
( $1 = W1 & $2 = W2 & W1 is Subspace of W2 );
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, Th20;
then reconsider X = X as non empty set by A1;
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 be Element of X; :: thesis:
assume ( S₃[x,y] & S₃[y,x] ) ; :: 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 VECTSP_4:25; :: thesis:

end;

A4: 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]

proof

let Y be set ; :: thesis:
assume that
A5: Y c= X and
A6: 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 A7: 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 A7; :: thesis:

end;

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

defpred S₄[ object , object ] means ex W1 being strict Subspace of V st
( $1 = W1 & $2 = the carrier of W1 );
A9: 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
A10: x = W1 and
W /\ W1 = (0). V by A1, A5;
reconsider y = the carrier of W1 as set ;
take y ; :: thesis:
take W1 ; :: thesis:
thus ( x = W1 & y = the carrier of W1 ) by A10; :: thesis:

end;

consider f being Function such that
A11: dom f = Y and
A12: for x being object st x in Y holds
S₄[x,f . x] from CLASSES1:sch 1(A9);
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
A13: x in Y9 and
A14: Y9 in rng f by TARSKI:def 4;
consider y being object such that
A15: y in dom f and
A16: f . y = Y9 by A14, FUNCT_1:def 3;
consider W1 being strict Subspace of V such that
y = W1 and
A17: f . y = the carrier of W1 by A11, A12, A15;
the carrier of W1 c= the carrier of V by VECTSP_4:def 2;
hence x in the carrier of V by A13, A16, A17; :: thesis:

end;

then reconsider Z = union (rng f) as Subset of V by TARSKI:def 3;
A18: Z is linearly-closed

proof

thus for v1, v2 being Element of V st v1 in Z & v2 in Z holds
v1 + v2 in Z :: according to VECTSP_4:def 1 :: thesis:

proof

let v1, v2 be Element of V; :: thesis:
assume that
A19: v1 in Z and
A20: v2 in Z ; :: thesis:
consider Y1 being set such that
A21: v1 in Y1 and
A22: Y1 in rng f by A19, TARSKI:def 4;
consider y1 being object such that
A23: y1 in dom f and
A24: f . y1 = Y1 by A22, FUNCT_1:def 3;
consider Y2 being set such that
A25: v2 in Y2 and
A26: Y2 in rng f by A20, TARSKI:def 4;
consider y2 being object such that
A27: y2 in dom f and
A28: f . y2 = Y2 by A26, FUNCT_1:def 3;
consider W1 being strict Subspace of V such that
A29: y1 = W1 and
A30: f . y1 = the carrier of W1 by A11, A12, A23;
consider W2 being strict Subspace of V such that
A31: y2 = W2 and
A32: f . y2 = the carrier of W2 by A11, A12, A27;
reconsider y1 = y1, y2 = y2 as Element of X by A5, A11, A23, A27;

now :: thesis:

per cases in R or [y2,y1] in R ) by A6, A11, A23, A27;

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 A29, A31, VECTSP_4:def 2;
then A33: v1 in W2 by A21, A24, A30, STRUCT_0:def 5;
v2 in W2 by A25, A28, A32, STRUCT_0:def 5;
then v1 + v2 in W2 by A33, VECTSP_4:20;
then A34: v1 + v2 in the carrier of W2 by STRUCT_0:def 5;
f . y2 in rng f by A27, FUNCT_1:def 3;
hence v1 + v2 in Z by A32, A34, 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 A29, A31, VECTSP_4:def 2;
then A35: v2 in W1 by A25, A28, A32, STRUCT_0:def 5;
v1 in W1 by A21, A24, A30, STRUCT_0:def 5;
then v1 + v2 in W1 by A35, VECTSP_4:20;
then A36: v1 + v2 in the carrier of W1 by STRUCT_0:def 5;
f . y1 in rng f by A23, FUNCT_1:def 3;
hence v1 + v2 in Z by A30, A36, TARSKI:def 4; :: thesis:

end;

hence v1 + v2 in Z ; :: thesis:

end;

let a be Element of F; :: thesis:
let v1 be Element of V; :: thesis:
assume v1 in Z ; :: thesis:
then consider Y1 being set such that
A37: v1 in Y1 and
A38: Y1 in rng f by TARSKI:def 4;
consider y1 being object such that
A39: y1 in dom f and
A40: f . y1 = Y1 by A38, FUNCT_1:def 3;
consider W1 being strict Subspace of V such that
y1 = W1 and
A41: f . y1 = the carrier of W1 by A11, A12, A39;
v1 in W1 by A37, A40, A41, STRUCT_0:def 5;
then a * v1 in W1 by VECTSP_4:21;
then A42: a * v1 in the carrier of W1 by STRUCT_0:def 5;
f . y1 in rng f by A39, FUNCT_1:def 3;
hence a * v1 in Z by A41, A42, TARSKI:def 4; :: thesis:

end;

set z = the Element of rng f;
A43: rng f <> {} by A8, A11, RELAT_1:42;
then consider z1 being object such that
A44: z1 in dom f and
A45: 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 A11, A12, A44;
then Z <> {} by A43, A45, ORDERS_1:6;
then consider E being strict Subspace of V such that
A46: Z = the carrier of E by A18, VECTSP_4:34;

now :: thesis:

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

proof

assume A47: u in W /\ E ; :: thesis:
then A48: u in W by Th3;
u in E by A47, Th3;
then u in Z by A46, STRUCT_0:def 5;
then consider Y1 being set such that
A49: u in Y1 and
A50: Y1 in rng f by TARSKI:def 4;
consider y1 being object such that
A51: y1 in dom f and
A52: f . y1 = Y1 by A50, FUNCT_1:def 3;
A53: ex W2 being strict Subspace of V st
( y1 = W2 & W /\ W2 = (0). V ) by A1, A5, A11, A51;
consider W1 being strict Subspace of V such that
A54: y1 = W1 and
A55: f . y1 = the carrier of W1 by A11, A12, A51;
u in W1 by A49, A52, A55, STRUCT_0:def 5;
hence u in (0). V by A54, A48, A53, 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 VECTSP_4:def 3;
then u = 0. V by TARSKI:def 1;
hence u in W /\ E by VECTSP_4:17; :: thesis:

end;

then A56: W /\ E = (0). V by VECTSP_4:30;
E in Subspaces V by Def3;
then reconsider y9 = E as Element of X by A1, A56;
take y = y9; :: thesis:
let x be Element of X; :: thesis:
assume A57: x in Y ; :: thesis:
then consider W1 being strict Subspace of V such that
A58: x = W1 and
A59: f . x = the carrier of W1 by A12;

now :: thesis:

let u be Element of V; :: thesis:
assume u in W1 ; :: thesis:
then A60: u in the carrier of W1 by STRUCT_0:def 5;
the carrier of W1 in rng f by A11, A57, A59, FUNCT_1:def 3;
then u in Z by A60, TARSKI:def 4;
hence u in E by A46, STRUCT_0:def 5; :: thesis:

end;

then W1 is Subspace of E by VECTSP_4:28;
hence [x,y] in R by A2, A58; :: thesis:

end;

hence ex y being Element of X st
for x being Element of X st x in Y holds
S₃[x,y] ; :: thesis:

end;

A61: now :: thesis:

let x, y, z be Element of X; :: thesis:
assume that
A62: S₃[x,y] and
A63: S₃[y,z] ; :: thesis:
consider W1, W2 being strict Subspace of V such that
A64: x = W1 and
A65: ( y = W2 & W1 is Subspace of W2 ) by A2, A62;
consider W3, W4 being strict Subspace of V such that
A66: y = W3 and
A67: z = W4 and
A68: W3 is Subspace of W4 by A2, A63;
W1 is Subspace of W4 by A65, A66, A68, VECTSP_4:26;
hence S₃[x,z] by A2, A64, A67; :: thesis:

end;

A69: now :: thesis:

let x be Element of X; :: thesis:
consider W1 being strict Subspace of V such that
A70: x = W1 and
W /\ W1 = (0). V by A1;
W1 is Subspace of W1 by VECTSP_4:24;
hence S₃[x,x] by A2, A70; :: thesis:

end;

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(A69, A3, A61, A4);
consider L being strict Subspace of V such that
A72: x = L and
A73: W /\ L = (0). V by A1;
take L ; :: thesis:
thus ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = L + W :: according to VECTSP_5:def 4 :: thesis:

proof

assume not ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = L + W ; :: thesis:
then consider v being Element of V such that
A74: for v1, v2 being Element of V holds
( not v1 in L or not v2 in W or v <> v1 + v2 ) by Lm16;
( v = (0. V) + v & 0. V in W ) by RLVECT_1:4, VECTSP_4:17;
then A75: not v in L by A74;
set A = { (a * v) where a is Element of F : verum } ;
A76: (1_ F) * v in { (a * v) where a is Element of F : verum } ;

now :: thesis:

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

end;

then reconsider A = { (a * v) where a is Element of F : verum } as Subset of V by TARSKI:def 3;
A is linearly-closed

proof

thus for v1, v2 being Element of V st v1 in A & v2 in A holds
v1 + v2 in A :: according to VECTSP_4:def 1 :: thesis:

proof

let v1, v2 be Element of V; :: thesis:
assume v1 in A ; :: thesis:
then consider a1 being Element of F such that
A77: v1 = a1 * v ;
assume v2 in A ; :: thesis:
then consider a2 being Element of F such that
A78: v2 = a2 * v ;
v1 + v2 = (a1 + a2) * v by A77, A78, VECTSP_1:def 15;
hence v1 + v2 in A ; :: thesis:

end;

let a be Element of F; :: thesis:
let v1 be Element of V; :: thesis:
assume v1 in A ; :: thesis:
then consider a1 being Element of F such that
A79: v1 = a1 * v ;
a * v1 = (a * a1) * v by A79, VECTSP_1:def 16;
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, VECTSP_4:34;
A81: not v in L + W by A74, Th1;

now :: thesis:

let u be Element 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 Element of F such that
A83: u = a * v ;

now :: thesis:

u in W + L by A82, Th3;
then (a ") * (a * v) in W + L by A83, VECTSP_4:21;
then A84: ((a ") * a) * v in W + L by VECTSP_1:def 16;
assume a <> 0. F ; :: thesis:
then (1_ F) * v in W + L by A84, VECTSP_1:def 10;
then (1_ F) * v in L + W by Lm1;
hence contradiction by A81, VECTSP_1:def 17; :: thesis:

end;

then u = 0. V by A83, VECTSP_1:14;
hence u in (0). V by VECTSP_4: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 VECTSP_4:def 3;
then u = 0. V by TARSKI:def 1;
hence u in Z /\ (W + L) by VECTSP_4:17; :: thesis:

end;

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

now :: thesis:

let u be Element 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 Element 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, Th2, VECTSP_2:2;
then v1 in W + L by A91, VECTSP_4: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 VECTSP_4:def 3;
then v1 = 0. V by TARSKI:def 1;
then v2 = u by A89, RLVECT_1:4;
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 VECTSP_4:def 3;
then u = 0. V by TARSKI:def 1;
hence u in (Z + L) /\ W by VECTSP_4:17; :: thesis:

end;

then A92: W /\ (Z + L) = (0). V by VECTSP_4:30;
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, VECTSP_1:def 17;
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; :: thesis: