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

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, Th32;
hence x,y are_c=-comparable by XBOOLE_0:def 9; :: thesis: verum

end;

then A6: { ((S . i) `2) where i is Element of NAT : verum } is c=-linear by ORDINAL1:def 8;
{ ((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: ( 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 Def12;
A9 = (S . j) `1 by A8, MCART_1:def 1;
then A9 in { ((S . i) `1) where i is Element of NAT : verum } ;
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, MCART_1:def 2;
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>[ set , set ] 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 set ; :: 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 set ; :: 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 set st x in NAT holds
ex y being set st S<sub>1</sub>[x,y] ;
consider F being Function such that
A16: dom F = NAT and
A17: for x being set 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 set ; :: 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 set 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 set ; :: 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 set ; :: 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_extension2_of A1,d1 and
A22: S . j = [A1,d1] and
S . (j + 1) = [Aq1,dq1] by Def12;
(S . j) `2 = d1 by A22, MCART_1:def 2;
hence F . x is set by A17; :: 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 set ; :: 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 set 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_extension2_of A1,d1 and
A27: S . j = [A1,d1] and
S . (j + 1) = [Aq1,dq1] by Def12;
A28: (S . j) `2 = d1 by A27, MCART_1:def 2;
A29: (S . j) `1 = A1 by A27, MCART_1:def 1;
x = dom (F . j) by A25, A26, FUNCT_6:22
.= dom d1 by A17, A28
.= [:((S . j) `1),((S . j) `1):] by A29, 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 set ; :: 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 Def12;
A32: (S . j) `2 = d1 by A31, MCART_1:def 2;
j in NAT ;
then A33: j in dom (doms F) by A16, FUNCT_6:59;
(S . j) `1 = A1 by A31, MCART_1:def 1;
then x = dom d1 by A30, FUNCT_2:def 1
.= dom (F . j) by A17, A32
.= (doms F) . j by A16, FUNCT_6:22 ;
hence x in rng (doms F) by A33, FUNCT_1:def 3; :: thesis: verum

end;

now

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, Th31;
hence x,y are_c=-comparable by XBOOLE_0:def 9; :: thesis: verum

end;

then X is c=-linear by ORDINAL1:def 8;
then [:FS,FS:] = union (rng (doms F)) by A1, A23, A11, LATTICE5:3
.= dom FD by A18, LATTICE5:1 ;
then reconsider FD = FD as BiFunction of FS,L by A10, 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 Def12;
A43: x in A1 by A39, A41, A42, MCART_1:def 1;
A44: (S . k) `1 = A1 by A42, MCART_1:def 1;
(S . k) `2 = d1 by A42, MCART_1:def 2;
then d1 in { ((S . i) `2) where i is Element of NAT : verum } ;
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 Def12;
A50: y in A2 by A46, A48, A49, MCART_1:def 1;
A51: (S . l) `1 = A2 by A49, MCART_1:def 1;
(S . l) `2 = d2 by A49, MCART_1:def 2;
then d2 in { ((S . i) `2) where i is Element of NAT : verum } ;
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 A44, A51, Th31;
then reconsider x9 = x, y9 = y as Element of A2 by A43, A46, A48, A49, MCART_1:def 1;
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 A44, A51, Th31;
then reconsider x9 = x, y9 = y as Element of A1 by A39, A41, A42, A50, MCART_1:def 1;
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 Def12;
A60: x in A1 by A56, A58, A59, MCART_1:def 1;
(S . k) `2 = d1 by A59, MCART_1:def 2;
then d1 in { ((S . i) `2) where i is Element of NAT : verum } ;
then A61: d1 c= FD by ZFMISC_1:74;
A62: dom d1 = [:A1,A1:] by FUNCT_2:def 1;
A63: (S . k) `1 = A1 by A59, MCART_1: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 Def12;
A68: y in A2 by A64, A66, A67, MCART_1:def 1;
(S . l) `2 = d2 by A67, MCART_1:def 2;
then d2 in { ((S . i) `2) where i is Element of NAT : verum } ;
then A69: d2 c= FD by ZFMISC_1:74;
A70: dom d2 = [:A2,A2:] by FUNCT_2:def 1;
A71: (S . l) `1 = A2 by A67, MCART_1: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 Def12;
A76: z in A3 by A72, A74, A75, MCART_1:def 1;
A77: (S . n) `1 = A3 by A75, MCART_1:def 1;
(S . n) `2 = d3 by A75, MCART_1:def 2;
then d3 in { ((S . i) `2) where i is Element of NAT : verum } ;
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 A63, A71, Th31;
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 A71, A77, Th31;
then A1 c= A3 by A80, XBOOLE_1:1;
then reconsider x9 = x, y9 = y, z9 = z as Element of A3 by A60, A68, A72, A74, A75, A81, MCART_1:def 1;
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 A71, A77, Th31;
then reconsider x9 = x, y9 = y, z9 = z as Element of A2 by A60, A64, A66, A67, A76, A80, MCART_1:def 1;
A84: FD . (y,z) = d2 . [y9,z9] by A69, A70, GRFUNC_1:2
.= d2 . (y9,z9) ;
A85: FD . (x,z) = d2 . [x9,z9] by A69, A70, GRFUNC_1:2
.= d2 . (x9,z9) ;
FD . (x,y) = d2 . [x9,y9] by A69, A70, 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 A63, A71, Th31;
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 A63, A77, Th31;
then A2 c= A3 by A86, XBOOLE_1:1;
then reconsider x9 = x, y9 = y, z9 = z as Element of A3 by A60, A68, A72, A74, A75, A87, MCART_1:def 1;
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 A63, A77, Th31;
then reconsider x9 = x, y9 = y, z9 = z as Element of A1 by A56, A58, A59, A68, A76, A86, MCART_1:def 1;
A90: FD . (y,z) = d1 . [y9,z9] by A61, A62, GRFUNC_1:2
.= d1 . (y9,z9) ;
A91: FD . (x,z) = d1 . [x9,z9] by A61, A62, GRFUNC_1:2
.= d1 . (x9,z9) ;
FD . (x,y) = d1 . [x9,y9] by A61, A62, 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 Def12;
(S . j) `2 = d1 by A95, MCART_1:def 2;
then d1 in { ((S . i) `2) where i is Element of NAT : verum } ;
then A96: d1 c= FD by ZFMISC_1:74;
reconsider x9 = x as Element of A1 by A92, A94, A95, MCART_1:def 1;
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