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

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 () )
assume A1: F = id the carrier of U0 ; :: thesis: FuncLatt F = id the carrier of ()
A2: for a being object st a in the carrier of () holds
() . a = a
proof
let a be object ; :: thesis: ( a in the carrier of () implies () . a = a )
assume a in the carrier of () ; :: thesis: () . 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 ;
hence a1 in F .: the carrier of a by ; :: 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 ;
hence a1 in the carrier of a by ; :: 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 ;
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 () = the carrier of () by FUNCT_2:def 1;
hence FuncLatt F = id the carrier of () by ; :: thesis: verum