let L be complete Lattice; :: thesis:
let f be monotone UnOp of L; :: thesis:
let a be Element of L; :: thesis:
set cL = the carrier of L;
set ccL = card the carrier of L;
set nccL = nextcard (card the carrier of L);
deffunc H₁( Ordinal) -> Element of L = (f,$1) -. a;
consider Ls being Sequence such that
A1: ( dom Ls = nextcard (card the carrier of L) & ( for O2 being Ordinal st O2 in nextcard (card the carrier of L) holds
Ls . O2 = H₁(O2) ) ) from ORDINAL2:sch 2();
assume A2: f . a [= a ; :: thesis:

now :: thesis:

assume A3: for O being Ordinal st O in nextcard (card the carrier of L) holds
not (f,O) -. a is_a_fixpoint_of f ; :: thesis:
A4: Ls is one-to-one

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A5: x1 in dom Ls and
A6: x2 in dom Ls and
A7: Ls . x1 = Ls . x2 ; :: thesis:
reconsider x1 = x1, x2 = x2 as Ordinal by A5, A6;
A8: Ls . x1 = (f,x1) -. a by A1, A5;
A9: Ls . x2 = (f,x2) -. a by A1, A6;

per cases by Lm1;

suppose A10: x1 c< x2 ; :: thesis:

not (f,x2) -. a is_a_fixpoint_of f by A1, A3, A6;
hence x1 = x2 by A2, A1, A6, A7, A8, A10, Th27; :: thesis:

end;

suppose A11: x2 c< x1 ; :: thesis:

not (f,x1) -. a is_a_fixpoint_of f by A1, A3, A5;
hence x1 = x2 by A2, A1, A5, A7, A9, A11, Th27; :: thesis:

end;

suppose x2 = x1 ; :: thesis:

hence x1 = x2 ; :: thesis:

end;

end;

end;

rng Ls c= the carrier of L

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng Ls ; :: thesis:
then consider x being object such that
A12: x in dom Ls and
A13: Ls . x = y by FUNCT_1:def 3;
reconsider x = x as Ordinal by A12;
Ls . x = (f,x) -. a by A1, A12;
hence y in the carrier of L by A13; :: thesis:

end;

then card (nextcard (card the carrier of L)) c= card the carrier of L by A1, A4, CARD_1:10;
then A14: nextcard (card the carrier of L) c= card the carrier of L ;
card the carrier of L in nextcard (card the carrier of L) by CARD_1:18;
hence contradiction by A14, CARD_1:4; :: thesis:

end;

then consider O being Ordinal such that
A15: O in nextcard (card the carrier of L) and
A16: (f,O) -. a is_a_fixpoint_of f ;
take O ; :: thesis:
card O in nextcard (card the carrier of L) by A15, CARD_1:9;
hence card O c= card the carrier of L by CARD_3:91; :: thesis:
thus (f,O) -. a is_a_fixpoint_of f by A16; :: thesis: