let L be lower-bounded LATTICE; :: thesis: for S being ExtensionSeq of the carrier of L, BasicDF L
for FS being non empty set st FS = union { ((S . i) `1) where i is Element of NAT : verum } holds
union { ((S . i) `2) where i is Element of NAT : verum } is distance_function of FS,L
let S be ExtensionSeq of the carrier of L, BasicDF L; :: thesis: for FS being non empty set st FS = union { ((S . i) `1) where i is Element of NAT : verum } holds
union { ((S . i) `2) where i is Element of NAT : verum } is distance_function of FS,L
let FS be non empty set ; :: thesis: ( FS = union { ((S . i) `1) where i is Element of NAT : verum } implies union { ((S . i) `2) where i is Element of NAT : verum } is distance_function of FS,L )
assume A1: FS = union { ((S . i) `1) where i is Element of NAT : verum } ; :: thesis: union { ((S . i) `2) where i is Element of NAT : verum } is distance_function of FS,L
reconsider FS = FS as non empty set ;
set A = the carrier of L;
set FD = union { ((S . i) `2) where i is Element of NAT : verum } ;

now :: thesis: for x, y being set st x in { ((S . i) `2) where i is Element of NAT : verum } & y in { ((S . i) `2) where i is Element of NAT : verum } holds
x,y are_c=-comparable

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

end;

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

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { ((S . i) `2) where i is Element of NAT : verum } or z in PFuncs ([:FS,FS:], the carrier of L) )
assume z in { ((S . i) `2) where i is Element of NAT : verum } ; :: thesis: z in PFuncs ([:FS,FS:], the carrier of L)
then consider j being Element of NAT such that
A7: z = (S . j) `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
Aq,dq is_extension_of A9,d9 and
A8: S . j = [A9,d9] and
S . (j + 1) = [Aq,dq] by Def20;
A9 = [A9,d9] `1 ;
then A9 in { ((S . i) `1) where i is Element of NAT : verum } by A8;
then ( dom d9 = [:A9,A9:] & A9 c= FS ) by A1, FUNCT_2:def 1, ZFMISC_1:74;
then A9: ( rng d9 c= the carrier of L & dom d9 c= [:FS,FS:] ) by ZFMISC_1:96;
z = d9 by A7, A8;
hence z in PFuncs ([:FS,FS:], the carrier of L) by A9, PARTFUN1:def 3; :: thesis: verum

end;

then union { ((S . i) `2) where i is Element of NAT : verum } in PFuncs ([:FS,FS:], the carrier of L) by A6, TREES_2:40;
then A10: ex g being Function st
( union { ((S . i) `2) where i is Element of NAT : verum } = g & dom g c= [:FS,FS:] & rng g c= the carrier of L ) by PARTFUN1:def 3;
(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 ;
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 } ;
defpred S<sub>1</sub>[ object , object ] means $2 = (S . $1) `2 ;
A11: { [: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: { [:((S . i) `1),((S . i) `1):] where i is Element of NAT : verum } c= { [:I,I:] where I is Element of X : I in X }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { [:I,I:] where I is Element of X : I in X } or x in { [:((S . i) `1),((S . i) `1):] where i is Element of NAT : verum } )
assume x in { [:I,I:] where I is Element of X : I in X } ; :: thesis: x in { [:((S . i) `1),((S . i) `1):] where i is Element of NAT : verum }
then consider J being Element of X such that
A12: x = [:J,J:] and
A13: J in X ;
ex j being Element of NAT st J = (S . j) `1 by A13;
hence x in { [:((S . i) `1),((S . i) `1):] where i is Element of NAT : verum } by A12; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { [:((S . i) `1),((S . i) `1):] where i is Element of NAT : verum } or x in { [:I,I:] where I is Element of X : I in X } )
assume x in { [:((S . i) `1),((S . i) `1):] where i is Element of NAT : verum } ; :: thesis: x in { [:I,I:] where I is Element of X : I in X }
then consider j being Element of NAT such that
A14: 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 A14; :: thesis: verum

end;

reconsider FD = union { ((S . i) `2) where i is Element of NAT : verum } as Function by A10;
A15: for x being object st x in NAT holds
ex y being object st S<sub>1</sub>[x,y] ;
consider F being Function such that
A16: dom F = NAT and
A17: for x being object st x in NAT holds
S<sub>1</sub>[x,F . x] from CLASSES1:sch 1(A15);
A18: 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: { ((S . i) `2) where i is Element of NAT : verum } c= rng F

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng F or x in { ((S . i) `2) where i is Element of NAT : verum } )
assume x in rng F ; :: thesis: x in { ((S . i) `2) where i is Element of NAT : verum }
then consider j being object such that
A19: j in dom F and
A20: F . j = x by FUNCT_1:def 3;
reconsider j = j as Element of NAT by A16, A19;
x = (S . j) `2 by A17, A20;
hence x in { ((S . i) `2) where i is Element of NAT : verum } ; :: thesis: verum

