let L be lower-bounded LATTICE; :: thesis:
let S be ExtensionSeq of the carrier of L, BasicDF L; :: thesis:
let FS be non empty set ; :: thesis:
assume A1: FS = union { ((S . i) `1 ) where i is Element of NAT : verum } ; :: thesis:
set FD = union { ((S . i) `2 ) where i is Element of NAT : verum } ;
set A = the carrier of L;
(S . 0 ) `1 in { ((S . i) `1 ) where i is Element of NAT : verum } ;
then reconsider X = { ((S . i) `1 ) where i is Element of NAT : verum } as non empty set ;
reconsider FS = FS as non empty set ;
A2: { ((S . i) `2 ) where i is Element of NAT : verum } is c=-linear

proof

now

let x, y be set ; :: thesis:
assume that
A3: x in { ((S . i) `2 ) where i is Element of NAT : verum } and
A4: y in { ((S . i) `2 ) where i is Element of NAT : verum } ; :: thesis:
consider k being Element of NAT such that
A5: x = (S . k) `2 by A3;
consider l being Element of NAT such that
A6: y = (S . l) `2 by A4;
( k <= l or l <= k ) ;
then ( x c= y or y c= x ) by A5, A6, Th42;
hence x,y are_c=-comparable by XBOOLE_0:def 9; :: thesis:

end;

