let A be non empty set ; for L being lower-bounded LATTICE
for O being Ordinal
for d being BiFunction of A,L
for q being QuadrSeq of d holds d c= ConsecutiveDelta (q,O)
let L be lower-bounded LATTICE; for O being Ordinal
for d being BiFunction of A,L
for q being QuadrSeq of d holds d c= ConsecutiveDelta (q,O)
let O be Ordinal; for d being BiFunction of A,L
for q being QuadrSeq of d holds d c= ConsecutiveDelta (q,O)
let d be BiFunction of A,L; for q being QuadrSeq of d holds d c= ConsecutiveDelta (q,O)
let q be QuadrSeq of d; d c= ConsecutiveDelta (q,O)
defpred S1[ Ordinal] means d c= ConsecutiveDelta (q,$1);
A1:
for O2 being Ordinal st O2 <> 0 & O2 is limit_ordinal & ( for O1 being Ordinal st O1 in O2 holds
S1[O1] ) holds
S1[O2]
proof
deffunc H1(
Ordinal)
-> BiFunction of
(ConsecutiveSet (A,$1)),
L =
ConsecutiveDelta (
q,$1);
let O2 be
Ordinal;
( O2 <> 0 & O2 is limit_ordinal & ( for O1 being Ordinal st O1 in O2 holds
S1[O1] ) implies S1[O2] )
assume that A2:
O2 <> 0
and A3:
O2 is
limit_ordinal
and
for
O1 being
Ordinal st
O1 in O2 holds
d c= ConsecutiveDelta (
q,
O1)
;
S1[O2]
A4:
{} in O2
by A2, ORDINAL3:8;
consider Ls being
Sequence such that A5:
(
dom Ls = O2 & ( for
O1 being
Ordinal st
O1 in O2 holds
Ls . O1 = H1(
O1) ) )
from ORDINAL2:sch 2();
Ls . {} =
ConsecutiveDelta (
q,
{})
by A2, A5, ORDINAL3:8
.=
d
by Th26
;
then A6:
d in rng Ls
by A5, A4, FUNCT_1:def 3;
ConsecutiveDelta (
q,
O2)
= union (rng Ls)
by A2, A3, A5, Th28;
hence
S1[
O2]
by A6, ZFMISC_1:74;
verum
end;
A7:
for O1 being Ordinal st S1[O1] holds
S1[ succ O1]
proof
let O1 be
Ordinal;
( S1[O1] implies S1[ succ O1] )
ConsecutiveDelta (
q,
(succ O1)) =
new_bi_fun (
(BiFun ((ConsecutiveDelta (q,O1)),(ConsecutiveSet (A,O1)),L)),
(Quadr (q,O1)))
by Th27
.=
new_bi_fun (
(ConsecutiveDelta (q,O1)),
(Quadr (q,O1)))
by Def15
;
then A8:
ConsecutiveDelta (
q,
O1)
c= ConsecutiveDelta (
q,
(succ O1))
by Th19;
assume
d c= ConsecutiveDelta (
q,
O1)
;
S1[ succ O1]
hence
S1[
succ O1]
by A8, XBOOLE_1:1;
verum
end;
A9:
S1[ 0 ]
by Th26;
for O being Ordinal holds S1[O]
from ORDINAL2:sch 1(A9, A7, A1);
hence
d c= ConsecutiveDelta (q,O)
; verum