let S be non empty complete continuous Poset; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( h9 | A = id A implies h9 = id S )
assume h9 | A = id A ; :: thesis: h9 = id S
hence h9 = h by A4
.= id S by A4, A5, A3 ;
:: thesis: verum