hence { ((S . i) `2 ) where i is Element of NAT : verum } is c=-linear by ORDINAL1:def 9; :: thesis:

end;

{ ((S . i) `2 ) where i is Element of NAT : verum } c= PFuncs [:FS,FS:],the carrier of L

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume z in { ((S . i) `2 ) where i is Element of NAT : verum } ; :: thesis:
then consider j being Element of NAT such that
A7: z = (S . j) `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
Aq,dq is_extension_of A',d' and
A8: ( S . j = [A',d'] & S . (j + 1) = [Aq,dq] ) by Def21;
A9: z = d' by A7, A8, MCART_1:def 2;
A10: rng d' c= the carrier of L ;
A11: dom d' = [:A',A':] by FUNCT_2:def 1;
A' = (S . j) `1 by A8, MCART_1:def 1;
then A' in { ((S . i) `1 ) where i is Element of NAT : verum } ;
then A' c= FS by A1, ZFMISC_1:92;
then dom d' c= [:FS,FS:] by A11, ZFMISC_1:119;
hence z in PFuncs [:FS,FS:],the carrier of L by A9, A10, PARTFUN1:def 5; :: thesis:

end;

then union { ((S . i) `2 ) where i is Element of NAT : verum } in PFuncs [:FS,FS:],the carrier of L by A2, HAHNBAN:13;
then consider g being Function such that
A12: union { ((S . i) `2 ) where i is Element of NAT : verum } = g and
dom g c= [:FS,FS:] and
A13: rng g c= the carrier of L by PARTFUN1:def 5;
reconsider FD = union { ((S . i) `2 ) where i is Element of NAT : verum } as Function by A12;
A14: X is c=-linear

proof

now

let x, y be set ; :: thesis:
assume that
A15: x in X and
A16: y in X ; :: thesis:
consider k being Element of NAT such that
A17: x = (S . k) `1 by A15;
consider l being Element of NAT such that
A18: y = (S . l) `1 by A16;
( k <= l or l <= k ) ;
then ( x c= y or y c= x ) by A17, A18, Th41;
hence x,y are_c=-comparable by XBOOLE_0:def 9; :: thesis:

end;

hence X is c=-linear by ORDINAL1:def 9; :: thesis:

end;

defpred S₁[ set , set ] means $2 = (S . $1) `2 ;
A20: for x being set st x in NAT holds
ex y being set st S₁[x,y] ;
consider F being Function such that
A21: dom F = NAT and
A22: for x being set st x in NAT holds
S₁[x,F . x] from CLASSES1:sch 1(A20);
A23: rng F = { ((S . i) `2 ) where i is Element of NAT : verum }

proof

thus rng F c= { ((S . i) `2 ) where i is Element of NAT : verum } :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng F ; :: thesis:
then consider j being set such that
A24: ( j in dom F & F . j = x ) by FUNCT_1:def 5;
reconsider j = j as Element of NAT by A21, A24;
x = (S . j) `2 by A22, A24;
hence x in { ((S . i) `2 ) where i is Element of NAT : verum } ; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { ((S . i) `2 ) where i is Element of NAT : verum } ; :: thesis:
then consider j being Element of NAT such that
A25: x = (S . j) `2 ;
x = F . j by A22, A25;
hence x in rng F by A21, FUNCT_1:def 5; :: thesis:

end;

F is Function-yielding

proof

let x be set ; :: according to FUNCOP_1:def 6 :: thesis:
assume x in dom F ; :: thesis:
then reconsider j = x as Element of NAT by A21;
consider A1 being non empty set , d1 being distance_function of A1,L, Aq1 being non empty set , dq1 being distance_function of Aq1,L such that
Aq1,dq1 is_extension_of A1,d1 and
A26: ( S . j = [A1,d1] & S . (j + 1) = [Aq1,dq1] ) by Def21;
(S . j) `2 = d1 by A26, MCART_1:def 2;
hence F . x is set by A22; :: thesis:

end;

then reconsider F = F as Function-yielding Function ;
set LL = { [:I,I:] where I is Element of X : I in X } ;
set PP = { [:((S . i) `1 ),((S . i) `1 ):] where i is Element of NAT : verum } ;
A27: rng (doms F) = { [:((S . i) `1 ),((S . i) `1 ):] where i is Element of NAT : verum }

proof

thus rng (doms F) c= { [:((S . i) `1 ),((S . i) `1 ):] where i is Element of NAT : verum } :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng (doms F) ; :: thesis:
then consider j being set such that
A28: ( j in dom (doms F) & x = (doms F) . j ) by FUNCT_1:def 5;
A29: j in dom F by A28, FUNCT_6:89;
reconsider j = j as Element of NAT by A21, A28, FUNCT_6:89;
consider A1 being non empty set , d1 being distance_function of A1,L, Aq1 being non empty set , dq1 being distance_function of Aq1,L such that
Aq1,dq1 is_extension_of A1,d1 and
A30: ( S . j = [A1,d1] & S . (j + 1) = [Aq1,dq1] ) by Def21;
A31: (S . j) `2 = d1 by A30, MCART_1:def 2;
A32: (S . j) `1 = A1 by A30, MCART_1:def 1;
x = dom (F . j) by A28, A29, FUNCT_6:31
.= dom d1 by A22, A31
.= [:((S . j) `1 ),((S . j) `1 ):] by A32, FUNCT_2:def 1 ;
hence x in { [:((S . i) `1 ),((S . i) `1 ):] where i is Element of NAT : verum } ; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { [:((S . i) `1 ),((S . i) `1 ):] where i is Element of NAT : verum } ; :: thesis:
then consider j being Element of NAT such that
A33: x = [:((S . j) `1 ),((S . j) `1 ):] ;
consider A1 being non empty set , d1 being distance_function of A1,L, Aq1 being non empty set , dq1 being distance_function of Aq1,L such that
Aq1,dq1 is_extension_of A1,d1 and
A34: ( S . j = [A1,d1] & S . (j + 1) = [Aq1,dq1] ) by Def21;
A35: (S . j) `2 = d1 by A34, MCART_1:def 2;
A36: (S . j) `1 = A1 by A34, MCART_1:def 1;
j in NAT ;
then A37: j in dom (doms F) by A21, FUNCT_6:89;
x = dom d1 by A33, A36, FUNCT_2:def 1
.= dom (F . j) by A22, A35
.= (doms F) . j by A21, FUNCT_6:31 ;
hence x in rng (doms F) by A37, FUNCT_1:def 5; :: thesis:

end;

{ [:I,I:] where I is Element of X : I in X } = { [:((S . i) `1 ),((S . i) `1 ):] where i is Element of NAT : verum }

proof

thus { [:I,I:] where I is Element of X : I in X } c= { [:((S . i) `1 ),((S . i) `1 ):] where i is Element of NAT : verum } :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { [:I,I:] where I is Element of X : I in X } ; :: thesis:
then consider J being Element of X such that
A38: x = [:J,J:] and
A39: J in X ;
consider j being Element of NAT such that
A40: J = (S . j) `1 by A39;
thus x in { [:((S . i) `1 ),((S . i) `1 ):] where i is Element of NAT : verum } by A38, A40; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { [:((S . i) `1 ),((S . i) `1 ):] where i is Element of NAT : verum } ; :: thesis:
then consider j being Element of NAT such that
A41: x = [:((S . j) `1 ),((S . j) `1 ):] ;
(S . j) `1 in X ;
hence x in { [:I,I:] where I is Element of X : I in X } by A41; :: thesis:

end;

then [:FS,FS:] = union (rng (doms F)) by A1, A14, A27, Th3
.= dom FD by A23, Th1 ;
then reconsider FD = FD as BiFunction of FS,L by A12, A13, FUNCT_2:def 1, RELSET_1:11;
A42: FD is zeroed

proof

let x be Element of FS; :: according to LATTICE5:def 7 :: thesis:
consider y being set such that
A43: ( x in y & y in X ) by A1, TARSKI:def 4;
consider j being Element of NAT such that
A44: y = (S . j) `1 by A43;
consider A1 being non empty set , d1 being distance_function of A1,L, Aq1 being non empty set , dq1 being distance_function of Aq1,L such that
Aq1,dq1 is_extension_of A1,d1 and
A45: ( S . j = [A1,d1] & S . (j + 1) = [Aq1,dq1] ) by Def21;
A46: (S . j) `2 = d1 by A45, MCART_1:def 2;
reconsider x' = x as Element of A1 by A43, A44, A45, MCART_1:def 1;
d1 in { ((S . i) `2 ) where i is Element of NAT : verum } by A46;
then A47: d1 c= FD by ZFMISC_1:92;
dom d1 = [:A1,A1:] by FUNCT_2:def 1;
hence FD . x,x = d1 . [x',x'] by A47, GRFUNC_1:8
.= d1 . x',x'
.= Bottom L by Def7 ;
:: thesis:

end;

A48: FD is symmetric

proof

let x, y be Element of FS; :: according to LATTICE5:def 6 :: thesis:
consider x1 being set such that
A49: ( x in x1 & x1 in X ) by A1, TARSKI:def 4;
consider k being Element of NAT such that
A50: x1 = (S . k) `1 by A49;
consider A1 being non empty set , d1 being distance_function of A1,L, Aq1 being non empty set , dq1 being distance_function of Aq1,L such that
Aq1,dq1 is_extension_of A1,d1 and
A51: ( S . k = [A1,d1] & S . (k + 1) = [Aq1,dq1] ) by Def21;
A52: (S . k) `2 = d1 by A51, MCART_1:def 2;
A53: (S . k) `1 = A1 by A51, MCART_1:def 1;
d1 in { ((S . i) `2 ) where i is Element of NAT : verum } by A52;
then A54: d1 c= FD by ZFMISC_1:92;
A55: x in A1 by A49, A50, A51, MCART_1:def 1;
consider y1 being set such that
A56: ( y in y1 & y1 in X ) by A1, TARSKI:def 4;
consider l being Element of NAT such that
A57: y1 = (S . l) `1 by A56;
consider A2 being non empty set , d2 being distance_function of A2,L, Aq2 being non empty set , dq2 being distance_function of Aq2,L such that
Aq2,dq2 is_extension_of A2,d2 and
A58: ( S . l = [A2,d2] & S . (l + 1) = [Aq2,dq2] ) by Def21;
A59: (S . l) `2 = d2 by A58, MCART_1:def 2;
A60: (S . l) `1 = A2 by A58, MCART_1:def 1;
d2 in { ((S . i) `2 ) where i is Element of NAT : verum } by A59;
then A61: d2 c= FD by ZFMISC_1:92;
A62: y in A2 by A56, A57, A58, MCART_1:def 1;

