let A be non empty set ; for L being lower-bounded LATTICE
for d being distance_function of A,L
for S being ExtensionSeq of A,d
for k, l being Element of NAT st k <= l holds
(S . k) `2 c= (S . l) `2
let L be lower-bounded LATTICE; for d being distance_function of A,L
for S being ExtensionSeq of A,d
for k, l being Element of NAT st k <= l holds
(S . k) `2 c= (S . l) `2
let d be distance_function of A,L; for S being ExtensionSeq of A,d
for k, l being Element of NAT st k <= l holds
(S . k) `2 c= (S . l) `2
let S be ExtensionSeq of A,d; for k, l being Element of NAT st k <= l holds
(S . k) `2 c= (S . l) `2
let k be Element of NAT ; for l being Element of NAT st k <= l holds
(S . k) `2 c= (S . l) `2
defpred S1[ Element of NAT ] means ( k <= $1 implies (S . k) `2 c= (S . $1) `2 );
A1:
for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be
Element of
NAT ;
( S1[i] implies S1[i + 1] )
assume that A2:
(
k <= i implies
(S . k) `2 c= (S . i) `2 )
and A3:
k <= i + 1
;
(S . k) `2 c= (S . (i + 1)) `2
per cases
( k = i + 1 or k <= i )
by A3, NAT_1:8;
suppose A4:
k <= i
;
(S . k) `2 c= (S . (i + 1)) `2 consider A9 being non
empty set ,
d9 being
distance_function of
A9,
L,
Aq being non
empty set ,
dq being
distance_function of
Aq,
L such that A5:
Aq,
dq is_extension_of A9,
d9
and A6:
S . i = [A9,d9]
and A7:
S . (i + 1) = [Aq,dq]
by Def21;
consider q being
QuadrSeq of
d9 such that
Aq = NextSet d9
and A8:
dq = NextDelta q
by A5, Def20;
(S . i) `2 = d9
by A6, MCART_1:def 2;
then A9:
(S . i) `2 c= ConsecutiveDelta (
q,
(DistEsti d9))
by Th34;
(S . (i + 1)) `2 = ConsecutiveDelta (
q,
(DistEsti d9))
by A7, A8, MCART_1:def 2;
hence
(S . k) `2 c= (S . (i + 1)) `2
by A2, A4, A9, XBOOLE_1:1;
verum end;
end;
A10:
S1[ 0 ]
by NAT_1:3;
thus
for l being Element of NAT holds S1[l]
from NAT_1:sch 1(A10, A1); verum