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

A4: now :: thesis: for O1 being Ordinal st S₁[O1] holds
S₁[ succ O1]

let O1 be Ordinal; :: thesis: ( S₁[O1] implies S₁[ succ O1] )
assume S₁[O1] ; :: thesis: S₁[ succ O1]
then f . ((f,O1) +. a) [= f . b by QUANTAL1:def 12;
hence S₁[ succ O1] by A3, Th15; :: thesis: verum

end;

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

deffunc H₁( Ordinal) -> Element of L = (f,$1) +. a;
let O1 be Ordinal; :: thesis: ( O1 <> 0 & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
S₁[O2] ) implies S₁[O1] )
assume that
A6: ( O1 <> 0 & O1 is limit_ordinal ) and
A7: for O2 being Ordinal st O2 in O1 holds
S₁[O2] ; :: thesis: S₁[O1]
consider L1 being Sequence such that
A8: ( dom L1 = O1 & ( for O3 being Ordinal st O3 in O1 holds
L1 . O3 = H₁(O3) ) ) from ORDINAL2:sch 2();
A9: rng L1 is_less_than b

proof

let q be Element of L; :: according to LATTICE3:def 17 :: thesis: ( not q in rng L1 or q [= b )
assume q in rng L1 ; :: thesis: q [= b
then consider O3 being object such that
A10: O3 in dom L1 and
A11: q = L1 . O3 by FUNCT_1:def 3;
reconsider O3 = O3 as Ordinal by A10;
(f,O3) +. a [= b by A7, A8, A10;
hence q [= b by A8, A10, A11; :: thesis: verum

end;

(f,O1) +. a = "\/" ((rng L1),L) by A6, A8, Th17;
hence S₁[O1] by A9, LATTICE3:def 21; :: thesis: verum

end;

A12: S₁[ 0 ] by A1, Th13;
thus for O2 being Ordinal holds S₁[O2] from ORDINAL2:sch 1(A12, A4, A5); :: thesis: verum