per cases ;

suppose k <= l ; :: thesis:

then A1 c= A2 by A53, A60, Th41;
then reconsider x' = x, y' = y as Element of A2 by A55, A56, A57, A58, MCART_1:def 1;
A63: dom d2 = [:A2,A2:] by FUNCT_2:def 1;
hence FD . x,y = d2 . [x',y'] by A61, GRFUNC_1:8
.= d2 . x',y'
.= d2 . y',x' by Def6
.= FD . [y',x'] by A61, A63, GRFUNC_1:8
.= FD . y,x ;
:: thesis:

end;

suppose l <= k ; :: thesis:

then A2 c= A1 by A53, A60, Th41;
then reconsider x' = x, y' = y as Element of A1 by A49, A50, A51, A62, MCART_1:def 1;
A64: dom d1 = [:A1,A1:] by FUNCT_2:def 1;
hence FD . x,y = d1 . [x',y'] by A54, GRFUNC_1:8
.= d1 . x',y'
.= d1 . y',x' by Def6
.= FD . [y',x'] by A54, A64, GRFUNC_1:8
.= FD . y,x ;
:: thesis:

end;

FD is u.t.i.

proof

let x, y, z be Element of FS; :: according to LATTICE5:def 8 :: thesis:
consider x1 being set such that
A65: ( x in x1 & x1 in X ) by A1, TARSKI:def 4;
consider k being Element of NAT such that
A66: x1 = (S . k) `1 by A65;
consider A1 being non empty set , d1 being distance_function of A1,L, Aq1 being non empty set , dq1 being distance_function of Aq1,L such that
Aq1,dq1 is_extension_of A1,d1 and
A67: ( S . k = [A1,d1] & S . (k + 1) = [Aq1,dq1] ) by Def21;
A68: (S . k) `2 = d1 by A67, MCART_1:def 2;
A69: (S . k) `1 = A1 by A67, MCART_1:def 1;
d1 in { ((S . i) `2 ) where i is Element of NAT : verum } by A68;
then A70: d1 c= FD by ZFMISC_1:92;
A71: x in A1 by A65, A66, A67, MCART_1:def 1;
A72: dom d1 = [:A1,A1:] by FUNCT_2:def 1;
consider y1 being set such that
A73: ( y in y1 & y1 in X ) by A1, TARSKI:def 4;
consider l being Element of NAT such that
A74: y1 = (S . l) `1 by A73;
consider A2 being non empty set , d2 being distance_function of A2,L, Aq2 being non empty set , dq2 being distance_function of Aq2,L such that
Aq2,dq2 is_extension_of A2,d2 and
A75: ( S . l = [A2,d2] & S . (l + 1) = [Aq2,dq2] ) by Def21;
A76: (S . l) `2 = d2 by A75, MCART_1:def 2;
A77: (S . l) `1 = A2 by A75, MCART_1:def 1;
d2 in { ((S . i) `2 ) where i is Element of NAT : verum } by A76;
then A78: d2 c= FD by ZFMISC_1:92;
A79: y in A2 by A73, A74, A75, MCART_1:def 1;
A80: dom d2 = [:A2,A2:] by FUNCT_2:def 1;
consider z1 being set such that
A81: ( z in z1 & z1 in X ) by A1, TARSKI:def 4;
consider n being Element of NAT such that
A82: z1 = (S . n) `1 by A81;
consider A3 being non empty set , d3 being distance_function of A3,L, Aq3 being non empty set , dq3 being distance_function of Aq3,L such that
Aq3,dq3 is_extension_of A3,d3 and
A83: ( S . n = [A3,d3] & S . (n + 1) = [Aq3,dq3] ) by Def21;
A84: (S . n) `2 = d3 by A83, MCART_1:def 2;
A85: (S . n) `1 = A3 by A83, MCART_1:def 1;
d3 in { ((S . i) `2 ) where i is Element of NAT : verum } by A84;
then A86: d3 c= FD by ZFMISC_1:92;
A87: z in A3 by A81, A82, A83, MCART_1:def 1;
A88: dom d3 = [:A3,A3:] by FUNCT_2:def 1;

