let O1 be Ordinal; :: thesis: for L being complete Lattice
for f being monotone UnOp of L
for a being Element of L st f . a [= a & (f,O1) -. a is_a_fixpoint_of f holds
for O2 being Ordinal st O1 c= O2 holds
(f,O1) -. a = (f,O2) -. a
let L be complete Lattice; :: thesis: for f being monotone UnOp of L
for a being Element of L st f . a [= a & (f,O1) -. a is_a_fixpoint_of f holds
for O2 being Ordinal st O1 c= O2 holds
(f,O1) -. a = (f,O2) -. a
let f be monotone UnOp of L; :: thesis: for a being Element of L st f . a [= a & (f,O1) -. a is_a_fixpoint_of f holds
for O2 being Ordinal st O1 c= O2 holds
(f,O1) -. a = (f,O2) -. a
let a be Element of L; :: thesis: ( f . a [= a & (f,O1) -. a is_a_fixpoint_of f implies for O2 being Ordinal st O1 c= O2 holds
(f,O1) -. a = (f,O2) -. a )
assume that
A1: f . a [= a and
A2: (f,O1) -. a is_a_fixpoint_of f ; :: thesis: for O2 being Ordinal st O1 c= O2 holds
(f,O1) -. a = (f,O2) -. a
set fa = (f,O1) -. a;
defpred S₁[ Ordinal] means ( O1 c= $1 implies (f,O1) -. a = (f,$1) -. a );

A3: now :: thesis: for O2 being Ordinal st O2 <> 0 & O2 is limit_ordinal & ( for O3 being Ordinal st O3 in O2 holds
S₁[O3] ) holds
S₁[O2]

let O2 be Ordinal; :: thesis: ( O2 <> 0 & O2 is limit_ordinal & ( for O3 being Ordinal st O3 in O2 holds
S₁[O3] ) implies S₁[O2] )
assume that
A4: ( O2 <> 0 & O2 is limit_ordinal ) and
A5: for O3 being Ordinal st O3 in O2 holds
S₁[O3] ; :: thesis: S₁[O2]
thus S₁[O2] :: thesis: verum

proof

assume O1 c= O2 ; :: thesis: (f,O1) -. a = (f,O2) -. a
then A6: (f,O2) -. a [= (f,O1) -. a by A1, Th25;
deffunc H₁( Ordinal) -> Element of L = (f,$1) -. a;
consider L1 being Sequence such that
A7: ( dom L1 = O2 & ( for O3 being Ordinal st O3 in O2 holds
L1 . O3 = H₁(O3) ) ) from ORDINAL2:sch 2();
A8: (f,O1) -. a is_less_than rng L1

proof

let q be Element of L; :: according to LATTICE3:def 16 :: thesis: ( not q in rng L1 or (f,O1) -. a [= q )
assume q in rng L1 ; :: thesis: (f,O1) -. a [= q
then consider O3 being object such that
A9: O3 in dom L1 and
A10: q = L1 . O3 by FUNCT_1:def 3;
reconsider O3 = O3 as Ordinal by A9;

per cases ( O1 c= O3 or O3 c= O1 ) ;

suppose O1 c= O3 ; :: thesis: (f,O1) -. a [= q

then (f,O1) -. a [= (f,O3) -. a by A5, A7, A9;
hence (f,O1) -. a [= q by A7, A9, A10; :: thesis: verum

end;

suppose O3 c= O1 ; :: thesis: (f,O1) -. a [= q

then (f,O1) -. a [= (f,O3) -. a by A1, Th25;
hence (f,O1) -. a [= q by A7, A9, A10; :: thesis: verum

end;

end;

end;

(f,O2) -. a = "/\" ((rng L1),L) by A4, A7, Th18;
then (f,O1) -. a [= (f,O2) -. a by A8, LATTICE3:39;
hence (f,O1) -. a = (f,O2) -. a by A6, LATTICES:8; :: thesis: verum

end;

end;

A11: now :: thesis: for O2 being Ordinal st S₁[O2] holds
S₁[ succ O2]

let O2 be Ordinal; :: thesis: ( S₁[O2] implies S₁[ succ O2] )
assume A12: S₁[O2] ; :: thesis: S₁[ succ O2]
thus S₁[ succ O2] :: thesis: verum

proof

assume A13: O1 c= succ O2 ; :: thesis: (f,O1) -. a = (f,(succ O2)) -. a

per cases ( O1 = succ O2 or O1 <> succ O2 ) ;

suppose O1 = succ O2 ; :: thesis: (f,O1) -. a = (f,(succ O2)) -. a

hence (f,O1) -. a = (f,(succ O2)) -. a ; :: thesis: verum

end;

suppose O1 <> succ O2 ; :: thesis: (f,O1) -. a = (f,(succ O2)) -. a

then O1 c< succ O2 by A13;
then O1 in succ O2 by ORDINAL1:11;
hence (f,O1) -. a = f . ((f,O2) -. a) by A2, A12, ORDINAL1:22
.= (f,(succ O2)) -. a by Th16 ;
:: thesis: verum

end;

end;

end;

end;

A14: S₁[ 0 ] ;
thus for O2 being Ordinal holds S₁[O2] from ORDINAL2:sch 1(A14, A11, A3); :: thesis: verum