vectsp_8.miz



    begin

    reserve F for Field;

    reserve VS for strict VectSp of F;

    definition

      let F, VS;

      :: VECTSP_8:def1

      func lattice VS -> strict bounded Lattice equals LattStr (# ( Subspaces VS), ( SubJoin VS), ( SubMeet VS) #);

      coherence by VECTSP_5: 60;

    end

    definition

      let F, VS;

      :: VECTSP_8:def2

      mode SubVS-Family of VS -> set means

      : Def2: for x be set st x in it holds x is Subspace of VS;

      existence

      proof

        take {} ;

        thus thesis;

      end;

    end

    registration

      let F, VS;

      cluster non empty for SubVS-Family of VS;

      existence

      proof

        set A = the Subspace of VS;

        for X be set st X in {A} holds X is Subspace of VS by TARSKI:def 1;

        then

        reconsider B = {A} as SubVS-Family of VS by Def2;

        take B;

        thus thesis;

      end;

    end

    definition

      let F, VS;

      :: original: Subspaces

      redefine

      func Subspaces (VS) -> non empty SubVS-Family of VS ;

      coherence

      proof

        ( Subspaces VS) is SubVS-Family of VS

        proof

          let x be set;

          assume x in ( Subspaces VS);

          then ex W be strict Subspace of VS st x = W by VECTSP_5:def 3;

          hence thesis;

        end;

        hence thesis;

      end;

      let X be non empty SubVS-Family of VS;

      :: original: Element

      redefine

      mode Element of X -> Subspace of VS ;

      coherence by Def2;

    end

    definition

      let F, VS;

      let x be Element of ( Subspaces VS);

      :: VECTSP_8:def3

      func carr (x) -> Subset of VS means

      : Def3: ex X be Subspace of VS st x = X & it = the carrier of X;

      existence

      proof

        reconsider A = the carrier of x as Subset of VS by VECTSP_4:def 2;

        consider X be Subspace of VS such that

         A1: X = x;

        take A, X;

        thus thesis by A1;

      end;

      uniqueness ;

    end

    reserve u,e for set;

    definition

      let F, VS;

      :: VECTSP_8:def4

      func carr VS -> Function of ( Subspaces VS), ( bool the carrier of VS) means

      : Def4: for h be Element of ( Subspaces VS), H be Subspace of VS st h = H holds (it . h) = the carrier of H;

      existence

      proof

        defpred P[ object, object] means for h be Element of ( Subspaces VS) st h = $1 holds $2 = the carrier of h;

        

         A1: for e be object st e in ( Subspaces VS) holds ex u be object st u in ( bool the carrier of VS) & P[e, u]

        proof

          let e be object;

          assume

           A2: e in ( Subspaces VS);

          then

          consider E be 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;

          ex X be Subspace of VS st u = X & u1 = the carrier of X by Def3;

          hence thesis by A3;

        end;

        consider f be Function of ( Subspaces VS), ( bool the carrier of VS) such that

         A4: for e be object st e in ( Subspaces VS) holds P[e, (f . e)] from FUNCT_2:sch 1( A1);

        take f;

        thus thesis by A4;

      end;

      uniqueness

      proof

        let F1,F2 be Function of ( Subspaces VS), ( bool the carrier of VS) such that

         A5: for h1 be Element of ( Subspaces VS), H1 be Subspace of VS st h1 = H1 holds (F1 . h1) = the carrier of H1 and

         A6: for h2 be Element of ( Subspaces VS), H2 be Subspace of VS st h2 = H2 holds (F2 . h2) = the carrier of H2;

        for h be object st h in ( Subspaces VS) holds (F1 . h) = (F2 . h)

        proof

          let h be object;

          assume

           A7: h in ( Subspaces VS);

          then h is Element of ( Subspaces VS);

          then

          consider H be Subspace of VS such that

           A8: H = h;

          (F1 . h) = the carrier of H by A5, A7, A8;

          hence thesis by A6, A7, A8;

        end;

        hence thesis by FUNCT_2: 12;

      end;

    end

    theorem :: VECTSP_8:1

    

     Th1: for VS be strict VectSp of F holds for H be non empty Subset of ( Subspaces VS) holds (( carr VS) .: H) is non empty

    proof

      let VS be strict VectSp of F;

      let H be non empty Subset of ( Subspaces VS);

      consider x be 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 thesis;

    end;

    theorem :: VECTSP_8:2

    for VS be strict VectSp of F holds for H be strict Subspace of VS holds ( 0. VS) in (( carr VS) . H)

    proof

      let VS be strict VectSp of F;

      let H be strict Subspace of VS;

      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 thesis by A1;

    end;

    reserve x for set;

    definition

      let F, VS;

      let G be non empty Subset of ( Subspaces VS);

      :: VECTSP_8:def5

      func meet G -> strict Subspace of VS means

      : Def5: the carrier of it = ( meet (( carr VS) .: G));

      existence

      proof

        reconsider cG = (( carr VS) .: G) as Subset-Family of VS;

        set C0 = ( meet cG);

        

         A1: for X be set st X in (( carr VS) .: G) holds ( 0. VS) in X

        proof

          let X be set;

          assume

           A2: X in (( carr VS) .: G);

          then

          reconsider X as Subset of VS;

          consider X1 be 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 thesis by A4, STRUCT_0:def 5;

        end;

        (( carr VS) .: G) <> {} by Th1;

        then

         A5: C0 <> {} by A1, SETFAM_1:def 1;

        reconsider C0 as Subset of VS;

        

         A6: for v,u be Element of VS st v in C0 & u in C0 holds (v + u) in C0

        proof

          let v,u be Element of VS such that

           A7: v in C0 and

           A8: u in C0;

          

           A9: for X be 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;

            reconsider vu = (v1 + u1) as Element of VS;

            assume

             A10: X in (( carr VS) .: G);

            then

             A11: v in X by A7, SETFAM_1:def 1;

            

             A12: u in X by A8, A10, SETFAM_1:def 1;

            reconsider X as Subset of VS by A10;

            consider X1 be 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 be 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 thesis by A14, A16, STRUCT_0:def 5;

          end;

          (( carr VS) .: G) <> {} by Th1;

          hence thesis by A9, SETFAM_1:def 1;

        end;

        for a be Element of F, v be Element of VS st v in C0 holds (a * v) in C0

        proof

          let a be Element of F;

          let v be Element of VS;

          assume

           A17: v in C0;

          

           A18: for X be set st X in (( carr VS) .: G) holds (a * v) in X

          proof

            reconsider v1 = v as Element of VS;

            let X be set;

            assume

             A19: X in (( carr VS) .: G);

            then

             A20: v in X by A17, SETFAM_1:def 1;

            reconsider X as Subset of VS by A19;

            consider X1 be 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 thesis by A22, STRUCT_0:def 5;

          end;

          (( carr VS) .: G) <> {} by Th1;

          hence thesis by A18, SETFAM_1:def 1;

        end;

        then C0 is linearly-closed by A6, VECTSP_4:def 1;

        hence thesis by A5, VECTSP_4: 34;

      end;

      uniqueness by VECTSP_4: 29;

    end

    theorem :: VECTSP_8:3

    ( Subspaces VS) = the carrier of ( lattice VS);

    theorem :: VECTSP_8:4

    the L_meet of ( lattice VS) = ( SubMeet VS);

    theorem :: VECTSP_8:5

    the L_join of ( lattice VS) = ( SubJoin VS);

    theorem :: VECTSP_8:6

    

     Th6: for VS be strict VectSp of F, p,q be Element of ( lattice VS), H1,H2 be strict Subspace of VS st p = H1 & q = H2 holds p [= q iff the carrier of H1 c= the carrier of H2

    proof

      let VS be strict VectSp of F;

      let p,q be Element of ( lattice VS);

      let H1,H2 be strict Subspace of VS;

      consider A1 be strict Subspace of VS such that

       A1: A1 = p by VECTSP_5:def 3;

      consider A2 be 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;

        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 thesis by A1, A4, LATTICES: 4;

      end;

      p [= q implies the carrier of A1 c= the carrier of A2

      proof

        assume p [= q;

        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 thesis by XBOOLE_1: 17;

      end;

      hence thesis by A1, A2, A3;

    end;

    theorem :: VECTSP_8:7

    

     Th7: for VS be strict VectSp of F, p,q be Element of ( lattice VS), H1,H2 be Subspace of VS st p = H1 & q = H2 holds (p "\/" q) = (H1 + H2)

    proof

      let VS be strict VectSp of F;

      let p,q be Element of ( lattice VS);

      let H1,H2 be Subspace of VS;

      consider H1 be strict Subspace of VS such that

       A1: H1 = p by VECTSP_5:def 3;

      consider H2 be 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 thesis by A1, A2;

    end;

    theorem :: VECTSP_8:8

    

     Th8: for VS be strict VectSp of F, p,q be Element of ( lattice VS), H1,H2 be Subspace of VS st p = H1 & q = H2 holds (p "/\" q) = (H1 /\ H2)

    proof

      let VS be strict VectSp of F;

      let p,q be Element of ( lattice VS);

      let H1,H2 be Subspace of VS;

      consider H1 be strict Subspace of VS such that

       A1: H1 = p by VECTSP_5:def 3;

      consider H2 be 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 thesis by A1, A2;

    end;

    definition

      let L be non empty LattStr;

      :: original: complete

      redefine

      :: VECTSP_8:def6

      attr L is complete means for X be Subset of L holds ex a be Element of L st a is_less_than X & for b be Element of L st b is_less_than X holds b [= a;

      compatibility

      proof

        hereby

          assume

           A1: L is complete;

          let X be Subset of L;

          set Y = { c where c be Element of L : c is_less_than X };

          consider p be Element of L such that

           A2: Y is_less_than p and

           A3: for r be Element of L st Y is_less_than r holds p [= r by A1;

          take p;

          thus p is_less_than X

          proof

            let q be Element of L;

            assume

             A4: q in X;

            Y is_less_than q

            proof

              let s be Element of L;

              assume s in Y;

              then ex t be Element of L st s = t & t is_less_than X;

              hence thesis by A4;

            end;

            hence thesis by A3;

          end;

          let b be Element of L;

          assume b is_less_than X;

          then b in Y;

          hence b [= p by A2;

        end;

        assume

         A5: for X be Subset of L holds ex a be Element of L st a is_less_than X & for b be Element of L st b is_less_than X holds b [= a;

        let X be set;

        defpred P[ Element of L] means X is_less_than $1;

        set Y = { c where c be Element of L : P[c] };

        Y is Subset of L from DOMAIN_1:sch 7;

        then

        consider p be Element of L such that

         A6: p is_less_than Y and

         A7: for r be Element of L st r is_less_than Y holds r [= p by A5;

        take p;

        thus X is_less_than p

        proof

          let q be Element of L;

          assume

           A8: q in X;

          q is_less_than Y

          proof

            let s be Element of L;

            assume s in Y;

            then ex t be Element of L st s = t & X is_less_than t;

            hence thesis by A8;

          end;

          hence thesis by A7;

        end;

        let r be Element of L;

        assume X is_less_than r;

        then r in Y;

        hence thesis by A6;

      end;

    end

    reserve Z1 for set;

    theorem :: VECTSP_8:9

    for VS holds ( lattice VS) is complete

    proof

      let VS;

      let Y be Subset of ( lattice VS);

      per cases ;

        suppose

         A1: Y = {} ;

        thus thesis

        proof

          take ( Top ( lattice VS));

          thus ( Top ( lattice VS)) is_less_than Y by A1;

          let b be Element of ( lattice VS);

          assume b is_less_than Y;

          thus thesis by LATTICES: 19;

        end;

      end;

        suppose Y <> {} ;

        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;

        set x = the Element of X;

        thus p is_less_than Y

        proof

          let q be Element of ( lattice VS);

          consider H be 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;

          (( 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;

        end;

        let r be Element of ( lattice VS);

        consider H be strict Subspace of VS such that

         A4: H = r by VECTSP_5:def 3;

        assume

         A5: r is_less_than Y;

        

         A6: for Z1 st Z1 in (( carr VS) .: X) holds the carrier of H c= Z1

        proof

          let Z1;

          assume

           A7: Z1 in (( carr VS) .: X);

          then

          reconsider Z2 = Z1 as Subset of VS;

          consider z1 be Element of ( Subspaces VS) such that

           A8: z1 in X and

           A9: Z2 = (( carr VS) . z1) by A7, FUNCT_2: 65;

          reconsider z1 as Element of ( lattice VS);

          

           A10: r [= z1 by A5, A8;

          consider z3 be strict Subspace of VS such that

           A11: z3 = z1 by VECTSP_5:def 3;

          Z1 = the carrier of z3 by A9, A11, Def4;

          hence thesis by A4, A11, A10, Th6;

        end;

        (( carr VS) . 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;

      end;

    end;

    theorem :: VECTSP_8:10

    

     Th10: for x be object holds for VS be strict VectSp of F holds for S be Subset of VS st S is non empty & S is linearly-closed holds x in ( Lin S) implies x in S

    proof

      let x be object, VS be strict VectSp of F, S be Subset of VS;

      assume S is non empty & S is linearly-closed;

      then

      consider W be strict Subspace of VS such that

       A1: S = the carrier of W by VECTSP_4: 34;

      assume

       A2: x in ( Lin S);

      ( Lin S) = W by A1, VECTSP_7: 11;

      hence thesis by A2, A1, STRUCT_0:def 5;

    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;

      :: VECTSP_8:def7

      func FuncLatt f -> Function of the carrier of ( lattice A), the carrier of ( lattice B) means

      : Def7: for S be strict Subspace of A, B0 be Subset of B st B0 = (f .: the carrier of S) holds (it . S) = ( Lin B0);

      existence

      proof

        defpred P[ object, object] means for S be Subspace of A st S = $1 holds $2 = ( Lin (f .: the carrier of S));

        

         A1: for x be object st x in the carrier of ( lattice A) holds ex y be object st y in the carrier of ( lattice B) & P[x, y]

        proof

          let x be object;

          assume x in the carrier of ( lattice A);

          then

          consider X be 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 be strict Subspace of B such that

           A3: Y = ( Lin y);

          take Y;

          thus thesis by A2, A3, VECTSP_5:def 3;

        end;

        consider f1 be Function of the carrier of ( lattice A), the carrier of ( lattice B) such that

         A4: for x be object st x in the carrier of ( lattice A) holds P[x, (f1 . x)] from FUNCT_2:sch 1( A1);

        take f1;

        thus thesis

        proof

          let S be strict Subspace of A;

          let B0 be Subset of B;

          

           A5: S is Element of ( Subspaces A) by VECTSP_5:def 3;

          assume B0 = (f .: the carrier of S);

          hence thesis by A4, A5;

        end;

      end;

      uniqueness

      proof

        let F1,F2 be Function of the carrier of ( lattice A), the carrier of ( lattice B) such that

         A6: for S be strict Subspace of A, B0 be Subset of B st B0 = (f .: the carrier of S) holds (F1 . S) = ( Lin B0) and

         A7: for S be strict Subspace of A, B0 be Subset of B st B0 = (f .: the carrier of S) holds (F2 . S) = ( Lin B0);

        for h be object st h in the carrier of ( lattice A) holds (F1 . h) = (F2 . h)

        proof

          let h be object;

          assume h in the carrier of ( lattice A);

          then

          consider S be 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 thesis by A7, A8;

        end;

        hence thesis by FUNCT_2: 12;

      end;

    end

    definition

      let L1,L2 be Lattice;

      mode Semilattice-Homomorphism of L1,L2 is "/\"-preserving Function of L1, L2;

      mode sup-Semilattice-Homomorphism of L1,L2 is "\/"-preserving Function of L1, L2;

    end

    theorem :: VECTSP_8:11

    for L1,L2 be Lattice holds for f be 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;

    theorem :: VECTSP_8:12

    

     Th12: for F be Field holds for A,B be strict VectSp of F holds for f be Function of A, B st f is additive homogeneous holds ( FuncLatt f) is sup-Semilattice-Homomorphism of ( lattice A), ( lattice B)

    proof

      let F be Field;

      let A,B be strict VectSp of F;

      let f be Function of A, B such that

       A1: f is additive homogeneous;

      ( FuncLatt f) is "\/"-preserving

      proof

        let a,b be Element of ( lattice A);

        (( FuncLatt f) . (a "\/" b)) = ((( FuncLatt f) . a) "\/" (( FuncLatt f) . b))

        proof

          reconsider b2 = (( FuncLatt f) . b) as Element of ( lattice B);

          consider B1 be 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 be 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 be Element of B st v in BB & u in BB holds (v + u) in BB

            proof

              let v,u be Element of B;

              assume that

               A8: v in BB and

               A9: u in BB;

              consider y be 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 be 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 BB by FUNCT_2: 35;

              hence thesis by A1, A14, A11, VECTSP_1:def 20;

            end;

            for a be Element of F, v be Element of B st v in BB holds (a * v) in BB

            proof

              let a be Element of F;

              let v be Element of B;

              assume v in BB;

              then

              consider x be 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 BB by FUNCT_2: 35;

              hence thesis by A1, A16, MOD_2:def 2;

            end;

            hence thesis by A7, VECTSP_4:def 1;

          end;

          

           A17: (f .: the carrier of B1) is linearly-closed

          proof

            set BB = (f .: the carrier of B1);

            

             A18: for v,u be Element of B st v in BB & u in BB holds (v + u) in BB

            proof

              let v,u be Element of B;

              assume that

               A19: v in BB and

               A20: u in BB;

              consider y be 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 be 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 BB by FUNCT_2: 35;

              hence thesis by A1, A25, A22, VECTSP_1:def 20;

            end;

            for a be Element of F, v be Element of B st v in BB holds (a * v) in BB

            proof

              let a be Element of F;

              let v be Element of B;

              assume v in BB;

              then

              consider x be 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 BB by FUNCT_2: 35;

              hence thesis by A1, A27, MOD_2:def 2;

            end;

            hence thesis by A18, VECTSP_4:def 1;

          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 be 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 be 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 be 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 be 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 object;

            

             A38: (f .: the carrier of A1) c= (f .: the carrier of (A1 + B1))

            proof

              let x be object;

              

               A39: the carrier of A1 c= the carrier of (A1 + B1)

              proof

                let x be object;

                assume

                 A40: x in the carrier of A1;

                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 as Element of A by A40;

                x in (A1 + B1) by A41, VECTSP_5: 2;

                hence thesis by STRUCT_0:def 5;

              end;

              assume

               A42: x in (f .: the carrier of A1);

              then

              reconsider x as Element of B;

              ex c be Element of A st c in the carrier of A1 & x = (f . c) by A42, FUNCT_2: 65;

              hence thesis by A39, FUNCT_2: 35;

            end;

            

             A43: (f .: the carrier of B1) c= (f .: the carrier of (A1 + B1))

            proof

              let x be object;

              

               A44: the carrier of B1 c= the carrier of (A1 + B1)

              proof

                let x be object;

                assume

                 A45: x in the carrier of 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 as Element of A by A45;

                x in (A1 + B1) by A46, VECTSP_5: 2;

                hence thesis by STRUCT_0:def 5;

              end;

              assume

               A47: x in (f .: the carrier of B1);

              then

              reconsider x as Element of B;

              ex c be Element of A st c in the carrier of B1 & x = (f . c) by A47, FUNCT_2: 65;

              hence thesis by A44, FUNCT_2: 35;

            end;

            assume x in the carrier of AB;

            then x in (A3 + B3) by STRUCT_0:def 5;

            then

            consider u,v be 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 thesis by STRUCT_0:def 5;

          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 be Element of B st v in BB & u in BB holds (v + u) in BB

            proof

              let v,u be Element of B;

              assume that

               A55: v in BB and

               A56: u in BB;

              consider y be 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 be 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 BB by FUNCT_2: 35;

              hence thesis by A1, A61, A58, VECTSP_1:def 20;

            end;

            for a be Element of F, v be Element of B st v in BB holds (a * v) in BB

            proof

              let a be Element of F;

              let v be Element of B;

              assume v in BB;

              then

              consider x be 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 BB by FUNCT_2: 35;

              hence thesis by A1, A63, MOD_2:def 2;

            end;

            hence thesis by A54, VECTSP_4:def 1;

          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 object;

              assume x in the carrier of (A3 + B3);

              then x in (A3 + B3) by STRUCT_0:def 5;

              then

              consider vb,ub be 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 be 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 be 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 thesis by A1, A67, A72, A69, VECTSP_1:def 20;

            end;

            let x be object;

            assume x in the carrier of P;

            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 object;

              assume

               A74: x in (f .: the carrier of (A1 + B1));

              then

              reconsider x as Element of B;

              consider c be 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 be 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 thesis by A52, A34, STRUCT_0:def 5;

            end;

            then (f .: the carrier of (A1 + B1)) = the carrier of (A3 + B3) by A64, XBOOLE_0:def 10;

            hence thesis by A53, A73, Th10;

          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 thesis by A30, A3, A28, A52, A34, A82, Th7;

        end;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: VECTSP_8:13

    for F be Field holds for A,B be strict VectSp of F holds for f be Function of A, B st f is one-to-one additive homogeneous holds ( FuncLatt f) is Homomorphism of ( lattice A), ( lattice B)

    proof

      let F be Field, A,B be strict VectSp of F, f be Function of A, B such that

       A1: f is one-to-one additive homogeneous;

      for a,b be 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);

        

         A2: (( FuncLatt f) . (a "/\" b)) = ((( FuncLatt f) . a) "/\" (( FuncLatt f) . b))

        proof

          reconsider b2 = (( FuncLatt f) . b) as Element of ( lattice B);

          consider B1 be 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 be 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 be Element of B st v in BB & u in BB holds (v + u) in BB

            proof

              let v,u be Element of B;

              assume that

               A13: v in BB and

               A14: u in BB;

              consider y be 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 be 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 BB by FUNCT_2: 35;

              hence thesis by A1, A19, A16, VECTSP_1:def 20;

            end;

            for a be Element of F, v be Element of B st v in BB holds (a * v) in BB

            proof

              let a be Element of F;

              let v be Element of B;

              assume v in BB;

              then

              consider x be 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 BB by FUNCT_2: 35;

              hence thesis by A1, A21, MOD_2:def 2;

            end;

            hence thesis by A12, VECTSP_4:def 1;

          end;

          

           A22: (f .: the carrier of A1) is linearly-closed

          proof

            set BB = (f .: the carrier of A1);

            

             A23: for v,u be Element of B st v in BB & u in BB holds (v + u) in BB

            proof

              let v,u be Element of B;

              assume that

               A24: v in BB and

               A25: u in BB;

              consider y be 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 be 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 BB by FUNCT_2: 35;

              hence thesis by A1, A30, A27, VECTSP_1:def 20;

            end;

            for a be Element of F, v be Element of B st v in BB holds (a * v) in BB

            proof

              let a be Element of F;

              let v be Element of B;

              assume v in BB;

              then

              consider x be 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 BB by FUNCT_2: 35;

              hence thesis by A1, A32, MOD_2:def 2;

            end;

            hence thesis by A23, VECTSP_4:def 1;

          end;

          ex y1 be 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 be 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 be 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 be 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 be Element of B st v in BB & u in BB holds (v + u) in BB

            proof

              let v,u be Element of B;

              assume that

               A41: v in BB and

               A42: u in BB;

              consider y be 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 be 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 BB by FUNCT_2: 35;

              hence thesis by A1, A47, A44, VECTSP_1:def 20;

            end;

            for a be Element of F, v be Element of B st v in BB holds (a * v) in BB

            proof

              let a be Element of F;

              let v be Element of B;

              assume v in BB;

              then

              consider x be 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 BB by FUNCT_2: 35;

              hence thesis by A1, A49, MOD_2:def 2;

            end;

            hence thesis by A40, VECTSP_4:def 1;

          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 object;

              assume x in the carrier of (A3 /\ B3);

              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 as Element of B;

              consider xa be 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 be 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 thesis by A55, FUNCT_2: 35;

            end;

            let x be object;

            assume x in the carrier of P;

            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 object;

              assume

               A61: x in (f .: the carrier of (A1 /\ B1));

              then

              reconsider x as Element of B;

              consider c be 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 thesis by A38, A35, STRUCT_0:def 5;

            end;

            then (f .: the carrier of (A1 /\ B1)) = the carrier of (A3 /\ B3) by A51, XBOOLE_0:def 10;

            hence thesis by A39, A60, Th10;

          end;

          the carrier of AB c= the carrier of P

          proof

            let x be object;

            assume x in the carrier of AB;

            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 be 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 be 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 thesis by STRUCT_0:def 5;

          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 thesis by A9, A4, A7, A38, A35, A73, Th8;

        end;

        ( FuncLatt f) is sup-Semilattice-Homomorphism of ( lattice A), ( lattice B) by A1, Th12;

        hence thesis by A2, LATTICE4:def 1;

      end;

      then ( FuncLatt f) is "\/"-preserving "/\"-preserving;

      hence thesis;

    end;

    theorem :: VECTSP_8:14

    for A,B be strict VectSp of F holds for f be Function of A, B st f is additive homogeneous & f is one-to-one holds ( FuncLatt f) is one-to-one

    proof

      let A,B be strict VectSp of F;

      let f be Function of A, B such that

       A1: f is additive homogeneous and

       A2: f is one-to-one;

      for x1,x2 be object 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 object;

        assume that

         A3: x1 in ( dom ( FuncLatt f)) and

         A4: x2 in ( dom ( FuncLatt f)) and

         A5: (( FuncLatt f) . x1) = (( FuncLatt f) . x2);

        consider X1 be 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 be Element of B st v in BB & u in BB holds (v + u) in BB

          proof

            let v,u be Element of B;

            assume that

             A9: v in BB and

             A10: u in BB;

            consider y be 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 be 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 BB by FUNCT_2: 35;

            hence thesis by A1, A15, A12, VECTSP_1:def 20;

          end;

          for a be Element of F, v be Element of B st v in BB holds (a * v) in BB

          proof

            let a be Element of F;

            let v be Element of B;

            assume v in BB;

            then

            consider x be 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 BB by FUNCT_2: 35;

            hence thesis by A1, A17, MOD_2:def 2;

          end;

          hence thesis by A8, VECTSP_4:def 1;

        end;

        consider A1 be 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 be 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 be 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 be 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 be Element of B st v in BB & u in BB holds (v + u) in BB

          proof

            let v,u be Element of B;

            assume that

             A26: v in BB and

             A27: u in BB;

            consider y be 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 be 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 BB by FUNCT_2: 35;

            hence thesis by A1, A32, A29, VECTSP_1:def 20;

          end;

          for a be Element of F, v be Element of B st v in BB holds (a * v) in BB

          proof

            let a be Element of F;

            let v be Element of B;

            assume v in BB;

            then

            consider x be 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 BB by FUNCT_2: 35;

            hence thesis by A1, A34, MOD_2:def 2;

          end;

          hence thesis by A25, VECTSP_4:def 1;

        end;

        consider A2 be 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 be Element of B st y = (f . ( 0. A));

        then (f .: the carrier of X2) <> {} by A20, A37, FUNCT_1:def 6;

        then

        consider B2 be 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 thesis by A6, A23, VECTSP_4: 29;

      end;

      hence thesis by FUNCT_1:def 4;

    end;

    theorem :: VECTSP_8:15

    for A be strict VectSp of F holds ( FuncLatt ( id the carrier of A)) = ( id the carrier of ( lattice A))

    proof

      let A be strict VectSp of F;

      set f = ( id the carrier of A);

      

       A1: for x be object st x in the carrier of ( lattice A) holds (( FuncLatt f) . x) = x

      proof

        let x be object;

        assume x in the carrier of ( lattice A);

        then

        consider X1 be strict Subspace of A such that

         A2: X1 = x by VECTSP_5:def 3;

        

         A3: the carrier of X1 c= (f .: the carrier of X1)

        proof

          let z be object;

          assume

           A4: z in the carrier of X1;

          the carrier of X1 c= the carrier of A by VECTSP_4:def 2;

          then

          reconsider z as Element of A by A4;

          (f . z) = z;

          hence thesis by A4, FUNCT_2: 35;

        end;

        

         A5: (( FuncLatt f) . X1) = ( Lin (f .: the carrier of X1)) by Def7;

        (f .: the carrier of X1) c= the carrier of X1

        proof

          let z be object;

          assume

           A6: z in (f .: the carrier of X1);

          then

          reconsider z as Element of A;

          ex Z be Element of A st Z in the carrier of X1 & z = (f . Z) by A6, FUNCT_2: 65;

          hence thesis;

        end;

        then (f .: the carrier of X1) = the carrier of X1 by A3, XBOOLE_0:def 10;

        hence thesis by A2, A5, VECTSP_7: 11;

      end;

      ( dom ( FuncLatt f)) = the carrier of ( lattice A) by FUNCT_2:def 1;

      hence thesis by A1, FUNCT_1: 17;

    end;