per cases ;

suppose k <= l ; :: thesis:

then A89: A1 c= A2 by A69, A77, Th41;
thus (FD . x,y) "\/" (FD . y,z) >= FD . x,z :: thesis:

proof

per cases ;

suppose l <= n ; :: thesis:

then A90: A2 c= A3 by A77, A85, Th41;
then A1 c= A3 by A89, XBOOLE_1:1;
then reconsider x' = x, y' = y, z' = z as Element of A3 by A71, A79, A81, A82, A83, A90, MCART_1:def 1;
A91: FD . x,y = d3 . [x',y'] by A86, A88, GRFUNC_1:8
.= d3 . x',y' ;
A92: FD . y,z = d3 . [y',z'] by A86, A88, GRFUNC_1:8
.= d3 . y',z' ;
FD . x,z = d3 . [x',z'] by A86, A88, GRFUNC_1:8
.= d3 . x',z' ;
hence (FD . x,y) "\/" (FD . y,z) >= FD . x,z by A91, A92, Def8; :: thesis:

end;

suppose n <= l ; :: thesis:

then A3 c= A2 by A77, A85, Th41;
then reconsider x' = x, y' = y, z' = z as Element of A2 by A71, A73, A74, A75, A87, A89, MCART_1:def 1;
A93: FD . x,y = d2 . [x',y'] by A78, A80, GRFUNC_1:8
.= d2 . x',y' ;
A94: FD . y,z = d2 . [y',z'] by A78, A80, GRFUNC_1:8
.= d2 . y',z' ;
FD . x,z = d2 . [x',z'] by A78, A80, GRFUNC_1:8
.= d2 . x',z' ;
hence (FD . x,y) "\/" (FD . y,z) >= FD . x,z by A93, A94, Def8; :: thesis:

