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

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