let S be non empty complete continuous Poset; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: for h' being CLHomomorphism of S,S st h' | A = id A holds
h' = id S
set L = S;
A2: A is Subset of S by A1, Th7;
( 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, FUNCT_2:def 1, RELSET_1:11;
consider h being CLHomomorphism of S,S such that
h | A = f and
A3: for h' being CLHomomorphism of S,S st h' | A = f holds
h' = h by A1, Def1;
let h' be CLHomomorphism of S,S; :: thesis: ( h' | A = id A implies h' = id S )
assume A4: h' | A = id A ; :: thesis: h' = id S
A5: id S is CLHomomorphism of S,S by Th5;
A6: (id S) | A = id A by A2, FUNCT_3:1;
thus h' = h by A3, A4
.= id S by A3, A5, A6 ; :: thesis: verum