let S be non empty complete continuous Poset; for A being set st A is_FreeGen_set_of S holds
for h' being CLHomomorphism of S,S st h' | A = id A holds
h' = id S
let A be set ; ( A is_FreeGen_set_of S implies for h' being CLHomomorphism of S,S st h' | A = id A holds
h' = id S )
assume A1:
A is_FreeGen_set_of S
; for h' being CLHomomorphism of S,S st h' | A = id A holds
h' = id S
set L = S;
A2:
A is Subset of
by A1, Th7;
then A3:
(id S) | A = id A
by FUNCT_3:1;
( dom (id A) = A & rng (id A) = A )
by RELAT_1:71;
then reconsider f = id A as Function of A,the carrier of S by A2, RELSET_1:11;
consider h being CLHomomorphism of S,S such that
h | A = f
and
A4:
for h' being CLHomomorphism of S,S st h' | A = f holds
h' = h
by A1, Def1;
A5:
id S is CLHomomorphism of S,S
by Th5;
let h' be CLHomomorphism of S,S; ( h' | A = id A implies h' = id S )
assume
h' | A = id A
; h' = id S
hence h' =
h
by A4
.=
id S
by A4, A5, A3
;
verum