let A be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: for k, l being Element of NAT st k <= l holds
(S . k) `2 c= (S . l) `2
let k be Element of NAT ; :: thesis: 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 ;
:: thesis: ( S1[i] implies S1[i + 1] )
assume that A2:
(
k <= i implies
(S . k) `2 c= (S . i) `2 )
and A3:
k <= i + 1
;
:: thesis: (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
;
:: thesis: (S . k) `2 c= (S . (i + 1)) `2 consider A' being non
empty set ,
d' being
distance_function of
A',
L,
Aq being non
empty set ,
dq being
distance_function of
Aq,
L such that A5:
Aq,
dq is_extension_of A',
d'
and A6:
S . i = [A',d']
and A7:
S . (i + 1) = [Aq,dq]
by Def21;
consider q being
QuadrSeq of
d' such that
Aq = NextSet d'
and A8:
dq = NextDelta q
by A5, Def20;
(S . i) `2 = d'
by A6, MCART_1:def 2;
then A9:
(S . i) `2 c= ConsecutiveDelta q,
(DistEsti d')
by Th34;
(S . (i + 1)) `2 = ConsecutiveDelta q,
(DistEsti d')
by A7, A8, MCART_1:def 2;
hence
(S . k) `2 c= (S . (i + 1)) `2
by A2, A4, A9, XBOOLE_1:1;
:: thesis: 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); :: thesis: verum