let U0 be strict with_const_op Universal_Algebra; :: thesis: for F being Function of the carrier of U0, the carrier of U0 st F = id the carrier of U0 holds
FuncLatt F = id the carrier of (UnSubAlLattice U0)
let F be Function of the carrier of U0, the carrier of U0; :: thesis: ( F = id the carrier of U0 implies FuncLatt F = id the carrier of (UnSubAlLattice U0) )
assume A1: F = id the carrier of U0 ; :: thesis: FuncLatt F = id the carrier of (UnSubAlLattice U0)
A2: for a being object st a in the carrier of (UnSubAlLattice U0) holds
(FuncLatt F) . a = a
proof
let a be object ; :: thesis: ( a in the carrier of (UnSubAlLattice U0) implies (FuncLatt F) . a = a )
assume a in the carrier of (UnSubAlLattice U0) ; :: thesis: (FuncLatt F) . a = a
then reconsider a = a as strict SubAlgebra of U0 by UNIALG_2:def 14;
for a1 being object st a1 in the carrier of a holds
a1 in F .: the carrier of a
proof
let a1 be object ; :: thesis: ( a1 in the carrier of a implies a1 in F .: the carrier of a )
assume A3: a1 in the carrier of a ; :: thesis: a1 in F .: the carrier of a
the carrier of a c= the carrier of U0 by Th3;
then reconsider a1 = a1 as Element of U0 by A3;
F . a1 = a1 by A1, FUNCT_1:17;
hence a1 in F .: the carrier of a by A3, FUNCT_2:35; :: thesis: verum
end;
then A4: the carrier of a c= F .: the carrier of a ;
for a1 being object st a1 in F .: the carrier of a holds
a1 in the carrier of a
proof
let a1 be object ; :: thesis: ( a1 in F .: the carrier of a implies a1 in the carrier of a )
assume A5: a1 in F .: the carrier of a ; :: thesis: a1 in the carrier of a
then reconsider a1 = a1 as Element of U0 ;
ex H being Element of U0 st
( H in the carrier of a & a1 = F . H ) by A5, FUNCT_2:65;
hence a1 in the carrier of a by A1, FUNCT_1:17; :: thesis: verum
end;
then A6: F .: the carrier of a c= the carrier of a ;
then reconsider H1 = the carrier of a as Subset of U0 by A4, XBOOLE_0:def 10;
F .: the carrier of a = the carrier of a by A6, A4;
then (FuncLatt F) . a = GenUnivAlg H1 by Def6;
hence (FuncLatt F) . a = a by UNIALG_2:19; :: thesis: verum
end;
dom (FuncLatt F) = the carrier of (UnSubAlLattice U0) by FUNCT_2:def 1;
hence FuncLatt F = id the carrier of (UnSubAlLattice U0) by A2, FUNCT_1:17; :: thesis: verum