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

hence FuncLatt F = id the carrier of (UnSubAlLattice U0) by A2, FUNCT_1:17; :: thesis: verum

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

dom (FuncLatt F) = the carrier of (UnSubAlLattice U0)
by FUNCT_2:def 1;
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

for a1 being object st a1 in F .: the carrier of a holds

a1 in 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;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

then A4:
the carrier of a c= F .: the carrier of a
;
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;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

for a1 being object st a1 in F .: the carrier of a holds

a1 in the carrier of a

proof

then A6:
F .: the carrier of a c= the carrier of a
;
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;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

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

hence FuncLatt F = id the carrier of (UnSubAlLattice U0) by A2, FUNCT_1:17; :: thesis: verum