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₁[ Ordinal] means a [= (f,$1) +. a;
deffunc H₁( Ordinal) -> Element of L = (f,$1) +. a;

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

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
A2: O1 <> 0 and
A3: O1 is limit_ordinal and
A4: for O2 being Ordinal st O2 in O1 holds
S₁[O2] ; :: thesis: S₁[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₁[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₁(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₁[O1] by A2, A3, A7, Th17; :: thesis: verum

end;

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

A9: 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 . a [= f . ((f,O1) +. a) by QUANTAL1:def 12;
then a [= f . ((f,O1) +. a) by A8, LATTICES:7;
hence S₁[ succ O1] by Th15; :: thesis: verum

end;

A10: S₁[ 0 ] by Th13;
thus for O being Ordinal holds S₁[O] from ORDINAL2:sch 1(A10, A9, A1); :: thesis: verum