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 object st x in the carrier of (lattice A) holds
(FuncLatt (id the carrier of A)) . x = x

proof

let x be object ; :: 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 object ; :: 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 ;
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 object ; :: 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 ; :: 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