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

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

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

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

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

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

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

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

_{1}[ 0 ]
by Th13;

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 a [= f . a holds

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

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

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

let a be Element of L; :: thesis: ( a [= f . a implies for O being Ordinal holds a [= (f,O) +. 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:
a [= f . a
; :: thesis: for O being Ordinal holds a [= (f,O) +. 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 (f,O2) +. a [= "\/" ((rng Ls),L) by LATTICE3:38;

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

hence S_{1}[O1]
by A2, A3, A7, Th17; :: 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 (f,O2) +. a [= "\/" ((rng Ls),L) by LATTICE3:38;

then a [= "\/" ((rng Ls),L) 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 . a [= f . ((f,O1) +. a) by QUANTAL1:def 12;

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

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

end;assume S

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

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

hence S

thus for O being Ordinal holds S