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