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 )
assume A1: f . a [= a ; :: thesis: for O being Ordinal holds f,O -. a [= a
defpred S₁[ Ordinal] means f,$1 -. a [= a;
A2: S₁[ {} ] by Th17;

A3: now

let O1 be Ordinal; :: thesis: ( S₁[O1] implies S₁[ succ O1] )
assume S₁[O1] ; :: thesis: S₁[ succ O1]
then f . (f,O1 -. a) [= f . a by QUANTAL1:def 12;
then f . (f,O1 -. a) [= a by A1, LATTICES:25;
hence S₁[ succ O1] by Th19; :: thesis: verum

end;

deffunc H₁( Ordinal) -> Element of L = f,$1 -. a;

A4: now

let O1 be Ordinal; :: thesis: ( O1 <> {} & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
S₁[O2] ) implies S₁[O1] )
assume A5: ( O1 <> {} & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
S₁[O2] ) ) ; :: thesis: S₁[O1]
consider Ls being T-Sequence such that
A6: ( dom Ls = O1 & ( for O2 being Ordinal st O2 in O1 holds
Ls . O2 = H₁(O2) ) ) from ORDINAL2:sch 2();
consider O2 being set such that
A7: O2 in O1 by A5, XBOOLE_0:def 1;
reconsider O2 = O2 as Ordinal by A7;
A8: Ls . O2 = f,O2 -. a by A6, A7;
Ls . O2 in rng Ls by A6, A7, FUNCT_1:def 5;
then A9: "/\" (rng Ls),L [= f,O2 -. a by A8, LATTICE3:38;
S₁[O2] by A5, A7;
then "/\" (rng Ls),L [= a by A9, LATTICES:25;
hence S₁[O1] by A5, A6, Th21; :: thesis: verum

end;

thus for O being Ordinal holds S₁[O] from ORDINAL2:sch 1(A2, A3, A4); :: thesis: verum