let L be complete Lattice; 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; 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; ( f . a [= a implies for O being Ordinal holds (f,O) -. a [= a )
defpred S1[ Ordinal] means (f,$1) -. a [= a;
deffunc H1( Ordinal) -> Element of L = (f,$1) -. a;
A1:
now for O1 being Ordinal st O1 <> 0 & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
S1[O2] ) holds
S1[O1]let O1 be
Ordinal;
( O1 <> 0 & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
S1[O2] ) implies S1[O1] )assume that A2:
O1 <> 0
and A3:
O1 is
limit_ordinal
and A4:
for
O2 being
Ordinal st
O2 in O1 holds
S1[
O2]
;
S1[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:
S1[
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 = H1(
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
S1[
O1]
by A2, A3, A7, Th18;
verum end;
assume A8:
f . a [= a
; for O being Ordinal holds (f,O) -. a [= a
A10:
S1[ 0 ]
by Th14;
thus
for O being Ordinal holds S1[O]
from ORDINAL2:sch 1(A10, A9, A1); verum