:: VECTSP_8 semantic presentation

begin


definition
let F be Field;
let VS be strict VectSp of F;
func lattice VS ->  strict bounded Lattice equals :: VECTSP_8:def 1
 LattStr(# (Subspaces VS),(SubJoin VS),(SubMeet VS) #);
coherence
 LattStr(# (Subspaces VS),(SubJoin VS),(SubMeet VS) #) is strict bounded Lattice by VECTSP_5:60;
end;

:: deftheorem  defines lattice VECTSP_8:def_1_:_
 for F being Field
for VS being strict VectSp of F holds lattice VS = LattStr(# (Subspaces VS),(SubJoin VS),(SubMeet VS) #);

definition
let F be Field;
let VS be strict VectSp of F;
mode SubVS-Family of VS ->  set  means :Def2: :: VECTSP_8:def 2
 for x being set st x in it holds
x is Subspace of VS;
existence
 ex b1 being set st
for x being set st x in b1 holds
x is Subspace of VS
proof
take  {} ; ::_thesis: for x being set st x in {} holds
x is Subspace of VS
thus  for x being set st x in {} holds
x is Subspace of VS ; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines SubVS-Family VECTSP_8:def_2_:_
 for F being Field
for VS being strict VectSp of F
for b3 being set holds
( b3 is SubVS-Family of VS iff for x being set st x in b3 holds
x is Subspace of VS );

registration
let F be Field;
let VS be strict VectSp of F;
cluster non empty for SubVS-Family of VS;
existence
 not for b1 being SubVS-Family of VS holds b1 is empty
proof
set A = the Subspace of VS;
 for X being set st X in { the Subspace of VS} holds
X is Subspace of VS by TARSKI:def_1;
then reconsider B = { the Subspace of VS} as SubVS-Family of VS by Def2;
take  B ; ::_thesis: not B is empty
thus  not B is empty ; ::_thesis: verum
end;
end;

definition
let F be Field;
let VS be strict VectSp of F;
:: original: Subspaces
redefine func Subspaces VS ->  non empty SubVS-Family of VS;
coherence
 Subspaces VS is non empty SubVS-Family of VS
proof
 Subspaces VS is SubVS-Family of VS
proof
let x be set ; :: according to VECTSP_8:def_2 ::_thesis: ( x in Subspaces VS implies x is Subspace of VS )
assume  x in Subspaces VS ; ::_thesis: x is Subspace of VS
then  ex W being strict Subspace of VS st x = W by VECTSP_5:def_3;
hence  x is Subspace of VS ; ::_thesis: verum
end;
hence  Subspaces VS is non empty SubVS-Family of VS ; ::_thesis: verum
end;
let X be non empty SubVS-Family of VS;
:: original: Element
redefine mode Element of X ->  Subspace of VS;
coherence
 for b1 being Element of X holds b1 is Subspace of VS by Def2;
end;

definition
let F be Field;
let VS be strict VectSp of F;
let x be Element of Subspaces VS;
func carr x ->  Subset of VS means :Def3: :: VECTSP_8:def 3
 ex X being Subspace of VS st
( x = X & it = the carrier of X );
existence
 ex b1 being Subset of VS ex X being Subspace of VS st
( x = X & b1 = the carrier of X )
proof
reconsider A = the carrier of x as Subset of VS by VECTSP_4:def_2;
consider X being Subspace of VS such that
A1: X = x ;
take  A ; ::_thesis: ex X being Subspace of VS st
( x = X & A = the carrier of X )
take  X ; ::_thesis: ( x = X & A = the carrier of X )
thus  ( x = X & A = the carrier of X ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of VS st ex X being Subspace of VS st
( x = X & b1 = the carrier of X ) & ex X being Subspace of VS st
( x = X & b2 = the carrier of X ) holds
b1 = b2 ;
end;

:: deftheorem Def3 defines carr VECTSP_8:def_3_:_
 for F being Field
for VS being strict VectSp of F
for x being Element of Subspaces VS
for b4 being Subset of VS holds
( b4 = carr x iff ex X being Subspace of VS st
( x = X & b4 = the carrier of X ) );


definition
let F be Field;
let VS be strict VectSp of F;
func carr VS ->  Function of (Subspaces VS),(bool the carrier of VS) means :Def4: :: VECTSP_8:def 4
 for h being Element of Subspaces VS
for H being Subspace of VS st h = H holds
it . h = the carrier of H;
existence
 ex b1 being Function of (Subspaces VS),(bool the carrier of VS) st
for h being Element of Subspaces VS
for H being Subspace of VS st h = H holds
b1 . h = the carrier of H
proof
defpred S1[ set , set ] means  for h being Element of Subspaces VS st h = $1 holds
$2 = the carrier of h;
A1: for e being set st e in Subspaces VS holds
ex u being set st
( u in bool the carrier of VS & S1[e,u] )
proof
let e be set ; ::_thesis: ( e in Subspaces VS implies ex u being set st
( u in bool the carrier of VS & S1[e,u] ) )
assume A2: e in Subspaces VS ; ::_thesis: ex u being set st
( u in bool the carrier of VS & S1[e,u] )
then consider E being strict Subspace of VS such that
A3: E = e by VECTSP_5:def_3;
reconsider u = E as Element of Subspaces VS by A2, A3;
reconsider u1 = carr u as Subset of VS ;
take  u1 ; ::_thesis: ( u1 in bool the carrier of VS & S1[e,u1] )
 ex X being Subspace of VS st
( u = X & u1 = the carrier of X ) by Def3;
hence  ( u1 in bool the carrier of VS & S1[e,u1] ) by A3; ::_thesis: verum
end;
consider f being Function of (Subspaces VS),(bool the carrier of VS) such that
A4: for e being set st e in Subspaces VS holds
S1[e,f . e] from FUNCT_2:sch_1(A1);
take  f ; ::_thesis: for h being Element of Subspaces VS
for H being Subspace of VS st h = H holds
f . h = the carrier of H
thus  for h being Element of Subspaces VS
for H being Subspace of VS st h = H holds
f . h = the carrier of H by A4; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (Subspaces VS),(bool the carrier of VS) st ( for h being Element of Subspaces VS
for H being Subspace of VS st h = H holds
b1 . h = the carrier of H ) & ( for h being Element of Subspaces VS
for H being Subspace of VS st h = H holds
b2 . h = the carrier of H ) holds
b1 = b2
proof
let F1, F2 be Function of (Subspaces VS),(bool the carrier of VS); ::_thesis: ( ( for h being Element of Subspaces VS
for H being Subspace of VS st h = H holds
F1 . h = the carrier of H ) & ( for h being Element of Subspaces VS
for H being Subspace of VS st h = H holds
F2 . h = the carrier of H ) implies F1 = F2 )
assume that
A5: for h1 being Element of Subspaces VS
for H1 being Subspace of VS st h1 = H1 holds
F1 . h1 = the carrier of H1 and
A6: for h2 being Element of Subspaces VS
for H2 being Subspace of VS st h2 = H2 holds
F2 . h2 = the carrier of H2 ; ::_thesis: F1 = F2
 for h being set st h in Subspaces VS holds
F1 . h = F2 . h
proof
let h be set ; ::_thesis: ( h in Subspaces VS implies F1 . h = F2 . h )
assume A7: h in Subspaces VS ; ::_thesis: F1 . h = F2 . h
then  h is Element of Subspaces VS ;
then consider H being Subspace of VS such that
A8: H = h ;
 F1 . h = the carrier of H by A5, A7, A8;
hence  F1 . h = F2 . h by A6, A7, A8; ::_thesis: verum
end;
hence  F1 = F2 by FUNCT_2:12; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines carr VECTSP_8:def_4_:_
 for F being Field
for VS being strict VectSp of F
for b3 being Function of (Subspaces VS),(bool the carrier of VS) holds
( b3 = carr VS iff for h being Element of Subspaces VS
for H being Subspace of VS st h = H holds
b3 . h = the carrier of H );

theorem Th1: :: VECTSP_8:1
for F being Field
for VS being strict VectSp of F
for H being non empty Subset of (Subspaces VS) holds not (carr VS) .: H is empty
proof
let F be Field; ::_thesis: for VS being strict VectSp of F
for H being non empty Subset of (Subspaces VS) holds not (carr VS) .: H is empty
let VS be strict VectSp of F; ::_thesis: for H being non empty Subset of (Subspaces VS) holds not (carr VS) .: H is empty
let H be non empty Subset of (Subspaces VS); ::_thesis: not (carr VS) .: H is empty
consider x being Element of Subspaces VS such that
A1: x in H by SUBSET_1:4;
 (carr VS) . x in (carr VS) .: H by A1, FUNCT_2:35;
hence  not (carr VS) .: H is empty ; ::_thesis: verum
end;

theorem :: VECTSP_8:2
for F being Field
for VS being strict VectSp of F
for H being strict Subspace of VS holds 0. VS in (carr VS) . H
proof
let F be Field; ::_thesis: for VS being strict VectSp of F
for H being strict Subspace of VS holds 0. VS in (carr VS) . H
let VS be strict VectSp of F; ::_thesis: for H being strict Subspace of VS holds 0. VS in (carr VS) . H
let H be strict Subspace of VS; ::_thesis: 0. VS in (carr VS) . H
 H in Subspaces VS by VECTSP_5:def_3;
then A1: (carr VS) . H = the carrier of H by Def4;
 0. H = 0. VS by VECTSP_4:11;
hence  0. VS in (carr VS) . H by A1; ::_thesis: verum
end;

definition
let F be Field;
let VS be strict VectSp of F;
let G be non empty Subset of (Subspaces VS);
func meet G ->  strict Subspace of VS means :Def5: :: VECTSP_8:def 5
 the carrier of it = meet ((carr VS) .: G);
existence
 ex b1 being strict Subspace of VS st the carrier of b1 = meet ((carr VS) .: G)
proof
reconsider cG = (carr VS) .: G as Subset-Family of VS ;
set C0 = meet cG;
A1: for X being set st X in (carr VS) .: G holds
0. VS in X
proof
let X be set ; ::_thesis: ( X in (carr VS) .: G implies 0. VS in X )
assume A2: X in (carr VS) .: G ; ::_thesis: 0. VS in X
then reconsider X = X as Subset of VS ;
consider X1 being Element of Subspaces VS such that
 X1 in G and
A3: X = (carr VS) . X1 by A2, FUNCT_2:65;
A4: 0. VS in X1 by VECTSP_4:17;
 X = the carrier of X1 by A3, Def4;
hence  0. VS in X by A4, STRUCT_0:def_5; ::_thesis: verum
end;
 (carr VS) .: G <> {} by Th1;
then A5: meet cG <> {} by A1, SETFAM_1:def_1;
reconsider C0 = meet cG as Subset of VS ;
A6: for v, u being Element of VS st v in C0 & u in C0 holds
v + u in C0
proof
let v, u be Element of VS; ::_thesis: ( v in C0 & u in C0 implies v + u in C0 )
assume that
A7: v in C0 and
A8: u in C0 ; ::_thesis: v + u in C0
A9: for X being set st X in (carr VS) .: G holds
v + u in X
proof
reconsider v1 = v, u1 = u as Element of VS ;
let X be set ; ::_thesis: ( X in (carr VS) .: G implies v + u in X )
reconsider vu = v1 + u1 as Element of VS ;
assume A10: X in (carr VS) .: G ; ::_thesis: v + u in X
then A11: v in X by A7, SETFAM_1:def_1;
A12: u in X by A8, A10, SETFAM_1:def_1;
reconsider X = X as Subset of VS by A10;
consider X1 being Element of Subspaces VS such that
 X1 in G and
A13: X = (carr VS) . X1 by A10, FUNCT_2:65;
A14: X = the carrier of X1 by A13, Def4;
then A15: u1 in X1 by A12, STRUCT_0:def_5;
consider X2 being strict Subspace of VS such that
A16: X2 = X1 by VECTSP_5:def_3;
 v1 in X1 by A11, A14, STRUCT_0:def_5;
then  vu in X1 + X1 by A15, VECTSP_5:1;
then  vu in X2 by A16, VECTSP_5:4;
hence  v + u in X by A14, A16, STRUCT_0:def_5; ::_thesis: verum
end;
 (carr VS) .: G <> {} by Th1;
hence  v + u in C0 by A9, SETFAM_1:def_1; ::_thesis: verum
end;
 for a being Element of F
for v being Element of VS st v in C0 holds
a * v in C0
proof
let a be Element of F; ::_thesis: for v being Element of VS st v in C0 holds
a * v in C0
let v be Element of VS; ::_thesis: ( v in C0 implies a * v in C0 )
assume A17: v in C0 ; ::_thesis: a * v in C0
A18: for X being set st X in (carr VS) .: G holds
a * v in X
proof
reconsider v1 = v as Element of VS ;
let X be set ; ::_thesis: ( X in (carr VS) .: G implies a * v in X )
assume A19: X in (carr VS) .: G ; ::_thesis: a * v in X
then A20: v in X by A17, SETFAM_1:def_1;
reconsider X = X as Subset of VS by A19;
consider X1 being Element of Subspaces VS such that
 X1 in G and
A21: X = (carr VS) . X1 by A19, FUNCT_2:65;
A22: X = the carrier of X1 by A21, Def4;
then  v1 in X1 by A20, STRUCT_0:def_5;
then  a * v1 in X1 by VECTSP_4:21;
hence  a * v in X by A22, STRUCT_0:def_5; ::_thesis: verum
end;
 (carr VS) .: G <> {} by Th1;
hence  a * v in C0 by A18, SETFAM_1:def_1; ::_thesis: verum
end;
then  C0 is linearly-closed by A6, VECTSP_4:def_1;
hence  ex b1 being strict Subspace of VS st the carrier of b1 = meet ((carr VS) .: G) by A5, VECTSP_4:34; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict Subspace of VS st the carrier of b1 = meet ((carr VS) .: G) & the carrier of b2 = meet ((carr VS) .: G) holds
b1 = b2 by VECTSP_4:29;
end;

:: deftheorem Def5 defines meet VECTSP_8:def_5_:_
 for F being Field
for VS being strict VectSp of F
for G being non empty Subset of (Subspaces VS)
for b4 being strict Subspace of VS holds
( b4 = meet G iff the carrier of b4 = meet ((carr VS) .: G) );

theorem :: VECTSP_8:3
for F being Field
for VS being strict VectSp of F holds Subspaces VS = the carrier of (lattice VS) ;

theorem :: VECTSP_8:4
for F being Field
for VS being strict VectSp of F holds the L_meet of (lattice VS) = SubMeet VS ;

theorem :: VECTSP_8:5
for F being Field
for VS being strict VectSp of F holds the L_join of (lattice VS) = SubJoin VS ;

theorem Th6: :: VECTSP_8:6
for F being Field
for VS being strict VectSp of F
for p, q being Element of (lattice VS)
for H1, H2 being strict Subspace of VS st p = H1 & q = H2 holds
( p [= q iff the carrier of H1 c= the carrier of H2 )
proof
let F be Field; ::_thesis: for VS being strict VectSp of F
for p, q being Element of (lattice VS)
for H1, H2 being strict Subspace of VS st p = H1 & q = H2 holds
( p [= q iff the carrier of H1 c= the carrier of H2 )
let VS be strict VectSp of F; ::_thesis: for p, q being Element of (lattice VS)
for H1, H2 being strict Subspace of VS st p = H1 & q = H2 holds
( p [= q iff the carrier of H1 c= the carrier of H2 )
let p, q be Element of (lattice VS); ::_thesis: for H1, H2 being strict Subspace of VS st p = H1 & q = H2 holds
( p [= q iff the carrier of H1 c= the carrier of H2 )
let H1, H2 be strict Subspace of VS; ::_thesis: ( p = H1 & q = H2 implies ( p [= q iff the carrier of H1 c= the carrier of H2 ) )
consider A1 being strict Subspace of VS such that
A1: A1 = p by VECTSP_5:def_3;
consider A2 being strict Subspace of VS such that
A2: A2 = q by VECTSP_5:def_3;
A3: ( the carrier of A1 c= the carrier of A2 implies p [= q )
proof
assume  the carrier of A1 c= the carrier of A2 ; ::_thesis: p [= q
then  the carrier of A1 /\ the carrier of A2 = the carrier of A1 by XBOOLE_1:28;
then A4: A1 /\ A2 = A1 by VECTSP_5:def_2;
A1 /\ A2 = the L_meet of (lattice VS) . (p,q) by A1, A2, VECTSP_5:def_8
.= p "/\" q by LATTICES:def_2 ;
hence  p [= q by A1, A4, LATTICES:4; ::_thesis: verum
end;
 ( p [= q implies the carrier of A1 c= the carrier of A2 )
proof
assume  p [= q ; ::_thesis: the carrier of A1 c= the carrier of A2
then A5: p "/\" q = p by LATTICES:4;
p "/\" q = (SubMeet VS) . (p,q) by LATTICES:def_2
.= A1 /\ A2 by A1, A2, VECTSP_5:def_8 ;
then  the carrier of A1 /\ the carrier of A2 = the carrier of A1 by A1, A5, VECTSP_5:def_2;
hence  the carrier of A1 c= the carrier of A2 by XBOOLE_1:17; ::_thesis: verum
end;
hence  ( p = H1 & q = H2 implies ( p [= q iff the carrier of H1 c= the carrier of H2 ) ) by A1, A2, A3; ::_thesis: verum
end;

theorem Th7: :: VECTSP_8:7
for F being Field
for VS being strict VectSp of F
for p, q being Element of (lattice VS)
for H1, H2 being Subspace of VS st p = H1 & q = H2 holds
p "\/" q = H1 + H2
proof
let F be Field; ::_thesis: for VS being strict VectSp of F
for p, q being Element of (lattice VS)
for H1, H2 being Subspace of VS st p = H1 & q = H2 holds
p "\/" q = H1 + H2
let VS be strict VectSp of F; ::_thesis: for p, q being Element of (lattice VS)
for H1, H2 being Subspace of VS st p = H1 & q = H2 holds
p "\/" q = H1 + H2
let p, q be Element of (lattice VS); ::_thesis: for H1, H2 being Subspace of VS st p = H1 & q = H2 holds
p "\/" q = H1 + H2
let H1, H2 be Subspace of VS; ::_thesis: ( p = H1 & q = H2 implies p "\/" q = H1 + H2 )
consider H1 being strict Subspace of VS such that
A1: H1 = p by VECTSP_5:def_3;
consider H2 being strict Subspace of VS such that
A2: H2 = q by VECTSP_5:def_3;
p "\/" q = (SubJoin VS) . (p,q) by LATTICES:def_1
.= H1 + H2 by A1, A2, VECTSP_5:def_7 ;
hence  ( p = H1 & q = H2 implies p "\/" q = H1 + H2 ) by A1, A2; ::_thesis: verum
end;

theorem Th8: :: VECTSP_8:8
for F being Field
for VS being strict VectSp of F
for p, q being Element of (lattice VS)
for H1, H2 being Subspace of VS st p = H1 & q = H2 holds
p "/\" q = H1 /\ H2
proof
let F be Field; ::_thesis: for VS being strict VectSp of F
for p, q being Element of (lattice VS)
for H1, H2 being Subspace of VS st p = H1 & q = H2 holds
p "/\" q = H1 /\ H2
let VS be strict VectSp of F; ::_thesis: for p, q being Element of (lattice VS)
for H1, H2 being Subspace of VS st p = H1 & q = H2 holds
p "/\" q = H1 /\ H2
let p, q be Element of (lattice VS); ::_thesis: for H1, H2 being Subspace of VS st p = H1 & q = H2 holds
p "/\" q = H1 /\ H2
let H1, H2 be Subspace of VS; ::_thesis: ( p = H1 & q = H2 implies p "/\" q = H1 /\ H2 )
consider H1 being strict Subspace of VS such that
A1: H1 = p by VECTSP_5:def_3;
consider H2 being strict Subspace of VS such that
A2: H2 = q by VECTSP_5:def_3;
p "/\" q = (SubMeet VS) . (p,q) by LATTICES:def_2
.= H1 /\ H2 by A1, A2, VECTSP_5:def_8 ;
hence  ( p = H1 & q = H2 implies p "/\" q = H1 /\ H2 ) by A1, A2; ::_thesis: verum
end;

definition
let L be non empty LattStr ;
redefine attr L is complete  means :: VECTSP_8:def 6
 for X being Subset of L ex a being Element of L st
( a is_less_than X & ( for b being Element of L st b is_less_than X holds
b [= a ) );
compatibility
 ( L is complete iff for X being Subset of L ex a being Element of L st
( a is_less_than X & ( for b being Element of L st b is_less_than X holds
b [= a ) ) )
proof
hereby  ::_thesis: ( ( for X being Subset of L ex a being Element of L st
( a is_less_than X & ( for b being Element of L st b is_less_than X holds
b [= a ) ) ) implies L is complete )
assume A1: L is complete ; ::_thesis: for X being Subset of L ex p being Element of L st
( p is_less_than X & ( for b being Element of L st b is_less_than X holds
b [= p ) )
let X be Subset of L; ::_thesis: ex p being Element of L st
( p is_less_than X & ( for b being Element of L st b is_less_than X holds
b [= p ) )
set Y =  {  c where c is Element of L : c is_less_than X  }  ;
consider p being Element of L such that
A2:  {  c where c is Element of L : c is_less_than X  }  is_less_than p and
A3: for r being Element of L st  {  c where c is Element of L : c is_less_than X  }  is_less_than r holds
p [= r by A1, LATTICE3:def_18;
take p = p; ::_thesis: ( p is_less_than X & ( for b being Element of L st b is_less_than X holds
b [= p ) )
thus  p is_less_than X ::_thesis: for b being Element of L st b is_less_than X holds
b [= p
proof
let q be Element of L; :: according to LATTICE3:def_16 ::_thesis: ( not q in X or p [= q )
assume A4: q in X ; ::_thesis: p [= q
  {  c where c is Element of L : c is_less_than X  }  is_less_than q
proof
let s be Element of L; :: according to LATTICE3:def_17 ::_thesis: ( not s in  {  c where c is Element of L : c is_less_than X  }  or s [= q )
assume  s in  {  c where c is Element of L : c is_less_than X  }  ; ::_thesis: s [= q
then  ex t being Element of L st
( s = t & t is_less_than X ) ;
hence  s [= q by A4, LATTICE3:def_16; ::_thesis: verum
end;
hence  p [= q by A3; ::_thesis: verum
end;
let b be Element of L; ::_thesis: ( b is_less_than X implies b [= p )
assume  b is_less_than X ; ::_thesis: b [= p
then  b in  {  c where c is Element of L : c is_less_than X  }  ;
hence  b [= p by A2, LATTICE3:def_17; ::_thesis: verum
end;
assume A5: for X being Subset of L ex a being Element of L st
( a is_less_than X & ( for b being Element of L st b is_less_than X holds
b [= a ) ) ; ::_thesis: L is complete
let X be set ; :: according to LATTICE3:def_18 ::_thesis: ex b1 being Element of the carrier of L st
( X is_less_than b1 & ( for b2 being Element of the carrier of L holds
( not X is_less_than b2 or b1 [= b2 ) ) )
defpred S1[ Element of L] means X is_less_than $1;
set Y =  {  c where c is Element of L : S1[c]  }  ;
  {  c where c is Element of L : S1[c]  }  is Subset of L from DOMAIN_1:sch_7();
then consider p being Element of L such that
A6: p is_less_than  {  c where c is Element of L : S1[c]  }  and
A7: for r being Element of L st r is_less_than  {  c where c is Element of L : S1[c]  }  holds
r [= p by A5;
take  p ; ::_thesis: ( X is_less_than p & ( for b1 being Element of the carrier of L holds
( not X is_less_than b1 or p [= b1 ) ) )
thus  X is_less_than p ::_thesis: for b1 being Element of the carrier of L holds
( not X is_less_than b1 or p [= b1 )
proof
let q be Element of L; :: according to LATTICE3:def_17 ::_thesis: ( not q in X or q [= p )
assume A8: q in X ; ::_thesis: q [= p
 q is_less_than  {  c where c is Element of L : S1[c]  }
proof
let s be Element of L; :: according to LATTICE3:def_16 ::_thesis: ( not s in  {  c where c is Element of L : S1[c]  }  or q [= s )
assume  s in  {  c where c is Element of L : S1[c]  }  ; ::_thesis: q [= s
then  ex t being Element of L st
( s = t & X is_less_than t ) ;
hence  q [= s by A8, LATTICE3:def_17; ::_thesis: verum
end;
hence  q [= p by A7; ::_thesis: verum
end;
let r be Element of L; ::_thesis: ( not X is_less_than r or p [= r )
assume  X is_less_than r ; ::_thesis: p [= r
then  r in  {  c where c is Element of L : S1[c]  }  ;
hence  p [= r by A6, LATTICE3:def_16; ::_thesis: verum
end;
end;

:: deftheorem  defines complete VECTSP_8:def_6_:_
 for L being non empty LattStr holds
( L is complete iff for X being Subset of L ex a being Element of L st
( a is_less_than X & ( for b being Element of L st b is_less_than X holds
b [= a ) ) );

theorem :: VECTSP_8:9
for F being Field
for VS being strict VectSp of F holds lattice VS is complete
proof
let F be Field; ::_thesis: for VS being strict VectSp of F holds lattice VS is complete
let VS be strict VectSp of F; ::_thesis: lattice VS is complete
let Y be Subset of (lattice VS); :: according to VECTSP_8:def_6 ::_thesis: ex a being Element of (lattice VS) st
( a is_less_than Y & ( for b being Element of (lattice VS) st b is_less_than Y holds
b [= a ) )
percases ( Y = {} or Y <> {} ) ;
supposeA1: Y = {} ; ::_thesis: ex a being Element of (lattice VS) st
( a is_less_than Y & ( for b being Element of (lattice VS) st b is_less_than Y holds
b [= a ) )
thus  ex a being Element of (lattice VS) st
( a is_less_than Y & ( for b being Element of (lattice VS) st b is_less_than Y holds
b [= a ) ) ::_thesis: verum
proof
take  Top (lattice VS) ; ::_thesis: ( Top (lattice VS) is_less_than Y & ( for b being Element of (lattice VS) st b is_less_than Y holds
b [= Top (lattice VS) ) )
thus  Top (lattice VS) is_less_than Y ::_thesis: for b being Element of (lattice VS) st b is_less_than Y holds
b [= Top (lattice VS)
proof
let q be Element of (lattice VS); :: according to LATTICE3:def_16 ::_thesis: ( not q in Y or Top (lattice VS) [= q )
thus  ( not q in Y or Top (lattice VS) [= q ) by A1; ::_thesis: verum
end;
let b be Element of (lattice VS); ::_thesis: ( b is_less_than Y implies b [= Top (lattice VS) )
assume  b is_less_than Y ; ::_thesis: b [= Top (lattice VS)
thus  b [= Top (lattice VS) by LATTICES:19; ::_thesis: verum
end;
end;
suppose Y <> {} ; ::_thesis: ex a being Element of (lattice VS) st
( a is_less_than Y & ( for b being Element of (lattice VS) st b is_less_than Y holds
b [= a ) )
then reconsider X = Y as non empty Subset of (Subspaces VS) ;
reconsider p = meet X as Element of (lattice VS) by VECTSP_5:def_3;
take  p ; ::_thesis: ( p is_less_than Y & ( for b being Element of (lattice VS) st b is_less_than Y holds
b [= p ) )
set x = the Element of X;
thus  p is_less_than Y ::_thesis: for b being Element of (lattice VS) st b is_less_than Y holds
b [= p
proof
let q be Element of (lattice VS); :: according to LATTICE3:def_16 ::_thesis: ( not q in Y or p [= q )
consider H being strict Subspace of VS such that
A2: H = q by VECTSP_5:def_3;
reconsider h = q as Element of Subspaces VS ;
assume A3: q in Y ; ::_thesis: p [= q
 (carr VS) . h = the carrier of H by A2, Def4;
then  meet ((carr VS) .: X) c= the carrier of H by A3, FUNCT_2:35, SETFAM_1:3;
then  the carrier of (meet X) c= the carrier of H by Def5;
hence  p [= q by A2, Th6; ::_thesis: verum
end;
let r be Element of (lattice VS); ::_thesis: ( r is_less_than Y implies r [= p )
consider H being strict Subspace of VS such that
A4: H = r by VECTSP_5:def_3;
assume A5: r is_less_than Y ; ::_thesis: r [= p
A6: for Z1 being set st Z1 in (carr VS) .: X holds
the carrier of H c= Z1
proof
let Z1 be set ; ::_thesis: ( Z1 in (carr VS) .: X implies the carrier of H c= Z1 )
assume A7: Z1 in (carr VS) .: X ; ::_thesis: the carrier of H c= Z1
then reconsider Z2 = Z1 as Subset of VS ;
consider z1 being Element of Subspaces VS such that
A8: z1 in X and
A9: Z2 = (carr VS) . z1 by A7, FUNCT_2:65;
reconsider z1 = z1 as Element of (lattice VS) ;
A10: r [= z1 by A5, A8, LATTICE3:def_16;
consider z3 being strict Subspace of VS such that
A11: z3 = z1 by VECTSP_5:def_3;
 Z1 = the carrier of z3 by A9, A11, Def4;
hence  the carrier of H c= Z1 by A4, A11, A10, Th6; ::_thesis: verum
end;
 (carr VS) . the Element of X in (carr VS) .: X by FUNCT_2:35;
then  the carrier of H c= meet ((carr VS) .: X) by A6, SETFAM_1:5;
then  the carrier of H c= the carrier of (meet X) by Def5;
hence  r [= p by A4, Th6; ::_thesis: verum
end;
end;
end;

theorem Th10: :: VECTSP_8:10
for F being Field
for x being set
for VS being strict VectSp of F
for S being Subset of VS st not S is empty & S is linearly-closed & x in Lin S holds
x in S
proof
let F be Field; ::_thesis: for x being set
for VS being strict VectSp of F
for S being Subset of VS st not S is empty & S is linearly-closed & x in Lin S holds
x in S
let x be set ; ::_thesis: for VS being strict VectSp of F
for S being Subset of VS st not S is empty & S is linearly-closed & x in Lin S holds
x in S
let VS be strict VectSp of F; ::_thesis: for S being Subset of VS st not S is empty & S is linearly-closed & x in Lin S holds
x in S
let S be Subset of VS; ::_thesis: ( not S is empty & S is linearly-closed & x in Lin S implies x in S )
assume  ( not S is empty & S is linearly-closed ) ; ::_thesis: ( not x in Lin S or x in S )
then consider W being strict Subspace of VS such that
A1: S = the carrier of W by VECTSP_4:34;
assume A2: x in Lin S ; ::_thesis: x in S
 Lin S = W by A1, VECTSP_7:11;
hence  x in S by A2, A1, STRUCT_0:def_5; ::_thesis: verum
end;

definition
let F be Field;
let A, B be strict VectSp of F;
let f be Function of the carrier of A, the carrier of B;
func FuncLatt f ->  Function of the carrier of (lattice A), the carrier of (lattice B) means :Def7: :: VECTSP_8:def 7
 for S being strict Subspace of A
for B0 being Subset of B st B0 = f .: the carrier of S holds
it . S = Lin B0;
existence
 ex b1 being Function of the carrier of (lattice A), the carrier of (lattice B) st
for S being strict Subspace of A
for B0 being Subset of B st B0 = f .: the carrier of S holds
b1 . S = Lin B0
proof
defpred S1[ set , set ] means  for S being Subspace of A st S = $1 holds
$2 = Lin (f .: the carrier of S);
A1: for x being set st x in the carrier of (lattice A) holds
ex y being set st
( y in the carrier of (lattice B) & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in the carrier of (lattice A) implies ex y being set st
( y in the carrier of (lattice B) & S1[x,y] ) )
assume  x in the carrier of (lattice A) ; ::_thesis: ex y being set st
( y in the carrier of (lattice B) & S1[x,y] )
then consider X being strict Subspace of A such that
A2: X = x by VECTSP_5:def_3;
reconsider y = f .: the carrier of X as Subset of B ;
consider Y being strict Subspace of B such that
A3: Y = Lin y ;
take  Y ; ::_thesis: ( Y in the carrier of (lattice B) & S1[x,Y] )
thus  ( Y in the carrier of (lattice B) & S1[x,Y] ) by A2, A3, VECTSP_5:def_3; ::_thesis: verum
end;
consider f1 being Function of the carrier of (lattice A), the carrier of (lattice B) such that
A4: for x being set st x in the carrier of (lattice A) holds
S1[x,f1 . x] from FUNCT_2:sch_1(A1);
take  f1 ; ::_thesis: for S being strict Subspace of A
for B0 being Subset of B st B0 = f .: the carrier of S holds
f1 . S = Lin B0
thus  for S being strict Subspace of A
for B0 being Subset of B st B0 = f .: the carrier of S holds
f1 . S = Lin B0 ::_thesis: verum
proof
let S be strict Subspace of A; ::_thesis: for B0 being Subset of B st B0 = f .: the carrier of S holds
f1 . S = Lin B0
let B0 be Subset of B; ::_thesis: ( B0 = f .: the carrier of S implies f1 . S = Lin B0 )
A5: S is Element of Subspaces A by VECTSP_5:def_3;
assume  B0 = f .: the carrier of S ; ::_thesis: f1 . S = Lin B0
hence  f1 . S = Lin B0 by A4, A5; ::_thesis: verum
end;
end;
uniqueness
 for b1, b2 being Function of the carrier of (lattice A), the carrier of (lattice B) st ( for S being strict Subspace of A
for B0 being Subset of B st B0 = f .: the carrier of S holds
b1 . S = Lin B0 ) & ( for S being strict Subspace of A
for B0 being Subset of B st B0 = f .: the carrier of S holds
b2 . S = Lin B0 ) holds
b1 = b2
proof
let F1, F2 be Function of the carrier of (lattice A), the carrier of (lattice B); ::_thesis: ( ( for S being strict Subspace of A
for B0 being Subset of B st B0 = f .: the carrier of S holds
F1 . S = Lin B0 ) & ( for S being strict Subspace of A
for B0 being Subset of B st B0 = f .: the carrier of S holds
F2 . S = Lin B0 ) implies F1 = F2 )
assume that
A6: for S being strict Subspace of A
for B0 being Subset of B st B0 = f .: the carrier of S holds
F1 . S = Lin B0 and
A7: for S being strict Subspace of A
for B0 being Subset of B st B0 = f .: the carrier of S holds
F2 . S = Lin B0 ; ::_thesis: F1 = F2
 for h being set st h in the carrier of (lattice A) holds
F1 . h = F2 . h
proof
let h be set ; ::_thesis: ( h in the carrier of (lattice A) implies F1 . h = F2 . h )
assume  h in the carrier of (lattice A) ; ::_thesis: F1 . h = F2 . h
then consider S being strict Subspace of A such that
A8: S = h by VECTSP_5:def_3;
reconsider B0 = f .: the carrier of S as Subset of B ;
 F1 . h = Lin B0 by A6, A8;
hence  F1 . h = F2 . h by A7, A8; ::_thesis: verum
end;
hence  F1 = F2 by FUNCT_2:12; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines FuncLatt VECTSP_8:def_7_:_
 for F being Field
for A, B being strict VectSp of F
for f being Function of the carrier of A, the carrier of B
for b5 being Function of the carrier of (lattice A), the carrier of (lattice B) holds
( b5 = FuncLatt f iff for S being strict Subspace of A
for B0 being Subset of B st B0 = f .: the carrier of S holds
b5 . S = Lin B0 );

definition
let L1, L2 be Lattice;
mode Semilattice-Homomorphism of L1,L2 ->  Function of the carrier of L1, the carrier of L2 means :Def8: :: VECTSP_8:def 8
 for a, b being Element of L1 holds it . (a "/\" b) = (it . a) "/\" (it . b);
existence
 ex b1 being Function of the carrier of L1, the carrier of L2 st
for a, b being Element of L1 holds b1 . (a "/\" b) = (b1 . a) "/\" (b1 . b)
proof
set h = the Homomorphism of L1,L2;
take  the Homomorphism of L1,L2 ; ::_thesis: for a, b being Element of L1 holds the Homomorphism of L1,L2 . (a "/\" b) = ( the Homomorphism of L1,L2 . a) "/\" ( the Homomorphism of L1,L2 . b)
thus  for a, b being Element of L1 holds the Homomorphism of L1,L2 . (a "/\" b) = ( the Homomorphism of L1,L2 . a) "/\" ( the Homomorphism of L1,L2 . b) by LATTICE4:def_1; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines Semilattice-Homomorphism VECTSP_8:def_8_:_
 for L1, L2 being Lattice
for b3 being Function of the carrier of L1, the carrier of L2 holds
( b3 is Semilattice-Homomorphism of L1,L2 iff for a, b being Element of L1 holds b3 . (a "/\" b) = (b3 . a) "/\" (b3 . b) );

definition
let L1, L2 be Lattice;
mode sup-Semilattice-Homomorphism of L1,L2 ->  Function of the carrier of L1, the carrier of L2 means :Def9: :: VECTSP_8:def 9
 for a, b being Element of L1 holds it . (a "\/" b) = (it . a) "\/" (it . b);
existence
 ex b1 being Function of the carrier of L1, the carrier of L2 st
for a, b being Element of L1 holds b1 . (a "\/" b) = (b1 . a) "\/" (b1 . b)
proof
set h = the Homomorphism of L1,L2;
take  the Homomorphism of L1,L2 ; ::_thesis: for a, b being Element of L1 holds the Homomorphism of L1,L2 . (a "\/" b) = ( the Homomorphism of L1,L2 . a) "\/" ( the Homomorphism of L1,L2 . b)
thus  for a, b being Element of L1 holds the Homomorphism of L1,L2 . (a "\/" b) = ( the Homomorphism of L1,L2 . a) "\/" ( the Homomorphism of L1,L2 . b) by LATTICE4:def_1; ::_thesis: verum
end;
end;

:: deftheorem Def9 defines sup-Semilattice-Homomorphism VECTSP_8:def_9_:_
 for L1, L2 being Lattice
for b3 being Function of the carrier of L1, the carrier of L2 holds
( b3 is sup-Semilattice-Homomorphism of L1,L2 iff for a, b being Element of L1 holds b3 . (a "\/" b) = (b3 . a) "\/" (b3 . b) );

theorem :: VECTSP_8:11
for L1, L2 being Lattice
for f being Function of the carrier of L1, the carrier of L2 holds
( f is Homomorphism of L1,L2 iff ( f is sup-Semilattice-Homomorphism of L1,L2 & f is Semilattice-Homomorphism of L1,L2 ) )
proof
let L1, L2 be Lattice; ::_thesis: for f being Function of the carrier of L1, the carrier of L2 holds
( f is Homomorphism of L1,L2 iff ( f is sup-Semilattice-Homomorphism of L1,L2 & f is Semilattice-Homomorphism of L1,L2 ) )
let f be Function of the carrier of L1, the carrier of L2; ::_thesis: ( f is Homomorphism of L1,L2 iff ( f is sup-Semilattice-Homomorphism of L1,L2 & f is Semilattice-Homomorphism of L1,L2 ) )
A1: ( f is sup-Semilattice-Homomorphism of L1,L2 & f is Semilattice-Homomorphism of L1,L2 implies f is Homomorphism of L1,L2 )
proof
assume  ( f is sup-Semilattice-Homomorphism of L1,L2 & f is Semilattice-Homomorphism of L1,L2 ) ; ::_thesis: f is Homomorphism of L1,L2
then  for a, b being Element of L1 holds
( f . (a "\/" b) = (f . a) "\/" (f . b) & f . (a "/\" b) = (f . a) "/\" (f . b) ) by Def8, Def9;
hence  f is Homomorphism of L1,L2 by LATTICE4:def_1; ::_thesis: verum
end;
 ( f is Homomorphism of L1,L2 implies ( f is sup-Semilattice-Homomorphism of L1,L2 & f is Semilattice-Homomorphism of L1,L2 ) )
proof
assume  f is Homomorphism of L1,L2 ; ::_thesis: ( f is sup-Semilattice-Homomorphism of L1,L2 & f is Semilattice-Homomorphism of L1,L2 )
then  for a, b being Element of L1 holds
( f . (a "\/" b) = (f . a) "\/" (f . b) & f . (a "/\" b) = (f . a) "/\" (f . b) ) by LATTICE4:def_1;
hence  ( f is sup-Semilattice-Homomorphism of L1,L2 & f is Semilattice-Homomorphism of L1,L2 ) by Def8, Def9; ::_thesis: verum
end;
hence  ( f is Homomorphism of L1,L2 iff ( f is sup-Semilattice-Homomorphism of L1,L2 & f is Semilattice-Homomorphism of L1,L2 ) ) by A1; ::_thesis: verum
end;

theorem Th12: :: VECTSP_8:12
for F being Field
for A, B being strict VectSp of F
for f being Function of A,B st f is additive & f is homogeneous holds
FuncLatt f is sup-Semilattice-Homomorphism of lattice A, lattice B
proof
let F be Field; ::_thesis: for A, B being strict VectSp of F
for f being Function of A,B st f is additive & f is homogeneous holds
FuncLatt f is sup-Semilattice-Homomorphism of lattice A, lattice B
let A, B be strict VectSp of F; ::_thesis: for f being Function of A,B st f is additive & f is homogeneous holds
FuncLatt f is sup-Semilattice-Homomorphism of lattice A, lattice B
let f be Function of A,B; ::_thesis: ( f is additive & f is homogeneous implies FuncLatt f is sup-Semilattice-Homomorphism of lattice A, lattice B )
assume A1: ( f is additive & f is homogeneous ) ; ::_thesis: FuncLatt f is sup-Semilattice-Homomorphism of lattice A, lattice B
 FuncLatt f is sup-Semilattice-Homomorphism of lattice A, lattice B
proof
let a, b be Element of (lattice A); :: according to VECTSP_8:def_9 ::_thesis: (FuncLatt f) . (a "\/" b) = ((FuncLatt f) . a) "\/" ((FuncLatt f) . b)
 (FuncLatt f) . (a "\/" b) = ((FuncLatt f) . a) "\/" ((FuncLatt f) . b)
proof
reconsider b2 = (FuncLatt f) . b as Element of (lattice B) ;
consider B1 being strict Subspace of A such that
A2: B1 = b by VECTSP_5:def_3;
A3: b2 = Lin (f .: the carrier of B1) by A2, Def7;
 0. A in B1 by VECTSP_4:17;
then A4: 0. A in the carrier of B1 by STRUCT_0:def_5;
reconsider a2 = (FuncLatt f) . a as Element of (lattice B) ;
consider A1 being strict Subspace of A such that
A5: A1 = a by VECTSP_5:def_3;
A6: f .: the carrier of A1 is linearly-closed
proof
set BB = f .: the carrier of A1;
A7: for v, u being Element of B st v in f .: the carrier of A1 & u in f .: the carrier of A1 holds
v + u in f .: the carrier of A1
proof
let v, u be Element of B; ::_thesis: ( v in f .: the carrier of A1 & u in f .: the carrier of A1 implies v + u in f .: the carrier of A1 )
assume that
A8: v in f .: the carrier of A1 and
A9: u in f .: the carrier of A1 ; ::_thesis: v + u in f .: the carrier of A1
consider y being Element of A such that
A10: y in the carrier of A1 and
A11: u = f . y by A9, FUNCT_2:65;
A12: y in A1 by A10, STRUCT_0:def_5;
consider x being Element of A such that
A13: x in the carrier of A1 and
A14: v = f . x by A8, FUNCT_2:65;
 x in A1 by A13, STRUCT_0:def_5;
then  x + y in A1 by A12, VECTSP_4:20;
then  x + y in the carrier of A1 by STRUCT_0:def_5;
then  f . (x + y) in f .: the carrier of A1 by FUNCT_2:35;
hence  v + u in f .: the carrier of A1 by A1, A14, A11, VECTSP_1:def_20; ::_thesis: verum
end;
 for a being Element of F
for v being Element of B st v in f .: the carrier of A1 holds
a * v in f .: the carrier of A1
proof
let a be Element of F; ::_thesis: for v being Element of B st v in f .: the carrier of A1 holds
a * v in f .: the carrier of A1
let v be Element of B; ::_thesis: ( v in f .: the carrier of A1 implies a * v in f .: the carrier of A1 )
assume  v in f .: the carrier of A1 ; ::_thesis: a * v in f .: the carrier of A1
then consider x being Element of A such that
A15: x in the carrier of A1 and
A16: v = f . x by FUNCT_2:65;
 x in A1 by A15, STRUCT_0:def_5;
then  a * x in A1 by VECTSP_4:21;
then  a * x in the carrier of A1 by STRUCT_0:def_5;
then  f . (a * x) in f .: the carrier of A1 by FUNCT_2:35;
hence  a * v in f .: the carrier of A1 by A1, A16, MOD_2:def_2; ::_thesis: verum
end;
hence  f .: the carrier of A1 is linearly-closed by A7, VECTSP_4:def_1; ::_thesis: verum
end;
A17: f .: the carrier of B1 is linearly-closed
proof
set BB = f .: the carrier of B1;
A18: for v, u being Element of B st v in f .: the carrier of B1 & u in f .: the carrier of B1 holds
v + u in f .: the carrier of B1
proof
let v, u be Element of B; ::_thesis: ( v in f .: the carrier of B1 & u in f .: the carrier of B1 implies v + u in f .: the carrier of B1 )
assume that
A19: v in f .: the carrier of B1 and
A20: u in f .: the carrier of B1 ; ::_thesis: v + u in f .: the carrier of B1
consider y being Element of A such that
A21: y in the carrier of B1 and
A22: u = f . y by A20, FUNCT_2:65;
A23: y in B1 by A21, STRUCT_0:def_5;
consider x being Element of A such that
A24: x in the carrier of B1 and
A25: v = f . x by A19, FUNCT_2:65;
 x in B1 by A24, STRUCT_0:def_5;
then  x + y in B1 by A23, VECTSP_4:20;
then  x + y in the carrier of B1 by STRUCT_0:def_5;
then  f . (x + y) in f .: the carrier of B1 by FUNCT_2:35;
hence  v + u in f .: the carrier of B1 by A1, A25, A22, VECTSP_1:def_20; ::_thesis: verum
end;
 for a being Element of F
for v being Element of B st v in f .: the carrier of B1 holds
a * v in f .: the carrier of B1
proof
let a be Element of F; ::_thesis: for v being Element of B st v in f .: the carrier of B1 holds
a * v in f .: the carrier of B1
let v be Element of B; ::_thesis: ( v in f .: the carrier of B1 implies a * v in f .: the carrier of B1 )
assume  v in f .: the carrier of B1 ; ::_thesis: a * v in f .: the carrier of B1
then consider x being Element of A such that
A26: x in the carrier of B1 and
A27: v = f . x by FUNCT_2:65;
 x in B1 by A26, STRUCT_0:def_5;
then  a * x in B1 by VECTSP_4:21;
then  a * x in the carrier of B1 by STRUCT_0:def_5;
then  f . (a * x) in f .: the carrier of B1 by FUNCT_2:35;
hence  a * v in f .: the carrier of B1 by A1, A27, MOD_2:def_2; ::_thesis: verum
end;
hence  f .: the carrier of B1 is linearly-closed by A18, VECTSP_4:def_1; ::_thesis: verum
end;
reconsider P = Lin (f .: the carrier of (A1 + B1)) as Subspace of B ;
A28: (FuncLatt f) . (A1 + B1) = Lin (f .: the carrier of (A1 + B1)) by Def7;
 0. A in A1 by VECTSP_4:17;
then A29: 0. A in the carrier of A1 by STRUCT_0:def_5;
A30: a2 = Lin (f .: the carrier of A1) by A5, Def7;
A31: dom f = the carrier of A by FUNCT_2:def_1;
 ex y1 being Element of B st y1 = f . (0. A) ;
then A32: f .: the carrier of B1 <> {} by A31, A4, FUNCT_1:def_6;
then consider B3 being strict Subspace of B such that
A33: the carrier of B3 = f .: the carrier of B1 by A17, VECTSP_4:34;
A34: Lin (f .: the carrier of B1) = B3 by A33, VECTSP_7:11;
 ex y being Element of B st y = f . (0. A) ;
then A35: f .: the carrier of A1 <> {} by A31, A29, FUNCT_1:def_6;
then consider A3 being strict Subspace of B such that
A36: the carrier of A3 = f .: the carrier of A1 by A6, VECTSP_4:34;
reconsider AB = A3 + B3 as Subspace of B ;
A37: the carrier of AB c= the carrier of P
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of AB or x in the carrier of P )
A38: f .: the carrier of A1 c= f .: the carrier of (A1 + B1)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f .: the carrier of A1 or x in f .: the carrier of (A1 + B1) )
A39: the carrier of A1 c= the carrier of (A1 + B1)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of A1 or x in the carrier of (A1 + B1) )
assume A40: x in the carrier of A1 ; ::_thesis: x in the carrier of (A1 + B1)
then A41: x in A1 by STRUCT_0:def_5;
 the carrier of A1 c= the carrier of A by VECTSP_4:def_2;
then reconsider x = x as Element of A by A40;
 x in A1 + B1 by A41, VECTSP_5:2;
hence  x in the carrier of (A1 + B1) by STRUCT_0:def_5; ::_thesis: verum
end;
assume A42: x in f .: the carrier of A1 ; ::_thesis: x in f .: the carrier of (A1 + B1)
then reconsider x = x as Element of B ;
 ex c being Element of A st
( c in the carrier of A1 & x = f . c ) by A42, FUNCT_2:65;
hence  x in f .: the carrier of (A1 + B1) by A39, FUNCT_2:35; ::_thesis: verum
end;
A43: f .: the carrier of B1 c= f .: the carrier of (A1 + B1)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f .: the carrier of B1 or x in f .: the carrier of (A1 + B1) )
A44: the carrier of B1 c= the carrier of (A1 + B1)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of B1 or x in the carrier of (A1 + B1) )
assume A45: x in the carrier of B1 ; ::_thesis: x in the carrier of (A1 + B1)
then A46: x in B1 by STRUCT_0:def_5;
 the carrier of B1 c= the carrier of A by VECTSP_4:def_2;
then reconsider x = x as Element of A by A45;
 x in A1 + B1 by A46, VECTSP_5:2;
hence  x in the carrier of (A1 + B1) by STRUCT_0:def_5; ::_thesis: verum
end;
assume A47: x in f .: the carrier of B1 ; ::_thesis: x in f .: the carrier of (A1 + B1)
then reconsider x = x as Element of B ;
 ex c being Element of A st
( c in the carrier of B1 & x = f . c ) by A47, FUNCT_2:65;
hence  x in f .: the carrier of (A1 + B1) by A44, FUNCT_2:35; ::_thesis: verum
end;
assume  x in the carrier of AB ; ::_thesis: x in the carrier of P
then  x in A3 + B3 by STRUCT_0:def_5;
then consider u, v being Element of B such that
A48: u in A3 and
A49: v in B3 and
A50: x = u + v by VECTSP_5:1;
 v in f .: the carrier of B1 by A33, A49, STRUCT_0:def_5;
then A51: v in P by A43, VECTSP_7:8;
 u in f .: the carrier of A1 by A36, A48, STRUCT_0:def_5;
then  u in P by A38, VECTSP_7:8;
then  x in P by A50, A51, VECTSP_4:20;
hence  x in the carrier of P by STRUCT_0:def_5; ::_thesis: verum
end;
A52: Lin (f .: the carrier of A1) = A3 by A36, VECTSP_7:11;
A53: f .: the carrier of (A1 + B1) is linearly-closed
proof
set BB = f .: the carrier of (A1 + B1);
A54: for v, u being Element of B st v in f .: the carrier of (A1 + B1) & u in f .: the carrier of (A1 + B1) holds
v + u in f .: the carrier of (A1 + B1)
proof
let v, u be Element of B; ::_thesis: ( v in f .: the carrier of (A1 + B1) & u in f .: the carrier of (A1 + B1) implies v + u in f .: the carrier of (A1 + B1) )
assume that
A55: v in f .: the carrier of (A1 + B1) and
A56: u in f .: the carrier of (A1 + B1) ; ::_thesis: v + u in f .: the carrier of (A1 + B1)
consider y being Element of A such that
A57: y in the carrier of (A1 + B1) and
A58: u = f . y by A56, FUNCT_2:65;
A59: y in A1 + B1 by A57, STRUCT_0:def_5;
consider x being Element of A such that
A60: x in the carrier of (A1 + B1) and
A61: v = f . x by A55, FUNCT_2:65;
 x in A1 + B1 by A60, STRUCT_0:def_5;
then  x + y in A1 + B1 by A59, VECTSP_4:20;
then  x + y in the carrier of (A1 + B1) by STRUCT_0:def_5;
then  f . (x + y) in f .: the carrier of (A1 + B1) by FUNCT_2:35;
hence  v + u in f .: the carrier of (A1 + B1) by A1, A61, A58, VECTSP_1:def_20; ::_thesis: verum
end;
 for a being Element of F
for v being Element of B st v in f .: the carrier of (A1 + B1) holds
a * v in f .: the carrier of (A1 + B1)
proof
let a be Element of F; ::_thesis: for v being Element of B st v in f .: the carrier of (A1 + B1) holds
a * v in f .: the carrier of (A1 + B1)
let v be Element of B; ::_thesis: ( v in f .: the carrier of (A1 + B1) implies a * v in f .: the carrier of (A1 + B1) )
assume  v in f .: the carrier of (A1 + B1) ; ::_thesis: a * v in f .: the carrier of (A1 + B1)
then consider x being Element of A such that
A62: x in the carrier of (A1 + B1) and
A63: v = f . x by FUNCT_2:65;
 x in A1 + B1 by A62, STRUCT_0:def_5;
then  a * x in A1 + B1 by VECTSP_4:21;
then  a * x in the carrier of (A1 + B1) by STRUCT_0:def_5;
then  f . (a * x) in f .: the carrier of (A1 + B1) by FUNCT_2:35;
hence  a * v in f .: the carrier of (A1 + B1) by A1, A63, MOD_2:def_2; ::_thesis: verum
end;
hence  f .: the carrier of (A1 + B1) is linearly-closed by A54, VECTSP_4:def_1; ::_thesis: verum
end;
 the carrier of P c= the carrier of AB
proof
A64: the carrier of (A3 + B3) c= f .: the carrier of (A1 + B1)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (A3 + B3) or x in f .: the carrier of (A1 + B1) )
assume  x in the carrier of (A3 + B3) ; ::_thesis: x in f .: the carrier of (A1 + B1)
then  x in A3 + B3 by STRUCT_0:def_5;
then consider vb, ub being Element of B such that
A65: vb in A3 and
A66: ub in B3 and
A67: x = vb + ub by VECTSP_5:1;
consider ua being Element of A such that
A68: ua in the carrier of B1 and
A69: ub = f . ua by A32, A17, A34, A66, Th10, FUNCT_2:65;
 ua in B1 by A68, STRUCT_0:def_5;
then A70: ua in A1 + B1 by VECTSP_5:2;
consider va being Element of A such that
A71: va in the carrier of A1 and
A72: vb = f . va by A35, A6, A52, A65, Th10, FUNCT_2:65;
 va in A1 by A71, STRUCT_0:def_5;
then  va in A1 + B1 by VECTSP_5:2;
then  ua + va in A1 + B1 by A70, VECTSP_4:20;
then  ua + va in the carrier of (A1 + B1) by STRUCT_0:def_5;
then  f . (ua + va) in f .: the carrier of (A1 + B1) by FUNCT_2:35;
hence  x in f .: the carrier of (A1 + B1) by A1, A67, A72, A69, VECTSP_1:def_20; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of P or x in the carrier of AB )
assume  x in the carrier of P ; ::_thesis: x in the carrier of AB
then A73: x in P by STRUCT_0:def_5;
 f .: the carrier of (A1 + B1) c= the carrier of (A3 + B3)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f .: the carrier of (A1 + B1) or x in the carrier of (A3 + B3) )
assume A74: x in f .: the carrier of (A1 + B1) ; ::_thesis: x in the carrier of (A3 + B3)
then reconsider x = x as Element of B ;
consider c being Element of A such that
A75: c in the carrier of (A1 + B1) and
A76: x = f . c by A74, FUNCT_2:65;
 c in A1 + B1 by A75, STRUCT_0:def_5;
then consider u, v being Element of A such that
A77: u in A1 and
A78: v in B1 and
A79: c = u + v by VECTSP_5:1;
 v in the carrier of B1 by A78, STRUCT_0:def_5;
then A80: f . v in Lin (f .: the carrier of B1) by FUNCT_2:35, VECTSP_7:8;
 u in the carrier of A1 by A77, STRUCT_0:def_5;
then A81: f . u in Lin (f .: the carrier of A1) by FUNCT_2:35, VECTSP_7:8;
 x = (f . u) + (f . v) by A1, A76, A79, VECTSP_1:def_20;
then  x in (Lin (f .: the carrier of A1)) + (Lin (f .: the carrier of B1)) by A81, A80, VECTSP_5:1;
hence  x in the carrier of (A3 + B3) by A52, A34, STRUCT_0:def_5; ::_thesis: verum
end;
then  f .: the carrier of (A1 + B1) = the carrier of (A3 + B3) by A64, XBOOLE_0:def_10;
hence  x in the carrier of AB by A53, A73, Th10; ::_thesis: verum
end;
then  the carrier of AB = the carrier of P by A37, XBOOLE_0:def_10;
then A82: P = AB by VECTSP_4:29;
 (FuncLatt f) . (a "\/" b) = (FuncLatt f) . (A1 + B1) by A5, A2, Th7;
hence  (FuncLatt f) . (a "\/" b) = ((FuncLatt f) . a) "\/" ((FuncLatt f) . b) by A30, A3, A28, A52, A34, A82, Th7; ::_thesis: verum
end;
hence  (FuncLatt f) . (a "\/" b) = ((FuncLatt f) . a) "\/" ((FuncLatt f) . b) ; ::_thesis: verum
end;
hence  FuncLatt f is sup-Semilattice-Homomorphism of lattice A, lattice B ; ::_thesis: verum
end;

theorem :: VECTSP_8:13
for F being Field
for A, B being strict VectSp of F
for f being Function of A,B st f is one-to-one & f is additive & f is homogeneous holds
FuncLatt f is Homomorphism of lattice A, lattice B
proof
let F be Field; ::_thesis: for A, B being strict VectSp of F
for f being Function of A,B st f is one-to-one & f is additive & f is homogeneous holds
FuncLatt f is Homomorphism of lattice A, lattice B
let A, B be strict VectSp of F; ::_thesis: for f being Function of A,B st f is one-to-one & f is additive & f is homogeneous holds
FuncLatt f is Homomorphism of lattice A, lattice B
let f be Function of A,B; ::_thesis: ( f is one-to-one & f is additive & f is homogeneous implies FuncLatt f is Homomorphism of lattice A, lattice B )
assume A1: ( f is one-to-one & f is additive & f is homogeneous ) ; ::_thesis: FuncLatt f is Homomorphism of lattice A, lattice B
 for a, b being Element of (lattice A) holds
( (FuncLatt f) . (a "\/" b) = ((FuncLatt f) . a) "\/" ((FuncLatt f) . b) & (FuncLatt f) . (a "/\" b) = ((FuncLatt f) . a) "/\" ((FuncLatt f) . b) )
proof
let a, b be Element of (lattice A); ::_thesis: ( (FuncLatt f) . (a "\/" b) = ((FuncLatt f) . a) "\/" ((FuncLatt f) . b) & (FuncLatt f) . (a "/\" b) = ((FuncLatt f) . a) "/\" ((FuncLatt f) . b) )
A2: (FuncLatt f) . (a "/\" b) = ((FuncLatt f) . a) "/\" ((FuncLatt f) . b)
proof
reconsider b2 = (FuncLatt f) . b as Element of (lattice B) ;
consider B1 being strict Subspace of A such that
A3: B1 = b by VECTSP_5:def_3;
A4: b2 = Lin (f .: the carrier of B1) by A3, Def7;
 0. A in B1 by VECTSP_4:17;
then A5: 0. A in the carrier of B1 by STRUCT_0:def_5;
reconsider a2 = (FuncLatt f) . a as Element of (lattice B) ;
consider A1 being strict Subspace of A such that
A6: A1 = a by VECTSP_5:def_3;
reconsider P = Lin (f .: the carrier of (A1 /\ B1)) as Subspace of B ;
A7: (FuncLatt f) . (A1 /\ B1) = Lin (f .: the carrier of (A1 /\ B1)) by Def7;
 0. A in A1 by VECTSP_4:17;
then A8: 0. A in the carrier of A1 by STRUCT_0:def_5;
A9: a2 = Lin (f .: the carrier of A1) by A6, Def7;
A10: dom f = the carrier of A by FUNCT_2:def_1;
A11: f .: the carrier of B1 is linearly-closed
proof
set BB = f .: the carrier of B1;
A12: for v, u being Element of B st v in f .: the carrier of B1 & u in f .: the carrier of B1 holds
v + u in f .: the carrier of B1
proof
let v, u be Element of B; ::_thesis: ( v in f .: the carrier of B1 & u in f .: the carrier of B1 implies v + u in f .: the carrier of B1 )
assume that
A13: v in f .: the carrier of B1 and
A14: u in f .: the carrier of B1 ; ::_thesis: v + u in f .: the carrier of B1
consider y being Element of A such that
A15: y in the carrier of B1 and
A16: u = f . y by A14, FUNCT_2:65;
A17: y in B1 by A15, STRUCT_0:def_5;
consider x being Element of A such that
A18: x in the carrier of B1 and
A19: v = f . x by A13, FUNCT_2:65;
 x in B1 by A18, STRUCT_0:def_5;
then  x + y in B1 by A17, VECTSP_4:20;
then  x + y in the carrier of B1 by STRUCT_0:def_5;
then  f . (x + y) in f .: the carrier of B1 by FUNCT_2:35;
hence  v + u in f .: the carrier of B1 by A1, A19, A16, VECTSP_1:def_20; ::_thesis: verum
end;
 for a being Element of F
for v being Element of B st v in f .: the carrier of B1 holds
a * v in f .: the carrier of B1
proof
let a be Element of F; ::_thesis: for v being Element of B st v in f .: the carrier of B1 holds
a * v in f .: the carrier of B1
let v be Element of B; ::_thesis: ( v in f .: the carrier of B1 implies a * v in f .: the carrier of B1 )
assume  v in f .: the carrier of B1 ; ::_thesis: a * v in f .: the carrier of B1
then consider x being Element of A such that
A20: x in the carrier of B1 and
A21: v = f . x by FUNCT_2:65;
 x in B1 by A20, STRUCT_0:def_5;
then  a * x in B1 by VECTSP_4:21;
then  a * x in the carrier of B1 by STRUCT_0:def_5;
then  f . (a * x) in f .: the carrier of B1 by FUNCT_2:35;
hence  a * v in f .: the carrier of B1 by A1, A21, MOD_2:def_2; ::_thesis: verum
end;
hence  f .: the carrier of B1 is linearly-closed by A12, VECTSP_4:def_1; ::_thesis: verum
end;
A22: f .: the carrier of A1 is linearly-closed
proof
set BB = f .: the carrier of A1;
A23: for v, u being Element of B st v in f .: the carrier of A1 & u in f .: the carrier of A1 holds
v + u in f .: the carrier of A1
proof
let v, u be Element of B; ::_thesis: ( v in f .: the carrier of A1 & u in f .: the carrier of A1 implies v + u in f .: the carrier of A1 )
assume that
A24: v in f .: the carrier of A1 and
A25: u in f .: the carrier of A1 ; ::_thesis: v + u in f .: the carrier of A1
consider y being Element of A such that
A26: y in the carrier of A1 and
A27: u = f . y by A25, FUNCT_2:65;
A28: y in A1 by A26, STRUCT_0:def_5;
consider x being Element of A such that
A29: x in the carrier of A1 and
A30: v = f . x by A24, FUNCT_2:65;
 x in A1 by A29, STRUCT_0:def_5;
then  x + y in A1 by A28, VECTSP_4:20;
then  x + y in the carrier of A1 by STRUCT_0:def_5;
then  f . (x + y) in f .: the carrier of A1 by FUNCT_2:35;
hence  v + u in f .: the carrier of A1 by A1, A30, A27, VECTSP_1:def_20; ::_thesis: verum
end;
 for a being Element of F
for v being Element of B st v in f .: the carrier of A1 holds
a * v in f .: the carrier of A1
proof
let a be Element of F; ::_thesis: for v being Element of B st v in f .: the carrier of A1 holds
a * v in f .: the carrier of A1
let v be Element of B; ::_thesis: ( v in f .: the carrier of A1 implies a * v in f .: the carrier of A1 )
assume  v in f .: the carrier of A1 ; ::_thesis: a * v in f .: the carrier of A1
then consider x being Element of A such that
A31: x in the carrier of A1 and
A32: v = f . x by FUNCT_2:65;
 x in A1 by A31, STRUCT_0:def_5;
then  a * x in A1 by VECTSP_4:21;
then  a * x in the carrier of A1 by STRUCT_0:def_5;
then  f . (a * x) in f .: the carrier of A1 by FUNCT_2:35;
hence  a * v in f .: the carrier of A1 by A1, A32, MOD_2:def_2; ::_thesis: verum
end;
hence  f .: the carrier of A1 is linearly-closed by A23, VECTSP_4:def_1; ::_thesis: verum
end;
 ex y1 being Element of B st y1 = f . (0. A) ;
then A33: f .: the carrier of B1 <> {} by A10, A5, FUNCT_1:def_6;
then consider B3 being strict Subspace of B such that
A34: the carrier of B3 = f .: the carrier of B1 by A11, VECTSP_4:34;
A35: Lin (f .: the carrier of B1) = B3 by A34, VECTSP_7:11;
 ex y being Element of B st y = f . (0. A) ;
then A36: f .: the carrier of A1 <> {} by A10, A8, FUNCT_1:def_6;
then consider A3 being strict Subspace of B such that
A37: the carrier of A3 = f .: the carrier of A1 by A22, VECTSP_4:34;
reconsider AB = A3 /\ B3 as Subspace of B ;
A38: Lin (f .: the carrier of A1) = A3 by A37, VECTSP_7:11;
A39: f .: the carrier of (A1 /\ B1) is linearly-closed
proof
set BB = f .: the carrier of (A1 /\ B1);
A40: for v, u being Element of B st v in f .: the carrier of (A1 /\ B1) & u in f .: the carrier of (A1 /\ B1) holds
v + u in f .: the carrier of (A1 /\ B1)
proof
let v, u be Element of B; ::_thesis: ( v in f .: the carrier of (A1 /\ B1) & u in f .: the carrier of (A1 /\ B1) implies v + u in f .: the carrier of (A1 /\ B1) )
assume that
A41: v in f .: the carrier of (A1 /\ B1) and
A42: u in f .: the carrier of (A1 /\ B1) ; ::_thesis: v + u in f .: the carrier of (A1 /\ B1)
consider y being Element of A such that
A43: y in the carrier of (A1 /\ B1) and
A44: u = f . y by A42, FUNCT_2:65;
A45: y in A1 /\ B1 by A43, STRUCT_0:def_5;
consider x being Element of A such that
A46: x in the carrier of (A1 /\ B1) and
A47: v = f . x by A41, FUNCT_2:65;
 x in A1 /\ B1 by A46, STRUCT_0:def_5;
then  x + y in A1 /\ B1 by A45, VECTSP_4:20;
then  x + y in the carrier of (A1 /\ B1) by STRUCT_0:def_5;
then  f . (x + y) in f .: the carrier of (A1 /\ B1) by FUNCT_2:35;
hence  v + u in f .: the carrier of (A1 /\ B1) by A1, A47, A44, VECTSP_1:def_20; ::_thesis: verum
end;
 for a being Element of F
for v being Element of B st v in f .: the carrier of (A1 /\ B1) holds
a * v in f .: the carrier of (A1 /\ B1)
proof
let a be Element of F; ::_thesis: for v being Element of B st v in f .: the carrier of (A1 /\ B1) holds
a * v in f .: the carrier of (A1 /\ B1)
let v be Element of B; ::_thesis: ( v in f .: the carrier of (A1 /\ B1) implies a * v in f .: the carrier of (A1 /\ B1) )
assume  v in f .: the carrier of (A1 /\ B1) ; ::_thesis: a * v in f .: the carrier of (A1 /\ B1)
then consider x being Element of A such that
A48: x in the carrier of (A1 /\ B1) and
A49: v = f . x by FUNCT_2:65;
 x in A1 /\ B1 by A48, STRUCT_0:def_5;
then  a * x in A1 /\ B1 by VECTSP_4:21;
then  a * x in the carrier of (A1 /\ B1) by STRUCT_0:def_5;
then  f . (a * x) in f .: the carrier of (A1 /\ B1) by FUNCT_2:35;
hence  a * v in f .: the carrier of (A1 /\ B1) by A1, A49, MOD_2:def_2; ::_thesis: verum
end;
hence  f .: the carrier of (A1 /\ B1) is linearly-closed by A40, VECTSP_4:def_1; ::_thesis: verum
end;
A50: the carrier of P c= the carrier of AB
proof
A51: the carrier of (A3 /\ B3) c= f .: the carrier of (A1 /\ B1)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (A3 /\ B3) or x in f .: the carrier of (A1 /\ B1) )
assume  x in the carrier of (A3 /\ B3) ; ::_thesis: x in f .: the carrier of (A1 /\ B1)
then A52: x in A3 /\ B3 by STRUCT_0:def_5;
then A53: x in Lin (f .: the carrier of A1) by A38, VECTSP_5:3;
then  x in f .: the carrier of A1 by A36, A22, Th10;
then reconsider x = x as Element of B ;
consider xa being Element of A such that
A54: xa in the carrier of A1 and
A55: x = f . xa by A36, A22, A53, Th10, FUNCT_2:65;
A56: xa in A1 by A54, STRUCT_0:def_5;
 x in Lin (f .: the carrier of B1) by A35, A52, VECTSP_5:3;
then consider xa1 being Element of A such that
A57: xa1 in the carrier of B1 and
A58: x = f . xa1 by A33, A11, Th10, FUNCT_2:65;
A59: xa1 in B1 by A57, STRUCT_0:def_5;
 xa1 = xa by A1, A55, A58, FUNCT_2:19;
then  xa in A1 /\ B1 by A56, A59, VECTSP_5:3;
then  xa in the carrier of (A1 /\ B1) by STRUCT_0:def_5;
hence  x in f .: the carrier of (A1 /\ B1) by A55, FUNCT_2:35; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of P or x in the carrier of AB )
assume  x in the carrier of P ; ::_thesis: x in the carrier of AB
then A60: x in P by STRUCT_0:def_5;
 f .: the carrier of (A1 /\ B1) c= the carrier of (A3 /\ B3)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f .: the carrier of (A1 /\ B1) or x in the carrier of (A3 /\ B3) )
assume A61: x in f .: the carrier of (A1 /\ B1) ; ::_thesis: x in the carrier of (A3 /\ B3)
then reconsider x = x as Element of B ;
consider c being Element of A such that
A62: c in the carrier of (A1 /\ B1) and
A63: x = f . c by A61, FUNCT_2:65;
A64: c in A1 /\ B1 by A62, STRUCT_0:def_5;
then  c in B1 by VECTSP_5:3;
then  c in the carrier of B1 by STRUCT_0:def_5;
then A65: f . c in Lin (f .: the carrier of B1) by FUNCT_2:35, VECTSP_7:8;
 c in A1 by A64, VECTSP_5:3;
then  c in the carrier of A1 by STRUCT_0:def_5;
then  f . c in Lin (f .: the carrier of A1) by FUNCT_2:35, VECTSP_7:8;
then  x in (Lin (f .: the carrier of A1)) /\ (Lin (f .: the carrier of B1)) by A63, A65, VECTSP_5:3;
hence  x in the carrier of (A3 /\ B3) by A38, A35, STRUCT_0:def_5; ::_thesis: verum
end;
then  f .: the carrier of (A1 /\ B1) = the carrier of (A3 /\ B3) by A51, XBOOLE_0:def_10;
hence  x in the carrier of AB by A39, A60, Th10; ::_thesis: verum
end;
 the carrier of AB c= the carrier of P
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of AB or x in the carrier of P )
assume  x in the carrier of AB ; ::_thesis: x in the carrier of P
then A66: x in A3 /\ B3 by STRUCT_0:def_5;
then  x in Lin (f .: the carrier of B1) by A35, VECTSP_5:3;
then consider xa1 being Element of A such that
A67: xa1 in the carrier of B1 and
A68: x = f . xa1 by A33, A11, Th10, FUNCT_2:65;
A69: xa1 in B1 by A67, STRUCT_0:def_5;
 x in Lin (f .: the carrier of A1) by A38, A66, VECTSP_5:3;
then  x in f .: the carrier of A1 by A37, A38, STRUCT_0:def_5;
then consider xa being Element of A such that
A70: xa in the carrier of A1 and
A71: x = f . xa by FUNCT_2:65;
A72: xa in A1 by A70, STRUCT_0:def_5;
 xa1 = xa by A1, A71, A68, FUNCT_2:19;
then  xa in A1 /\ B1 by A72, A69, VECTSP_5:3;
then  xa in the carrier of (A1 /\ B1) by STRUCT_0:def_5;
then  x in P by A71, FUNCT_2:35, VECTSP_7:8;
hence  x in the carrier of P by STRUCT_0:def_5; ::_thesis: verum
end;
then  the carrier of AB = the carrier of P by A50, XBOOLE_0:def_10;
then A73: P = AB by VECTSP_4:29;
 (FuncLatt f) . (a "/\" b) = (FuncLatt f) . (A1 /\ B1) by A6, A3, Th8;
hence  (FuncLatt f) . (a "/\" b) = ((FuncLatt f) . a) "/\" ((FuncLatt f) . b) by A9, A4, A7, A38, A35, A73, Th8; ::_thesis: verum
end;
 FuncLatt f is sup-Semilattice-Homomorphism of lattice A, lattice B by A1, Th12;
hence  ( (FuncLatt f) . (a "\/" b) = ((FuncLatt f) . a) "\/" ((FuncLatt f) . b) & (FuncLatt f) . (a "/\" b) = ((FuncLatt f) . a) "/\" ((FuncLatt f) . b) ) by A2, Def9; ::_thesis: verum
end;
hence  FuncLatt f is Homomorphism of lattice A, lattice B by LATTICE4:def_1; ::_thesis: verum
end;

theorem :: VECTSP_8:14
for F being Field
for A, B being strict VectSp of F
for f being Function of A,B st f is additive & f is homogeneous & f is one-to-one holds
FuncLatt f is one-to-one
proof
let F be Field; ::_thesis: for A, B being strict VectSp of F
for f being Function of A,B st f is additive & f is homogeneous & f is one-to-one holds
FuncLatt f is one-to-one
let A, B be strict VectSp of F; ::_thesis: for f being Function of A,B st f is additive & f is homogeneous & f is one-to-one holds
FuncLatt f is one-to-one
let f be Function of A,B; ::_thesis: ( f is additive & f is homogeneous & f is one-to-one implies FuncLatt f is one-to-one )
assume that
A1: ( f is additive & f is homogeneous ) and
A2: f is one-to-one ; ::_thesis: FuncLatt f is one-to-one
 for x1, x2 being set st x1 in dom (FuncLatt f) & x2 in dom (FuncLatt f) & (FuncLatt f) . x1 = (FuncLatt f) . x2 holds
x1 = x2
proof
let x1, x2 be set ; ::_thesis: ( x1 in dom (FuncLatt f) & x2 in dom (FuncLatt f) & (FuncLatt f) . x1 = (FuncLatt f) . x2 implies x1 = x2 )
assume that
A3: x1 in dom (FuncLatt f) and
A4: x2 in dom (FuncLatt f) and
A5: (FuncLatt f) . x1 = (FuncLatt f) . x2 ; ::_thesis: x1 = x2
consider X1 being strict Subspace of A such that
A6: X1 = x1 by A3, VECTSP_5:def_3;
A7: f .: the carrier of X1 is linearly-closed
proof
set BB = f .: the carrier of X1;
A8: for v, u being Element of B st v in f .: the carrier of X1 & u in f .: the carrier of X1 holds
v + u in f .: the carrier of X1
proof
let v, u be Element of B; ::_thesis: ( v in f .: the carrier of X1 & u in f .: the carrier of X1 implies v + u in f .: the carrier of X1 )
assume that
A9: v in f .: the carrier of X1 and
A10: u in f .: the carrier of X1 ; ::_thesis: v + u in f .: the carrier of X1
consider y being Element of A such that
A11: y in the carrier of X1 and
A12: u = f . y by A10, FUNCT_2:65;
A13: y in X1 by A11, STRUCT_0:def_5;
consider x being Element of A such that
A14: x in the carrier of X1 and
A15: v = f . x by A9, FUNCT_2:65;
 x in X1 by A14, STRUCT_0:def_5;
then  x + y in X1 by A13, VECTSP_4:20;
then  x + y in the carrier of X1 by STRUCT_0:def_5;
then  f . (x + y) in f .: the carrier of X1 by FUNCT_2:35;
hence  v + u in f .: the carrier of X1 by A1, A15, A12, VECTSP_1:def_20; ::_thesis: verum
end;
 for a being Element of F
for v being Element of B st v in f .: the carrier of X1 holds
a * v in f .: the carrier of X1
proof
let a be Element of F; ::_thesis: for v being Element of B st v in f .: the carrier of X1 holds
a * v in f .: the carrier of X1
let v be Element of B; ::_thesis: ( v in f .: the carrier of X1 implies a * v in f .: the carrier of X1 )
assume  v in f .: the carrier of X1 ; ::_thesis: a * v in f .: the carrier of X1
then consider x being Element of A such that
A16: x in the carrier of X1 and
A17: v = f . x by FUNCT_2:65;
 x in X1 by A16, STRUCT_0:def_5;
then  a * x in X1 by VECTSP_4:21;
then  a * x in the carrier of X1 by STRUCT_0:def_5;
then  f . (a * x) in f .: the carrier of X1 by FUNCT_2:35;
hence  a * v in f .: the carrier of X1 by A1, A17, MOD_2:def_2; ::_thesis: verum
end;
hence  f .: the carrier of X1 is linearly-closed by A8, VECTSP_4:def_1; ::_thesis: verum
end;
consider A1 being Subset of B such that
A18: A1 = f .: the carrier of X1 ;
 0. A in X1 by VECTSP_4:17;
then A19: 0. A in the carrier of X1 by STRUCT_0:def_5;
A20: dom f = the carrier of A by FUNCT_2:def_1;
 ex y being Element of B st y = f . (0. A) ;
then  f .: the carrier of X1 <> {} by A20, A19, FUNCT_1:def_6;
then A21: ex B1 being strict Subspace of B st the carrier of B1 = f .: the carrier of X1 by A7, VECTSP_4:34;
A22: (FuncLatt f) . X1 = Lin A1 by A18, Def7;
consider X2 being strict Subspace of A such that
A23: X2 = x2 by A4, VECTSP_5:def_3;
A24: f .: the carrier of X2 is linearly-closed
proof
set BB = f .: the carrier of X2;
A25: for v, u being Element of B st v in f .: the carrier of X2 & u in f .: the carrier of X2 holds
v + u in f .: the carrier of X2
proof
let v, u be Element of B; ::_thesis: ( v in f .: the carrier of X2 & u in f .: the carrier of X2 implies v + u in f .: the carrier of X2 )
assume that
A26: v in f .: the carrier of X2 and
A27: u in f .: the carrier of X2 ; ::_thesis: v + u in f .: the carrier of X2
consider y being Element of A such that
A28: y in the carrier of X2 and
A29: u = f . y by A27, FUNCT_2:65;
A30: y in X2 by A28, STRUCT_0:def_5;
consider x being Element of A such that
A31: x in the carrier of X2 and
A32: v = f . x by A26, FUNCT_2:65;
 x in X2 by A31, STRUCT_0:def_5;
then  x + y in X2 by A30, VECTSP_4:20;
then  x + y in the carrier of X2 by STRUCT_0:def_5;
then  f . (x + y) in f .: the carrier of X2 by FUNCT_2:35;
hence  v + u in f .: the carrier of X2 by A1, A32, A29, VECTSP_1:def_20; ::_thesis: verum
end;
 for a being Element of F
for v being Element of B st v in f .: the carrier of X2 holds
a * v in f .: the carrier of X2
proof
let a be Element of F; ::_thesis: for v being Element of B st v in f .: the carrier of X2 holds
a * v in f .: the carrier of X2
let v be Element of B; ::_thesis: ( v in f .: the carrier of X2 implies a * v in f .: the carrier of X2 )
assume  v in f .: the carrier of X2 ; ::_thesis: a * v in f .: the carrier of X2
then consider x being Element of A such that
A33: x in the carrier of X2 and
A34: v = f . x by FUNCT_2:65;
 x in X2 by A33, STRUCT_0:def_5;
then  a * x in X2 by VECTSP_4:21;
then  a * x in the carrier of X2 by STRUCT_0:def_5;
then  f . (a * x) in f .: the carrier of X2 by FUNCT_2:35;
hence  a * v in f .: the carrier of X2 by A1, A34, MOD_2:def_2; ::_thesis: verum
end;
hence  f .: the carrier of X2 is linearly-closed by A25, VECTSP_4:def_1; ::_thesis: verum
end;
consider A2 being Subset of B such that
A35: A2 = f .: the carrier of X2 ;
A36: (FuncLatt f) . X2 = Lin A2 by A35, Def7;
 0. A in X2 by VECTSP_4:17;
then A37: 0. A in the carrier of X2 by STRUCT_0:def_5;
 ex y being Element of B st y = f . (0. A) ;
then  f .: the carrier of X2 <> {} by A20, A37, FUNCT_1:def_6;
then consider B2 being strict Subspace of B such that
A38: the carrier of B2 = f .: the carrier of X2 by A24, VECTSP_4:34;
 Lin (f .: the carrier of X2) = B2 by A38, VECTSP_7:11;
then A39: f .: the carrier of X1 = f .: the carrier of X2 by A5, A6, A23, A18, A35, A22, A36, A21, A38, VECTSP_7:11;
 the carrier of X2 c= dom f by A20, VECTSP_4:def_2;
then A40: the carrier of X2 c= the carrier of X1 by A2, A39, FUNCT_1:87;
 the carrier of X1 c= dom f by A20, VECTSP_4:def_2;
then  the carrier of X1 c= the carrier of X2 by A2, A39, FUNCT_1:87;
then  the carrier of X1 = the carrier of X2 by A40, XBOOLE_0:def_10;
hence  x1 = x2 by A6, A23, VECTSP_4:29; ::_thesis: verum
end;
hence  FuncLatt f is one-to-one by FUNCT_1:def_4; ::_thesis: verum
end;

theorem :: VECTSP_8:15
for F being Field
for A being strict VectSp of F holds FuncLatt (id the carrier of A) = id the carrier of (lattice A)
proof
let F be Field; ::_thesis: for A being strict VectSp of F holds FuncLatt (id the carrier of A) = id the carrier of (lattice A)
let A be strict VectSp of F; ::_thesis: FuncLatt (id the carrier of A) = id the carrier of (lattice A)
set f = id the carrier of A;
A1: for x being set st x in the carrier of (lattice A) holds
(FuncLatt (id the carrier of A)) . x = x
proof
let x be set ; ::_thesis: ( x in the carrier of (lattice A) implies (FuncLatt (id the carrier of A)) . x = x )
assume  x in the carrier of (lattice A) ; ::_thesis: (FuncLatt (id the carrier of A)) . x = x
then consider X1 being strict Subspace of A such that
A2: X1 = x by VECTSP_5:def_3;
A3: the carrier of X1 c= (id the carrier of A) .: the carrier of X1
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in the carrier of X1 or z in (id the carrier of A) .: the carrier of X1 )
assume A4: z in the carrier of X1 ; ::_thesis: z in (id the carrier of A) .: the carrier of X1
 the carrier of X1 c= the carrier of A by VECTSP_4:def_2;
then reconsider z = z as Element of A by A4;
 (id the carrier of A) . z = z by FUNCT_1:17;
hence  z in (id the carrier of A) .: the carrier of X1 by A4, FUNCT_2:35; ::_thesis: verum
end;
A5: (FuncLatt (id the carrier of A)) . X1 = Lin ((id the carrier of A) .: the carrier of X1) by Def7;
 (id the carrier of A) .: the carrier of X1 c= the carrier of X1
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in (id the carrier of A) .: the carrier of X1 or z in the carrier of X1 )
assume A6: z in (id the carrier of A) .: the carrier of X1 ; ::_thesis: z in the carrier of X1
then reconsider z = z as Element of A ;
 ex Z being Element of A st
( Z in the carrier of X1 & z = (id the carrier of A) . Z ) by A6, FUNCT_2:65;
hence  z in the carrier of X1 by FUNCT_1:17; ::_thesis: verum
end;
then  (id the carrier of A) .: the carrier of X1 = the carrier of X1 by A3, XBOOLE_0:def_10;
hence  (FuncLatt (id the carrier of A)) . x = x by A2, A5, VECTSP_7:11; ::_thesis: verum
end;
 dom (FuncLatt (id the carrier of A)) = the carrier of (lattice A) by FUNCT_2:def_1;
hence  FuncLatt (id the carrier of A) = id the carrier of (lattice A) by A1, FUNCT_1:17; ::_thesis: verum
end;