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: dom (FuncLatt (id the carrier of A)) = the carrier of (lattice A) by FUNCT_2:def 1;
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: (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 = the carrier of X1

proof

thus (id the carrier of A) .: the carrier of X1 c= the carrier of X1 :: according to XBOOLE_0:def 10 :: thesis: 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 (id the carrier of A) .: the carrier of X1 or z in the carrier of X1 )
assume A4: 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 ;
consider Z being Element of A such that
A5: ( Z in the carrier of X1 & z = (id the carrier of A) . Z ) by A4, FUNCT_2:116;
thus z in the carrier of X1 by A5, FUNCT_1:34; :: thesis: verum

end;

thus the carrier of X1 c= (id the carrier of A) .: the carrier of X1 :: thesis: verum

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 A6: 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 A6;
(id the carrier of A) . z = z by FUNCT_1:34;
hence z in (id the carrier of A) .: the carrier of X1 by A6, FUNCT_2:43; :: thesis: verum

end;

end;

hence (FuncLatt (id the carrier of A)) . x = x by A2, A3, VECTSP_7:16; :: thesis: verum

end;

hence FuncLatt (id the carrier of A) = id the carrier of (lattice A) by A1, FUNCT_1:34; :: thesis: verum