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_{1}[ Ordinal] means (f,$1) +. a [= b;

A3: f . b = b by A2;

_{1}[ 0 ]
by A1, Th13;

thus for O2 being Ordinal holds S_{1}[O2]
from ORDINAL2:sch 1(A12, A4, A5); :: thesis: verum

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

A3: f . b = b by A2;

A4: now :: thesis: for O1 being Ordinal st S_{1}[O1] holds

S_{1}[ succ O1]

S

let O1 be Ordinal; :: thesis: ( S_{1}[O1] implies S_{1}[ succ O1] )

assume S_{1}[O1]
; :: thesis: S_{1}[ succ O1]

then f . ((f,O1) +. a) [= f . b by QUANTAL1:def 12;

hence S_{1}[ succ O1]
by A3, Th15; :: thesis: verum

end;assume S

then f . ((f,O1) +. a) [= f . b by QUANTAL1:def 12;

hence S

A5: now :: thesis: for O1 being Ordinal st O1 <> 0 & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds

S_{1}[O2] ) holds

S_{1}[O1]

A12:
SS

S

deffunc H_{1}( 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_{1}[O2] ) implies S_{1}[O1] )

assume that

A6: ( O1 <> 0 & O1 is limit_ordinal ) and

A7: for O2 being Ordinal st O2 in O1 holds

S_{1}[O2]
; :: thesis: S_{1}[O1]

consider L1 being Sequence such that

A8: ( dom L1 = O1 & ( for O3 being Ordinal st O3 in O1 holds

L1 . O3 = H_{1}(O3) ) )
from ORDINAL2:sch 2();

A9: rng L1 is_less_than b

hence S_{1}[O1]
by A9, LATTICE3:def 21; :: thesis: verum

end;let O1 be Ordinal; :: thesis: ( O1 <> 0 & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds

S

assume that

A6: ( O1 <> 0 & O1 is limit_ordinal ) and

A7: for O2 being Ordinal st O2 in O1 holds

S

consider L1 being Sequence such that

A8: ( dom L1 = O1 & ( for O3 being Ordinal st O3 in O1 holds

L1 . O3 = H

A9: rng L1 is_less_than b

proof

(f,O1) +. a = "\/" ((rng L1),L)
by A6, A8, Th17;
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;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

hence S

thus for O2 being Ordinal holds S