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 O1, O2 being Ordinal st O1 c= O2 holds

(f,O1) +. a [= (f,O2) +. a

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

for O1, O2 being Ordinal st O1 c= O2 holds

(f,O1) +. a [= (f,O2) +. a

let a be Element of L; :: thesis: ( a [= f . a implies for O1, O2 being Ordinal st O1 c= O2 holds

(f,O1) +. a [= (f,O2) +. a )

defpred S_{1}[ Ordinal] means for O1, O2 being Ordinal st O1 c= O2 & O2 c= $1 holds

(f,O1) +. a [= (f,O2) +. a;

(f,O1) +. a [= (f,O2) +. a

assume A29: O1 c= O2 ; :: thesis: (f,O1) +. a [= (f,O2) +. a

A30: S_{1}[ 0 ]
;

for O4 being Ordinal holds S_{1}[O4]
from ORDINAL2:sch 1(A30, A13, A1);

hence (f,O1) +. a [= (f,O2) +. a by A29; :: thesis: verum

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

for O1, O2 being Ordinal st O1 c= O2 holds

(f,O1) +. a [= (f,O2) +. a

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

for O1, O2 being Ordinal st O1 c= O2 holds

(f,O1) +. a [= (f,O2) +. a

let a be Element of L; :: thesis: ( a [= f . a implies for O1, O2 being Ordinal st O1 c= O2 holds

(f,O1) +. a [= (f,O2) +. a )

defpred S

(f,O1) +. a [= (f,O2) +. a;

A1: now :: thesis: for O4 being Ordinal st O4 <> 0 & O4 is limit_ordinal & ( for O3 being Ordinal st O3 in O4 holds

S_{1}[O3] ) holds

S_{1}[O4]

assume A12:
a [= f . a
; :: thesis: for O1, O2 being Ordinal st O1 c= O2 holds S

S

let O4 be Ordinal; :: thesis: ( O4 <> 0 & O4 is limit_ordinal & ( for O3 being Ordinal st O3 in O4 holds

S_{1}[O3] ) implies S_{1}[O4] )

assume that

A2: ( O4 <> 0 & O4 is limit_ordinal ) and

A3: for O3 being Ordinal st O3 in O4 holds

S_{1}[O3]
; :: thesis: S_{1}[O4]

thus S_{1}[O4]
:: thesis: verum

end;S

assume that

A2: ( O4 <> 0 & O4 is limit_ordinal ) and

A3: for O3 being Ordinal st O3 in O4 holds

S

thus S

proof

let O1, O2 be Ordinal; :: thesis: ( O1 c= O2 & O2 c= O4 implies (f,O1) +. a [= (f,O2) +. a )

assume that

A4: O1 c= O2 and

A5: O2 c= O4 ; :: thesis: (f,O1) +. a [= (f,O2) +. a

A6: ( O2 c< O4 iff ( O2 c= O4 & O2 <> O4 ) ) ;

A7: ( O1 c< O2 iff ( O1 c= O2 & O1 <> O2 ) ) ;

end;assume that

A4: O1 c= O2 and

A5: O2 c= O4 ; :: thesis: (f,O1) +. a [= (f,O2) +. a

A6: ( O2 c< O4 iff ( O2 c= O4 & O2 <> O4 ) ) ;

A7: ( O1 c< O2 iff ( O1 c= O2 & O1 <> O2 ) ) ;

per cases
( O2 = O4 or O2 in O4 )
by A5, A6, ORDINAL1:11;

end;

suppose A8:
O2 = O4
; :: thesis: (f,O1) +. a [= (f,O2) +. a

thus
(f,O1) +. a [= (f,O2) +. a
:: thesis: verum

end;proof
end;

per cases
( O1 = O2 or O1 in O2 )
by A4, A7, ORDINAL1:11;

end;

suppose A9:
O1 in O2
; :: thesis: (f,O1) +. a [= (f,O2) +. a

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

consider L1 being Sequence such that

A10: ( dom L1 = O2 & ( for O3 being Ordinal st O3 in O2 holds

L1 . O3 = H_{1}(O3) ) )
from ORDINAL2:sch 2();

A11: ( L1 . O1 = (f,O1) +. a & L1 . O1 in rng L1 ) by A9, A10, FUNCT_1:def 3;

(f,O2) +. a = "\/" ((rng L1),L) by A2, A8, A10, Th17;

hence (f,O1) +. a [= (f,O2) +. a by A11, LATTICE3:38; :: thesis: verum

end;consider L1 being Sequence such that

A10: ( dom L1 = O2 & ( for O3 being Ordinal st O3 in O2 holds

L1 . O3 = H

A11: ( L1 . O1 = (f,O1) +. a & L1 . O1 in rng L1 ) by A9, A10, FUNCT_1:def 3;

(f,O2) +. a = "\/" ((rng L1),L) by A2, A8, A10, Th17;

hence (f,O1) +. a [= (f,O2) +. a by A11, LATTICE3:38; :: thesis: verum

(f,O1) +. a [= (f,O2) +. a

A13: now :: thesis: for O4 being Ordinal st S_{1}[O4] holds

S_{1}[ succ O4]

let O1, O2 be Ordinal; :: thesis: ( O1 c= O2 implies (f,O1) +. a [= (f,O2) +. a )S

let O4 be Ordinal; :: thesis: ( S_{1}[O4] implies S_{1}[ succ O4] )

assume A14: S_{1}[O4]
; :: thesis: S_{1}[ succ O4]

thus S_{1}[ succ O4]
:: thesis: verum

end;assume A14: S

thus S

proof

let O1, O2 be Ordinal; :: thesis: ( O1 c= O2 & O2 c= succ O4 implies (f,O1) +. a [= (f,O2) +. a )

assume that

A15: O1 c= O2 and

A16: O2 c= succ O4 ; :: thesis: (f,O1) +. a [= (f,O2) +. a

end;assume that

A15: O1 c= O2 and

A16: O2 c= succ O4 ; :: thesis: (f,O1) +. a [= (f,O2) +. a

per cases
( ( O1 = O2 & O2 <> succ O4 ) or ( O1 <> O2 & O2 <> succ O4 ) or ( O1 = O2 & O2 = succ O4 ) or ( O1 <> O2 & O2 = succ O4 ) )
;

end;

suppose
( O1 <> O2 & O2 <> succ O4 )
; :: thesis: (f,O1) +. a [= (f,O2) +. a

then
O2 c< succ O4
by A16;

then O2 in succ O4 by ORDINAL1:11;

then O2 c= O4 by ORDINAL1:22;

hence (f,O1) +. a [= (f,O2) +. a by A14, A15; :: thesis: verum

end;then O2 in succ O4 by ORDINAL1:11;

then O2 c= O4 by ORDINAL1:22;

hence (f,O1) +. a [= (f,O2) +. a by A14, A15; :: thesis: verum

suppose A17:
( O1 <> O2 & O2 = succ O4 )
; :: thesis: (f,O1) +. a [= (f,O2) +. a

A18:
(f,O4) +. a [= (f,(succ O4)) +. a

then O1 in O2 by ORDINAL1:11;

then O1 c= O4 by A17, ORDINAL1:22;

then (f,O1) +. a [= (f,O4) +. a by A14;

hence (f,O1) +. a [= (f,O2) +. a by A17, A18, LATTICES:7; :: thesis: verum

end;proof
end;

O1 c< O2
by A15, A17;per cases
( O4 is limit_ordinal or ex O3 being Ordinal st O4 = succ O3 )
by ORDINAL1:29;

end;

suppose A19:
O4 is limit_ordinal
; :: thesis: (f,O4) +. a [= (f,(succ O4)) +. a

thus
(f,O4) +. a [= (f,(succ O4)) +. a
:: thesis: verum

end;proof
end;

per cases
( O4 = {} or O4 <> {} )
;

end;

suppose A20:
O4 <> {}
; :: thesis: (f,O4) +. a [= (f,(succ O4)) +. a

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

consider L1 being Sequence such that

A21: ( dom L1 = O4 & ( for O3 being Ordinal st O3 in O4 holds

L1 . O3 = H_{1}(O3) ) )
from ORDINAL2:sch 2();

A22: rng L1 is_less_than (f,(succ O4)) +. a

hence (f,O4) +. a [= (f,(succ O4)) +. a by A22, LATTICE3:def 21; :: thesis: verum

end;consider L1 being Sequence such that

A21: ( dom L1 = O4 & ( for O3 being Ordinal st O3 in O4 holds

L1 . O3 = H

A22: rng L1 is_less_than (f,(succ O4)) +. a

proof

(f,O4) +. a = "\/" ((rng L1),L)
by A19, A20, A21, Th17;
let q be Element of L; :: according to LATTICE3:def 17 :: thesis: ( not q in rng L1 or q [= (f,(succ O4)) +. a )

assume q in rng L1 ; :: thesis: q [= (f,(succ O4)) +. a

then consider O3 being object such that

A23: O3 in dom L1 and

A24: q = L1 . O3 by FUNCT_1:def 3;

reconsider O3 = O3 as Ordinal by A23;

O3 in succ O3 by ORDINAL1:6;

then A25: O3 c= succ O3 by ORDINAL1:def 2;

O3 c= O4 by A21, A23, ORDINAL1:def 2;

then (f,O3) +. a [= (f,O4) +. a by A14;

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

then (f,(succ O3)) +. a [= f . ((f,O4) +. a) by Th15;

then A26: (f,(succ O3)) +. a [= (f,(succ O4)) +. a by Th15;

succ O3 c= O4 by A21, A23, ORDINAL1:21;

then A27: (f,O3) +. a [= (f,(succ O3)) +. a by A14, A25;

q = (f,O3) +. a by A21, A23, A24;

hence q [= (f,(succ O4)) +. a by A26, A27, LATTICES:7; :: thesis: verum

end;assume q in rng L1 ; :: thesis: q [= (f,(succ O4)) +. a

then consider O3 being object such that

A23: O3 in dom L1 and

A24: q = L1 . O3 by FUNCT_1:def 3;

reconsider O3 = O3 as Ordinal by A23;

O3 in succ O3 by ORDINAL1:6;

then A25: O3 c= succ O3 by ORDINAL1:def 2;

O3 c= O4 by A21, A23, ORDINAL1:def 2;

then (f,O3) +. a [= (f,O4) +. a by A14;

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

then (f,(succ O3)) +. a [= f . ((f,O4) +. a) by Th15;

then A26: (f,(succ O3)) +. a [= (f,(succ O4)) +. a by Th15;

succ O3 c= O4 by A21, A23, ORDINAL1:21;

then A27: (f,O3) +. a [= (f,(succ O3)) +. a by A14, A25;

q = (f,O3) +. a by A21, A23, A24;

hence q [= (f,(succ O4)) +. a by A26, A27, LATTICES:7; :: thesis: verum

hence (f,O4) +. a [= (f,(succ O4)) +. a by A22, LATTICE3:def 21; :: thesis: verum

suppose
ex O3 being Ordinal st O4 = succ O3
; :: thesis: (f,O4) +. a [= (f,(succ O4)) +. a

then consider O3 being Ordinal such that

A28: O4 = succ O3 ;

O3 c= O4 by A28, XBOOLE_1:7;

then (f,O3) +. a [= (f,O4) +. a by A14;

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

then (f,O4) +. a [= f . ((f,O4) +. a) by A28, Th15;

hence (f,O4) +. a [= (f,(succ O4)) +. a by Th15; :: thesis: verum

end;A28: O4 = succ O3 ;

O3 c= O4 by A28, XBOOLE_1:7;

then (f,O3) +. a [= (f,O4) +. a by A14;

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

then (f,O4) +. a [= f . ((f,O4) +. a) by A28, Th15;

hence (f,O4) +. a [= (f,(succ O4)) +. a by Th15; :: thesis: verum

then O1 in O2 by ORDINAL1:11;

then O1 c= O4 by A17, ORDINAL1:22;

then (f,O1) +. a [= (f,O4) +. a by A14;

hence (f,O1) +. a [= (f,O2) +. a by A17, A18, LATTICES:7; :: thesis: verum

assume A29: O1 c= O2 ; :: thesis: (f,O1) +. a [= (f,O2) +. a

A30: S

for O4 being Ordinal holds S

hence (f,O1) +. a [= (f,O2) +. a by A29; :: thesis: verum