let A be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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
; :: thesis: for q being QuadrSeq of d
for O being Ordinal holds ConsecutiveDelta2 q,O is zeroed
let q be QuadrSeq of d; :: thesis: for O being Ordinal holds ConsecutiveDelta2 q,O is zeroed
let O be Ordinal; :: thesis: ConsecutiveDelta2 q,O is zeroed
defpred S1[ Ordinal] means ConsecutiveDelta2 q,$1 is zeroed ;
A2:
S1[ {} ]
A3:
for O1 being Ordinal st S1[O1] holds
S1[ succ O1]
proof
let O1 be
Ordinal;
:: thesis: ( S1[O1] implies S1[ succ O1] )
assume
ConsecutiveDelta2 q,
O1 is
zeroed
;
:: thesis: S1[ succ O1]
then A4:
new_bi_fun2 (ConsecutiveDelta2 q,O1),
(Quadr2 q,O1) is
zeroed
by Th10;
let z be
Element of
ConsecutiveSet2 A,
(succ O1);
:: according to LATTICE5:def 7 :: thesis: (ConsecutiveDelta2 q,(succ O1)) . z,z = Bottom L
reconsider z' =
z as
Element of
new_set2 (ConsecutiveSet2 A,O1) by Th16;
ConsecutiveDelta2 q,
(succ O1) =
new_bi_fun2 (BiFun (ConsecutiveDelta2 q,O1),(ConsecutiveSet2 A,O1),L),
(Quadr2 q,O1)
by Th20
.=
new_bi_fun2 (ConsecutiveDelta2 q,O1),
(Quadr2 q,O1)
by LATTICE5:def 16
;
hence (ConsecutiveDelta2 q,(succ O1)) . z,
z =
(new_bi_fun2 (ConsecutiveDelta2 q,O1),(Quadr2 q,O1)) . z',
z'
.=
Bottom L
by A4, LATTICE5:def 7
;
:: thesis: verum
end;
A5:
for O1 being Ordinal st O1 <> {} & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
S1[O2] ) holds
S1[O1]
proof
let O2 be
Ordinal;
:: thesis: ( O2 <> {} & O2 is limit_ordinal & ( for O2 being Ordinal st O2 in O2 holds
S1[O2] ) implies S1[O2] )
assume A6:
(
O2 <> {} &
O2 is
limit_ordinal & ( for
O1 being
Ordinal st
O1 in O2 holds
ConsecutiveDelta2 q,
O1 is
zeroed ) )
;
:: thesis: S1[O2]
deffunc H1(
Ordinal)
-> BiFunction of
(ConsecutiveSet2 A,$1),
L =
ConsecutiveDelta2 q,$1;
consider Ls being
T-Sequence such that A7:
(
dom Ls = O2 & ( for
O1 being
Ordinal st
O1 in O2 holds
Ls . O1 = H1(
O1) ) )
from ORDINAL2:sch 2();
A8:
ConsecutiveDelta2 q,
O2 = union (rng Ls)
by A6, A7, Th21;
deffunc H2(
Ordinal)
-> set =
ConsecutiveSet2 A,$1;
consider Ts being
T-Sequence such that A9:
(
dom Ts = O2 & ( for
O1 being
Ordinal st
O1 in O2 holds
Ts . O1 = H2(
O1) ) )
from ORDINAL2:sch 2();
A10:
ConsecutiveSet2 A,
O2 = union (rng Ts)
by A6, A9, Th17;
set CS =
ConsecutiveSet2 A,
O2;
reconsider f =
union (rng Ls) as
BiFunction of
(ConsecutiveSet2 A,O2),
L by A8;
f is
zeroed
proof
let x be
Element of
ConsecutiveSet2 A,
O2;
:: according to LATTICE5:def 7 :: thesis: f . x,x = Bottom L
consider y being
set such that A11:
(
x in y &
y in rng Ts )
by A10, TARSKI:def 4;
consider o being
set such that A12:
(
o in dom Ts &
y = Ts . o )
by A11, FUNCT_1:def 5;
reconsider o =
o as
Ordinal by A12;
A13:
x in ConsecutiveSet2 A,
o
by A9, A11, A12;
A14:
Ls . o = ConsecutiveDelta2 q,
o
by A7, A9, A12;
then reconsider h =
Ls . o as
BiFunction of
(ConsecutiveSet2 A,o),
L ;
A15:
h is
zeroed
proof
let z be
Element of
ConsecutiveSet2 A,
o;
:: according to LATTICE5:def 7 :: thesis: h . z,z = Bottom L
A16:
ConsecutiveDelta2 q,
o is
zeroed
by A6, A9, A12;
thus h . z,
z =
(ConsecutiveDelta2 q,o) . z,
z
by A7, A9, A12
.=
Bottom L
by A16, LATTICE5:def 7
;
:: thesis: verum
end;
ConsecutiveDelta2 q,
o in rng Ls
by A7, A9, A12, A14, FUNCT_1:def 5;
then A17:
h c= f
by A14, ZFMISC_1:92;
reconsider x' =
x as
Element of
ConsecutiveSet2 A,
o by A9, A11, A12;
dom h = [:(ConsecutiveSet2 A,o),(ConsecutiveSet2 A,o):]
by FUNCT_2:def 1;
then
[x,x] in dom h
by A13, ZFMISC_1:106;
hence f . x,
x =
h . x',
x'
by A17, GRFUNC_1:8
.=
Bottom L
by A15, LATTICE5:def 7
;
:: thesis: verum
end;
hence
S1[
O2]
by A6, A7, Th21;
:: thesis: verum
end;
for O being Ordinal holds S1[O]
from ORDINAL2:sch 1(A2, A3, A5);
hence
ConsecutiveDelta2 q,O is zeroed
; :: thesis: verum