let F be Field; :: thesis: for A being strict VectSp of F holds FuncLatt (id the carrier of A) = id the carrier of ()
let A be strict VectSp of F; :: thesis: FuncLatt (id the carrier of A) = id the carrier of ()
set f = id the carrier of A;
A1: for x being object st x in the carrier of () holds
(FuncLatt (id the carrier of A)) . x = x
proof
let x be object ; :: thesis: ( x in the carrier of () implies (FuncLatt (id the carrier of A)) . x = x )
assume x in the carrier of () ; :: 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 ; :: 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 ;
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 ;
hence (FuncLatt (id the carrier of A)) . x = x by ; :: thesis: verum
end;
dom (FuncLatt (id the carrier of A)) = the carrier of () by FUNCT_2:def 1;
hence FuncLatt (id the carrier of A) = id the carrier of () by ; :: thesis: verum