let A be non empty set ; for L being lower-bounded LATTICE
for d being BiFunction of A,L st d is zeroed holds
for q being QuadrSeq of d
for O being Ordinal holds ConsecutiveDelta2 (q,O) is zeroed
let L be lower-bounded LATTICE; for d being BiFunction of A,L st d is zeroed holds
for q being QuadrSeq of d
for O being Ordinal holds ConsecutiveDelta2 (q,O) is zeroed
let d be BiFunction of A,L; ( d is zeroed implies for q being QuadrSeq of d
for O being Ordinal holds ConsecutiveDelta2 (q,O) is zeroed )
assume A1:
d is zeroed
; for q being QuadrSeq of d
for O being Ordinal holds ConsecutiveDelta2 (q,O) is zeroed
let q be QuadrSeq of d; for O being Ordinal holds ConsecutiveDelta2 (q,O) is zeroed
let O be Ordinal; ConsecutiveDelta2 (q,O) is zeroed
defpred S1[ Ordinal] means ConsecutiveDelta2 (q,$1) is zeroed ;
A2:
for O1 being Ordinal st S1[O1] holds
S1[ succ O1]
proof
let O1 be
Ordinal;
( S1[O1] implies S1[ succ O1] )
assume
ConsecutiveDelta2 (
q,
O1) is
zeroed
;
S1[ succ O1]
then A3:
new_bi_fun2 (
(ConsecutiveDelta2 (q,O1)),
(Quadr2 (q,O1))) is
zeroed
by Th10;
let z be
Element of
ConsecutiveSet2 (
A,
(succ O1));
LATTICE5:def 6 (ConsecutiveDelta2 (q,(succ O1))) . (z,z) = Bottom L
reconsider z9 =
z as
Element of
new_set2 (ConsecutiveSet2 (A,O1)) by Th15;
ConsecutiveDelta2 (
q,
(succ O1)) =
new_bi_fun2 (
(BiFun ((ConsecutiveDelta2 (q,O1)),(ConsecutiveSet2 (A,O1)),L)),
(Quadr2 (q,O1)))
by Th19
.=
new_bi_fun2 (
(ConsecutiveDelta2 (q,O1)),
(Quadr2 (q,O1)))
by LATTICE5:def 15
;
hence (ConsecutiveDelta2 (q,(succ O1))) . (
z,
z) =
(new_bi_fun2 ((ConsecutiveDelta2 (q,O1)),(Quadr2 (q,O1)))) . (
z9,
z9)
.=
Bottom L
by A3
;
verum
end;
A4:
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]
proof
deffunc H1(
Ordinal)
-> BiFunction of
(ConsecutiveSet2 (A,$1)),
L =
ConsecutiveDelta2 (
q,$1);
let O2 be
Ordinal;
( O2 <> 0 & O2 is limit_ordinal & ( for O2 being Ordinal st O2 in O2 holds
S1[O2] ) implies S1[O2] )
assume that A5:
(
O2 <> 0 &
O2 is
limit_ordinal )
and A6:
for
O1 being
Ordinal st
O1 in O2 holds
ConsecutiveDelta2 (
q,
O1) is
zeroed
;
S1[O2]
set CS =
ConsecutiveSet2 (
A,
O2);
consider Ls being
Sequence such that A7:
(
dom Ls = O2 & ( for
O1 being
Ordinal st
O1 in O2 holds
Ls . O1 = H1(
O1) ) )
from ORDINAL2:sch 2();
ConsecutiveDelta2 (
q,
O2)
= union (rng Ls)
by A5, A7, Th20;
then reconsider f =
union (rng Ls) as
BiFunction of
(ConsecutiveSet2 (A,O2)),
L ;
deffunc H2(
Ordinal)
-> set =
ConsecutiveSet2 (
A,$1);
consider Ts being
Sequence such that A8:
(
dom Ts = O2 & ( for
O1 being
Ordinal st
O1 in O2 holds
Ts . O1 = H2(
O1) ) )
from ORDINAL2:sch 2();
A9:
ConsecutiveSet2 (
A,
O2)
= union (rng Ts)
by A5, A8, Th16;
f is
zeroed
proof
let x be
Element of
ConsecutiveSet2 (
A,
O2);
LATTICE5:def 6 f . (x,x) = Bottom L
consider y being
set such that A10:
x in y
and A11:
y in rng Ts
by A9, TARSKI:def 4;
consider o being
object such that A12:
o in dom Ts
and A13:
y = Ts . o
by A11, FUNCT_1:def 3;
reconsider o =
o as
Ordinal by A12;
A14:
Ls . o = ConsecutiveDelta2 (
q,
o)
by A7, A8, A12;
then reconsider h =
Ls . o as
BiFunction of
(ConsecutiveSet2 (A,o)),
L ;
reconsider x9 =
x as
Element of
ConsecutiveSet2 (
A,
o)
by A8, A10, A12, A13;
A15:
dom h = [:(ConsecutiveSet2 (A,o)),(ConsecutiveSet2 (A,o)):]
by FUNCT_2:def 1;
A16:
h is
zeroed
proof
let z be
Element of
ConsecutiveSet2 (
A,
o);
LATTICE5:def 6 h . (z,z) = Bottom L
A17:
ConsecutiveDelta2 (
q,
o) is
zeroed
by A6, A8, A12;
thus h . (
z,
z) =
(ConsecutiveDelta2 (q,o)) . (
z,
z)
by A7, A8, A12
.=
Bottom L
by A17
;
verum
end;
ConsecutiveDelta2 (
q,
o)
in rng Ls
by A7, A8, A12, A14, FUNCT_1:def 3;
then A18:
h c= f
by A14, ZFMISC_1:74;
x in ConsecutiveSet2 (
A,
o)
by A8, A10, A12, A13;
then
[x,x] in dom h
by A15, ZFMISC_1:87;
hence f . (
x,
x) =
h . (
x9,
x9)
by A18, GRFUNC_1:2
.=
Bottom L
by A16
;
verum
end;
hence
S1[
O2]
by A5, A7, Th20;
verum
end;
A19:
S1[ 0 ]
for O being Ordinal holds S1[O]
from ORDINAL2:sch 1(A19, A2, A4);
hence
ConsecutiveDelta2 (q,O) is zeroed
; verum