let L be complete Lattice; :: thesis: for f being monotone UnOp of L

for a being Element of L st f . a [= a holds

for O being Ordinal holds (f,O) -. a [= a

let f be monotone UnOp of L; :: thesis: for a being Element of L st f . a [= a holds

for O being Ordinal holds (f,O) -. a [= a

let a be Element of L; :: thesis: ( f . a [= a implies for O being Ordinal holds (f,O) -. a [= a )

defpred S_{1}[ Ordinal] means (f,$1) -. a [= a;

deffunc H_{1}( Ordinal) -> Element of L = (f,$1) -. a;

_{1}[ 0 ]
by Th14;

thus for O being Ordinal holds S_{1}[O]
from ORDINAL2:sch 1(A10, A9, A1); :: thesis: verum

for a being Element of L st f . a [= a holds

for O being Ordinal holds (f,O) -. a [= a

let f be monotone UnOp of L; :: thesis: for a being Element of L st f . a [= a holds

for O being Ordinal holds (f,O) -. a [= a

let a be Element of L; :: thesis: ( f . a [= a implies for O being Ordinal holds (f,O) -. a [= a )

defpred S

deffunc H

A1: 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]

assume A8:
f . a [= a
; :: thesis: for O being Ordinal holds (f,O) -. a [= aS

S

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

A2: O1 <> 0 and

A3: O1 is limit_ordinal and

A4: for O2 being Ordinal st O2 in O1 holds

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

consider O2 being object such that

A5: O2 in O1 by A2, XBOOLE_0:def 1;

reconsider O2 = O2 as Ordinal by A5;

A6: S_{1}[O2]
by A4, A5;

consider Ls being Sequence such that

A7: ( dom Ls = O1 & ( for O2 being Ordinal st O2 in O1 holds

Ls . O2 = H_{1}(O2) ) )
from ORDINAL2:sch 2();

( Ls . O2 = (f,O2) -. a & Ls . O2 in rng Ls ) by A7, A5, FUNCT_1:def 3;

then "/\" ((rng Ls),L) [= (f,O2) -. a by LATTICE3:38;

then "/\" ((rng Ls),L) [= a by A6, LATTICES:7;

hence S_{1}[O1]
by A2, A3, A7, Th18; :: thesis: verum

end;S

assume that

A2: O1 <> 0 and

A3: O1 is limit_ordinal and

A4: for O2 being Ordinal st O2 in O1 holds

S

consider O2 being object such that

A5: O2 in O1 by A2, XBOOLE_0:def 1;

reconsider O2 = O2 as Ordinal by A5;

A6: S

consider Ls being Sequence such that

A7: ( dom Ls = O1 & ( for O2 being Ordinal st O2 in O1 holds

Ls . O2 = H

( Ls . O2 = (f,O2) -. a & Ls . O2 in rng Ls ) by A7, A5, FUNCT_1:def 3;

then "/\" ((rng Ls),L) [= (f,O2) -. a by LATTICE3:38;

then "/\" ((rng Ls),L) [= a by A6, LATTICES:7;

hence S

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

S_{1}[ succ O1]

A10:
SS

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 . a by QUANTAL1:def 12;

then f . ((f,O1) -. a) [= a by A8, LATTICES:7;

hence S_{1}[ succ O1]
by Th16; :: thesis: verum

end;assume S

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

then f . ((f,O1) -. a) [= a by A8, LATTICES:7;

hence S

thus for O being Ordinal holds S