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

let O2 be Ordinal; :: thesis: ( O2 <> {} & O2 is limit_ordinal & ( for O3 being Ordinal st O3 in O2 holds
S₁[O3] ) implies S₁[O2] )
assume that
A4: ( O2 <> {} & 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, Th28;
deffunc H₁( Ordinal) -> Element of L = f,$1 -. a;
consider L1 being T-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 set such that
A9: O3 in dom L1 and
A10: q = L1 . O3 by FUNCT_1:def 5;
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, Th28;
hence f,O1 -. a [= q by A7, A9, A10; :: thesis: verum

end;

end;

end;

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

end;

end;

A11: now

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, XBOOLE_0:def 8;
then O1 in succ O2 by ORDINAL1:21;
hence f,O1 -. a = f . (f,O2 -. a) by A2, A12, ABIAN:def 3, ORDINAL1:34
.= f,(succ O2) -. a by Th19 ;
:: thesis: verum

end;

end;

end;

end;

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