end;

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

end;

F is Function-yielding

proof

let x be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in proj1 F or F . x is set )
assume x in dom F ; :: thesis: F . x is set
then reconsider j = x as Element of NAT by A16;
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
A22: S . j = [A1,d1] and
S . (j + 1) = [Aq1,dq1] by Def20;
[A1,d1] `2 = d1 ;
hence F . x is set by A17, A22; :: thesis: verum

end;

then reconsider F = F as Function-yielding Function ;
A23: 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: { [:((S . i) `1),((S . i) `1):] where i is Element of NAT : verum } c= rng (doms F)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (doms F) or x in { [:((S . i) `1),((S . i) `1):] where i is Element of NAT : verum } )
assume x in rng (doms F) ; :: thesis: x in { [:((S . i) `1),((S . i) `1):] where i is Element of NAT : verum }
then consider j being object such that
A24: j in dom (doms F) and
A25: x = (doms F) . j by FUNCT_1:def 3;
A26: j in dom F by A24, FUNCT_6:59;
reconsider j = j as Element of NAT by A16, A24, FUNCT_6:59;
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
A27: S . j = [A1,d1] and
S . (j + 1) = [Aq1,dq1] by Def20;
A28: [A1,d1] `2 = d1 ;
x = dom (F . j) by A25, A26, FUNCT_6:22
.= dom d1 by A17, A28, A27
.= [:((S . j) `1),((S . j) `1):] by A27, FUNCT_2:def 1 ;
hence x in { [:((S . i) `1),((S . i) `1):] where i is Element of NAT : verum } ; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { [:((S . i) `1),((S . i) `1):] where i is Element of NAT : verum } or x in rng (doms F) )
assume x in { [:((S . i) `1),((S . i) `1):] where i is Element of NAT : verum } ; :: thesis: x in rng (doms F)
then consider j being Element of NAT such that
A29: 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
A30: S . j = [A1,d1] and
S . (j + 1) = [Aq1,dq1] by Def20;
A31: [A1,d1] `2 = d1 ;
j in NAT ;
then A32: j in dom (doms F) by A16, FUNCT_6:59;
x = dom d1 by A29, A30, FUNCT_2:def 1
.= dom (F . j) by A17, A31, A30
.= (doms F) . j by A16, FUNCT_6:22 ;
hence x in rng (doms F) by A32, FUNCT_1:def 3; :: thesis: verum

end;

now :: thesis: for x, y being set st x in X & y in X holds
x,y are_c=-comparable

let x, y be set ; :: thesis: ( x in X & y in X implies x,y are_c=-comparable )
assume that
A33: x in X and
A34: y in X ; :: thesis: x,y are_c=-comparable
consider k being Element of NAT such that
A35: x = (S . k) `1 by A33;
consider l being Element of NAT such that
A36: y = (S . l) `1 by A34;
( k <= l or l <= k ) ;
then ( x c= y or y c= x ) by A35, A36, Th38;
hence x,y are_c=-comparable ; :: thesis: verum

end;

then X is c=-linear ;
then [:FS,FS:] = union (rng (doms F)) by A1, A23, A11, Th3
.= dom FD by A18, Th1 ;
then reconsider FD = FD as BiFunction of FS,L by A10, FUNCT_2:def 1, RELSET_1:4;
A37: FD is symmetric

proof

let x, y be Element of FS; :: according to LATTICE5:def 5 :: thesis: FD . (x,y) = FD . (y,x)
consider x1 being set such that
A38: x in x1 and
A39: x1 in X by A1, TARSKI:def 4;
consider k being Element of NAT such that
A40: x1 = (S . k) `1 by A39;
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
A41: S . k = [A1,d1] and
S . (k + 1) = [Aq1,dq1] by Def20;
A42: [A1,d1] `1 = A1 ;
A43: x in A1 by A38, A40, A41;
[A1,d1] `2 = d1 ;
then d1 in { ((S . i) `2) where i is Element of NAT : verum } by A41;
then A44: d1 c= FD by ZFMISC_1:74;
consider y1 being set such that
A45: y in y1 and
A46: y1 in X by A1, TARSKI:def 4;
consider l being Element of NAT such that
A47: y1 = (S . l) `1 by A46;
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
A48: S . l = [A2,d2] and
S . (l + 1) = [Aq2,dq2] by Def20;
A49: [A2,d2] `1 = A2 ;
A50: y in A2 by A45, A47, A48;
[A2,d2] `2 = d2 ;
then d2 in { ((S . i) `2) where i is Element of NAT : verum } by A48;
then A51: d2 c= FD by ZFMISC_1:74;

per cases ( k <= l or l <= k ) ;

suppose k <= l ; :: thesis: FD . (x,y) = FD . (y,x)

then A1 c= A2 by A42, A49, Th38, A41, A48;
then reconsider x9 = x, y9 = y as Element of A2 by A43, A50;
A52: dom d2 = [:A2,A2:] by FUNCT_2:def 1;
hence FD . (x,y) = d2 . [x9,y9] by A51, GRFUNC_1:2
.= d2 . (x9,y9)
.= d2 . (y9,x9) by Def5
.= FD . [y9,x9] by A51, A52, GRFUNC_1:2
.= FD . (y,x) ;
:: thesis: verum

end;

suppose l <= k ; :: thesis: FD . (x,y) = FD . (y,x)

then A2 c= A1 by A42, A49, Th38, A48, A41;
then reconsider x9 = x, y9 = y as Element of A1 by A38, A40, A41, A50;
A53: dom d1 = [:A1,A1:] by FUNCT_2:def 1;
hence FD . (x,y) = d1 . [x9,y9] by A44, GRFUNC_1:2
.= d1 . (x9,y9)
.= d1 . (y9,x9) by Def5
.= FD . [y9,x9] by A44, A53, GRFUNC_1:2
.= FD . (y,x) ;
:: thesis: verum

end;

end;

end;

A54: FD is u.t.i.

proof

let x, y, z be Element of FS; :: according to LATTICE5:def 7 :: thesis: (FD . (x,y)) "\/" (FD . (y,z)) >= FD . (x,z)
consider x1 being set such that
A55: x in x1 and
A56: x1 in X by A1, TARSKI:def 4;
consider k being Element of NAT such that
A57: x1 = (S . k) `1 by A56;
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
A58: S . k = [A1,d1] and
S . (k + 1) = [Aq1,dq1] by Def20;
A59: x in A1 by A55, A57, A58;
[A1,d1] `2 = d1 ;
then d1 in { ((S . i) `2) where i is Element of NAT : verum } by A58;
then A60: d1 c= FD by ZFMISC_1:74;
A61: dom d1 = [:A1,A1:] by FUNCT_2:def 1;
A62: (S . k) `1 = A1 by A58;
consider y1 being set such that
A63: y in y1 and
A64: y1 in X by A1, TARSKI:def 4;
consider l being Element of NAT such that
A65: y1 = (S . l) `1 by A64;
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
A66: S . l = [A2,d2] and
S . (l + 1) = [Aq2,dq2] by Def20;
A67: y in A2 by A63, A65, A66;
[A2,d2] `2 = d2 ;
then d2 in { ((S . i) `2) where i is Element of NAT : verum } by A66;
then A68: d2 c= FD by ZFMISC_1:74;
A69: dom d2 = [:A2,A2:] by FUNCT_2:def 1;
A70: [A2,d2] `1 = A2 ;
consider z1 being set such that
A71: z in z1 and
A72: z1 in X by A1, TARSKI:def 4;
consider n being Element of NAT such that
A73: z1 = (S . n) `1 by A72;
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
A74: S . n = [A3,d3] and
S . (n + 1) = [Aq3,dq3] by Def20;
A75: [A3,d3] `1 = A3 ;
A76: z in A3 by A71, A73, A74;
[A3,d3] `2 = d3 ;
then d3 in { ((S . i) `2) where i is Element of NAT : verum } by A74;
then A77: d3 c= FD by ZFMISC_1:74;
A78: dom d3 = [:A3,A3:] by FUNCT_2:def 1;

per cases ( k <= l or l <= k ) ;

suppose k <= l ; :: thesis: (FD . (x,y)) "\/" (FD . (y,z)) >= FD . (x,z)

then A79: A1 c= A2 by A62, A70, Th38, A66;
thus (FD . (x,y)) "\/" (FD . (y,z)) >= FD . (x,z) :: thesis: verum

proof

per cases ( l <= n or n <= l ) ;

suppose l <= n ; :: thesis: (FD . (x,y)) "\/" (FD . (y,z)) >= FD . (x,z)

then A80: A2 c= A3 by A70, A75, Th38, A74, A66;
then A1 c= A3 by A79;
then reconsider x9 = x, y9 = y as Element of A3 by A59, A67, A80;
reconsider z9 = z as Element of A3 by A76;
A81: FD . (y,z) = d3 . [y9,z9] by A77, A78, GRFUNC_1:2
.= d3 . (y9,z9) ;
A82: FD . (x,z) = d3 . [x9,z9] by A77, A78, GRFUNC_1:2
.= d3 . (x9,z9) ;
FD . (x,y) = d3 . [x9,y9] by A77, A78, GRFUNC_1:2
.= d3 . (x9,y9) ;
hence (FD . (x,y)) "\/" (FD . (y,z)) >= FD . (x,z) by A81, A82, Def7; :: thesis: verum

end;

suppose n <= l ; :: thesis: (FD . (x,y)) "\/" (FD . (y,z)) >= FD . (x,z)

then A83: A3 c= A2 by A70, A75, Th38, A74, A66;
reconsider y9 = y as Element of A2 by A67;
reconsider x9 = x as Element of A2 by A59, A79;
reconsider z9 = z as Element of A2 by A76, A83;
A84: FD . (y,z) = d2 . [y9,z9] by A68, A69, GRFUNC_1:2
.= d2 . (y9,z9) ;
A85: FD . (x,z) = d2 . [x9,z9] by A68, A69, GRFUNC_1:2
.= d2 . (x9,z9) ;
FD . (x,y) = d2 . [x9,y9] by A68, A69, GRFUNC_1:2
.= d2 . (x9,y9) ;
hence (FD . (x,y)) "\/" (FD . (y,z)) >= FD . (x,z) by A84, A85, Def7; :: thesis: verum

end;

end;

end;

end;

suppose l <= k ; :: thesis: (FD . (x,y)) "\/" (FD . (y,z)) >= FD . (x,z)

then A86: A2 c= A1 by A62, A70, Th38, A66;
thus (FD . (x,y)) "\/" (FD . (y,z)) >= FD . (x,z) :: thesis: verum

proof

per cases ( k <= n or n <= k ) ;

suppose k <= n ; :: thesis: (FD . (x,y)) "\/" (FD . (y,z)) >= FD . (x,z)

then A87: A1 c= A3 by A62, A75, Th38, A74;
then A88: A2 c= A3 by A86;
reconsider x9 = x as Element of A3 by A59, A87;
reconsider z9 = z as Element of A3 by A71, A73, A74;
reconsider y9 = y as Element of A3 by A67, A88;
A89: FD . (y,z) = d3 . [y9,z9] by A77, A78, GRFUNC_1:2
.= d3 . (y9,z9) ;
A90: FD . (x,z) = d3 . [x9,z9] by A77, A78, GRFUNC_1:2
.= d3 . (x9,z9) ;
FD . (x,y) = d3 . [x9,y9] by A77, A78, GRFUNC_1:2
.= d3 . (x9,y9) ;
hence (FD . (x,y)) "\/" (FD . (y,z)) >= FD . (x,z) by A89, A90, Def7; :: thesis: verum

end;

suppose n <= k ; :: thesis: (FD . (x,y)) "\/" (FD . (y,z)) >= FD . (x,z)

then A3 c= A1 by A62, A75, Th38, A74;
then reconsider x9 = x, y9 = y, z9 = z as Element of A1 by A55, A57, A58, A67, A76, A86;
A91: FD . (y,z) = d1 . [y9,z9] by A60, A61, GRFUNC_1:2
.= d1 . (y9,z9) ;
A92: FD . (x,z) = d1 . [x9,z9] by A60, A61, GRFUNC_1:2
.= d1 . (x9,z9) ;
FD . (x,y) = d1 . [x9,y9] by A60, A61, GRFUNC_1:2
.= d1 . (x9,y9) ;
hence (FD . (x,y)) "\/" (FD . (y,z)) >= FD . (x,z) by A91, A92, Def7; :: thesis: verum

end;

end;

end;

end;

end;

end;

FD is zeroed

proof

let x be Element of FS; :: according to LATTICE5:def 6 :: thesis: FD . (x,x) = Bottom L
consider y being set such that
A93: x in y and
A94: y in X by A1, TARSKI:def 4;
consider j being Element of NAT such that
A95: y = (S . j) `1 by A94;
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
A96: S . j = [A1,d1] and
S . (j + 1) = [Aq1,dq1] by Def20;
reconsider x9 = x as Element of A1 by A93, A95, A96;
[A1,d1] `2 = d1 ;
then d1 in { ((S . i) `2) where i is Element of NAT : verum } by A96;
then A97: d1 c= FD by ZFMISC_1:74;
dom d1 = [:A1,A1:] by FUNCT_2:def 1;
hence FD . (x,x) = d1 . [x9,x9] by A97, GRFUNC_1:2
.= d1 . (x9,x9)
.= Bottom L by Def6 ;
:: thesis: verum

end;

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