let L be lower-bounded modular LATTICE; :: thesis: for S being ExtensionSeq2 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 ExtensionSeq2 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, Th31;
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_extension2_of A9,d9 and
A8: S . j = [A9,d9] and
S . (j + 1) = [Aq,dq] by Def11;
A9: A9 = [A9,d9] `1 ;
A9 in { ((S . i) `1) where i is Element of NAT : verum } by A9, A8;
then ( dom d9 = [:A9,A9:] & A9 c= FS ) by A1, FUNCT_2:def 1, ZFMISC_1:74;
then A10: ( 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 A10, 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 A11: 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 ;
A12: { [: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
A13: x = [:J,J:] and
A14: J in X ;
ex j being Element of NAT st J = (S . j) `1 by A14;
hence x in { [:((S . i) `1),((S . i) `1):] where i is Element of NAT : verum } by A13; :: 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
A15: 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 A15; :: thesis: verum

end;

reconsider FD = union { ((S . i) `2) where i is Element of NAT : verum } as Function by A11;
A16: 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
A17: dom F = NAT and
A18: for x being object st x in NAT holds
S<sub>1</sub>[x,F . x] from CLASSES1:sch 1(A16);
A19: 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
A20: j in dom F and
A21: F . j = x by FUNCT_1:def 3;
reconsider j = j as Element of NAT by A17, A20;
x = (S . j) `2 by A18, A21;
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
A22: x = (S . j) `2 ;
x = F . j by A18, A22;
hence x in rng F by A17, 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 A17;
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_extension2_of A1,d1 and
A23: S . j = [A1,d1] and
S . (j + 1) = [Aq1,dq1] by Def11;
[A1,d1] `2 = d1 ;
hence F . x is set by A18, A23; :: thesis: verum

end;

then reconsider F = F as Function-yielding Function ;
A24: 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
A25: j in dom (doms F) and
A26: x = (doms F) . j by FUNCT_1:def 3;
A27: j in dom F by A25, FUNCT_6:59;
reconsider j = j as Element of NAT by A17, A25, 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_extension2_of A1,d1 and
A28: S . j = [A1,d1] and
S . (j + 1) = [Aq1,dq1] by Def11;
A29: [A1,d1] `2 = d1 ;
x = dom (F . j) by A26, A27, FUNCT_6:22
.= dom d1 by A18, A29, A28
.= [:((S . j) `1),((S . j) `1):] by A28, 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
A30: 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_extension2_of A1,d1 and
A31: S . j = [A1,d1] and
S . (j + 1) = [Aq1,dq1] by Def11;
A32: [A1,d1] `2 = d1 ;
j in NAT ;
then A33: j in dom (doms F) by A17, FUNCT_6:59;
x = dom d1 by A30, A31, FUNCT_2:def 1
.= dom (F . j) by A18, A32, A31
.= (doms F) . j by A17, FUNCT_6:22 ;
hence x in rng (doms F) by A33, 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
A34: x in X and
A35: y in X ; :: thesis: x,y are_c=-comparable
consider k being Element of NAT such that
A36: x = (S . k) `1 by A34;
consider l being Element of NAT such that
A37: y = (S . l) `1 by A35;
( k <= l or l <= k ) ;
then ( x c= y or y c= x ) by A36, A37, Th30;
hence x,y are_c=-comparable ; :: thesis: verum

end;

then X is c=-linear ;
then [:FS,FS:] = union (rng (doms F)) by A1, A24, A12, LATTICE5:3
.= dom FD by A19, LATTICE5:1 ;
then reconsider FD = FD as BiFunction of FS,L by A11, FUNCT_2:def 1, RELSET_1:4;
A38: 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
A39: x in x1 and
A40: x1 in X by A1, TARSKI:def 4;
consider k being Element of NAT such that
A41: x1 = (S . k) `1 by A40;
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_extension2_of A1,d1 and
A42: S . k = [A1,d1] and
S . (k + 1) = [Aq1,dq1] by Def11;
A43: [A1,d1] `1 = A1 ;
A44: x in A1 by A39, A41, A42;
[A1,d1] `2 = d1 ;
then d1 in { ((S . i) `2) where i is Element of NAT : verum } by A42;
then A45: d1 c= FD by ZFMISC_1:74;
consider y1 being set such that
A46: y in y1 and
A47: y1 in X by A1, TARSKI:def 4;
consider l being Element of NAT such that
A48: y1 = (S . l) `1 by A47;
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_extension2_of A2,d2 and
A49: S . l = [A2,d2] and
S . (l + 1) = [Aq2,dq2] by Def11;
A50: [A2,d2] `1 = A2 ;
A51: y in A2 by A46, A48, A49;
[A2,d2] `2 = d2 ;
then d2 in { ((S . i) `2) where i is Element of NAT : verum } by A49;
then A52: 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 A43, A50, Th30, A42, A49;
then reconsider x9 = x, y9 = y as Element of A2 by A44, A46, A48, A49;
A53: dom d2 = [:A2,A2:] by FUNCT_2:def 1;
hence FD . (x,y) = d2 . [x9,y9] by A52, GRFUNC_1:2
.= d2 . (x9,y9)
.= d2 . (y9,x9) by LATTICE5:def 5
.= FD . [y9,x9] by A52, A53, GRFUNC_1:2
.= FD . (y,x) ;
:: thesis: verum

end;

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

then A2 c= A1 by A43, A50, Th30, A42, A49;
then reconsider x9 = x, y9 = y as Element of A1 by A39, A41, A42, A51;
A54: dom d1 = [:A1,A1:] by FUNCT_2:def 1;
hence FD . (x,y) = d1 . [x9,y9] by A45, GRFUNC_1:2
.= d1 . (x9,y9)
.= d1 . (y9,x9) by LATTICE5:def 5
.= FD . [y9,x9] by A45, A54, GRFUNC_1:2
.= FD . (y,x) ;
:: thesis: verum

end;

end;

end;

A55: FD is u.t.i.

proof

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

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

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

then A80: A1 c= A2 by A60, A68, Th30, A59, A67;
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 A81: A2 c= A3 by A68, A76, Th30, A67, A75;
then A1 c= A3 by A80;
then reconsider x9 = x, y9 = y, z9 = z as Element of A3 by A61, A69, A72, A74, A75, A81;
A82: FD . (y,z) = d3 . [y9,z9] by A78, A79, GRFUNC_1:2
.= d3 . (y9,z9) ;
A83: FD . (x,z) = d3 . [x9,z9] by A78, A79, GRFUNC_1:2
.= d3 . (x9,z9) ;
FD . (x,y) = d3 . [x9,y9] by A78, A79, GRFUNC_1:2
.= d3 . (x9,y9) ;
hence (FD . (x,y)) "\/" (FD . (y,z)) >= FD . (x,z) by A82, A83, LATTICE5:def 7; :: thesis: verum

end;

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

then A3 c= A2 by A68, A76, Th30, A67, A75;
then reconsider x9 = x, y9 = y, z9 = z as Element of A2 by A61, A64, A66, A67, A77, A80;
A84: FD . (y,z) = d2 . [y9,z9] by A70, A71, GRFUNC_1:2
.= d2 . (y9,z9) ;
A85: FD . (x,z) = d2 . [x9,z9] by A70, A71, GRFUNC_1:2
.= d2 . (x9,z9) ;
FD . (x,y) = d2 . [x9,y9] by A70, A71, GRFUNC_1:2
.= d2 . (x9,y9) ;
hence (FD . (x,y)) "\/" (FD . (y,z)) >= FD . (x,z) by A84, A85, LATTICE5:def 7; :: thesis: verum

end;

end;

end;

end;

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

then A86: A2 c= A1 by A60, A68, Th30, A59, A67;
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 A60, A76, Th30, A59, A75;
then A2 c= A3 by A86;
then reconsider x9 = x, y9 = y, z9 = z as Element of A3 by A61, A69, A72, A74, A75, A87;
A88: FD . (y,z) = d3 . [y9,z9] by A78, A79, GRFUNC_1:2
.= d3 . (y9,z9) ;
A89: FD . (x,z) = d3 . [x9,z9] by A78, A79, GRFUNC_1:2
.= d3 . (x9,z9) ;
FD . (x,y) = d3 . [x9,y9] by A78, A79, GRFUNC_1:2
.= d3 . (x9,y9) ;
hence (FD . (x,y)) "\/" (FD . (y,z)) >= FD . (x,z) by A88, A89, LATTICE5:def 7; :: thesis: verum

end;

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

then A3 c= A1 by A60, A76, Th30, A59, A75;
then reconsider x9 = x, y9 = y, z9 = z as Element of A1 by A56, A58, A59, A69, A77, A86;
A90: FD . (y,z) = d1 . [y9,z9] by A62, A63, GRFUNC_1:2
.= d1 . (y9,z9) ;
A91: FD . (x,z) = d1 . [x9,z9] by A62, A63, GRFUNC_1:2
.= d1 . (x9,z9) ;
FD . (x,y) = d1 . [x9,y9] by A62, A63, GRFUNC_1:2
.= d1 . (x9,y9) ;
hence (FD . (x,y)) "\/" (FD . (y,z)) >= FD . (x,z) by A90, A91, LATTICE5:def 7; :: 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
A92: x in y and
A93: y in X by A1, TARSKI:def 4;
consider j being Element of NAT such that
A94: y = (S . j) `1 by A93;
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_extension2_of A1,d1 and
A95: S . j = [A1,d1] and
S . (j + 1) = [Aq1,dq1] by Def11;
[A1,d1] `2 = d1 ;
then d1 in { ((S . i) `2) where i is Element of NAT : verum } by A95;
then A96: d1 c= FD by ZFMISC_1:74;
reconsider x9 = x as Element of A1 by A92, A94, A95;
dom d1 = [:A1,A1:] by FUNCT_2:def 1;
hence FD . (x,x) = d1 . [x9,x9] by A96, GRFUNC_1:2
.= d1 . (x9,x9)
.= Bottom L by LATTICE5:def 6 ;
:: thesis: verum

end;

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