end;

suppose l <= k ; :: thesis:

then A95: A2 c= A1 by A69, A77, Th41;
thus (FD . x,y) "\/" (FD . y,z) >= FD . x,z :: thesis:

proof

per cases ;

suppose k <= n ; :: thesis:

then A96: A1 c= A3 by A69, A85, Th41;
then A2 c= A3 by A95, XBOOLE_1:1;
then reconsider x' = x, y' = y, z' = z as Element of A3 by A71, A79, A81, A82, A83, A96, MCART_1:def 1;
A97: FD . x,y = d3 . [x',y'] by A86, A88, GRFUNC_1:8
.= d3 . x',y' ;
A98: FD . y,z = d3 . [y',z'] by A86, A88, GRFUNC_1:8
.= d3 . y',z' ;
FD . x,z = d3 . [x',z'] by A86, A88, GRFUNC_1:8
.= d3 . x',z' ;
hence (FD . x,y) "\/" (FD . y,z) >= FD . x,z by A97, A98, Def8; :: thesis:

end;

suppose n <= k ; :: thesis:

then A3 c= A1 by A69, A85, Th41;
then reconsider x' = x, y' = y, z' = z as Element of A1 by A65, A66, A67, A79, A87, A95, MCART_1:def 1;
A99: FD . x,y = d1 . [x',y'] by A70, A72, GRFUNC_1:8
.= d1 . x',y' ;
A100: FD . y,z = d1 . [y',z'] by A70, A72, GRFUNC_1:8
.= d1 . y',z' ;
FD . x,z = d1 . [x',z'] by A70, A72, GRFUNC_1:8
.= d1 . x',z' ;
hence (FD . x,y) "\/" (FD . y,z) >= FD . x,z by A99, A100, Def8; :: thesis:

end;

hence union { ((S . i) `2 ) where i is Element of NAT : verum } is distance_function of FS,L by A42, A48; :: thesis: