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:
let FD be distance_function of FS,L; :: thesis:
let f be Homomorphism of L,(EqRelLATT FS); :: thesis:
let x, y be Element of FS; :: thesis:
let e1, e2 be Equivalence_Relation of FS; :: thesis:
let x, y be object ; :: thesis:
assume that
A1: f = alpha FD and
A2: ( FS = union { ((S . i) `1) where i is Element of NAT : verum } & FD = union { ((S . i) `2) where i is Element of NAT : verum } ) and
A3: e1 in the carrier of (Image f) and
A4: e2 in the carrier of (Image f) and
A5: [x,y] in e1 "\/" e2 ; :: thesis:
A6: 4 in Seg 5 ;
field (e1 "\/" e2) = FS by ORDERS_1:12;
then reconsider u = x, v = y as Element of FS by A5, RELAT_1:15;
A7: 1 in Seg 5 ;
Image f = subrelstr (rng f) by YELLOW_2:def 2;
then A8: the carrier of (Image f) = rng f by YELLOW_0:def 15;
then consider a being object such that
A9: a in dom f and
A10: e1 = f . a by A3, FUNCT_1:def 3;
consider b being object such that
A11: b in dom f and
A12: e2 = f . b by A4, A8, FUNCT_1:def 3;
reconsider a = a, b = b as Element of L by A9, A11;
reconsider a = a, b = b as Element of L ;
consider e being Equivalence_Relation of FS such that
A13: e = f . (a "\/" b) and
A14: for u, v being Element of FS holds
( [u,v] in e iff FD . (u,v) <= a "\/" b ) by A1, Def8;
consider e19 being Equivalence_Relation of FS such that
A15: e19 = f . a and
A16: for u, v being Element of FS holds
( [u,v] in e19 iff FD . (u,v) <= a ) by A1, Def8;
consider e29 being Equivalence_Relation of FS such that
A17: e29 = f . b and
A18: for u, v being Element of FS holds
( [u,v] in e29 iff FD . (u,v) <= b ) by A1, Def8;
A19: 3 in Seg 5 ;
e = (f . a) "\/" (f . b) by A13, WAYBEL_6:2
.= e1 "\/" e2 by A10, A12, Th10 ;
then FD . (u,v) <= a "\/" b by A5, A14;
then consider z1, z2, z3 being Element of FS such that
A20: FD . (u,z1) = a and
A21: FD . (z2,z3) = a and
A22: FD . (z1,z2) = b and
A23: FD . (z3,v) = b by A2, Th42;
defpred S₁[ set , object ] means ( ( $1 = 1 implies $2 = u ) & ( $1 = 2 implies $2 = z1 ) & ( $1 = 3 implies $2 = z2 ) & ( $1 = 4 implies $2 = z3 ) & ( $1 = 5 implies $2 = v ) );
A24: for m being Nat st m in Seg 5 holds
ex w being object st S₁[m,w]

let m be Nat; :: thesis:
assume m in Seg 5 ; :: thesis:
then not not m = 1 & ... & not m = 5 by Lm3;

suppose A25: m = 1 ; :: thesis:

take x ; :: thesis:
thus S₁[m,x] by A25; :: thesis:

end;

suppose A26: m = 2 ; :: thesis:

take z1 ; :: thesis:
thus S₁[m,z1] by A26; :: thesis:

end;

suppose A27: m = 3 ; :: thesis:

take z2 ; :: thesis:
thus S₁[m,z2] by A27; :: thesis:

end;

suppose A28: m = 4 ; :: thesis:

take z3 ; :: thesis:
thus S₁[m,z3] by A28; :: thesis:

end;

suppose A29: m = 5 ; :: thesis:

take y ; :: thesis:
thus S₁[m,y] by A29; :: thesis:

end;

ex p being FinSequence st
( dom p = Seg 5 & ( for k being Nat st k in Seg 5 holds
S₁[k,p . k] ) ) from FINSEQ_1:sch 1(A24);
then consider h being FinSequence such that
A30: dom h = Seg 5 and
A31: for m being Nat st m in Seg 5 holds
( ( m = 1 implies h . m = u ) & ( m = 2 implies h . m = z1 ) & ( m = 3 implies h . m = z2 ) & ( m = 4 implies h . m = z3 ) & ( m = 5 implies h . m = v ) ) ;
A32: len h = 5 by A30, FINSEQ_1:def 3;
A33: 5 in Seg 5 ;
A34: 2 in Seg 5 ;
rng h c= FS

proof

let w be object ; :: according to TARSKI:def 3 :: thesis:
assume w in rng h ; :: thesis:
then consider j being object such that
A35: j in dom h and
A36: w = h . j by FUNCT_1:def 3;
not not j = 1 & ... & not j = 5 by A30, A35, Lm3;

per cases ;

suppose j = 1 ; :: thesis:

then h . j = u by A31, A7;
hence w in FS by A36; :: thesis:

end;

suppose j = 2 ; :: thesis:

then h . j = z1 by A31, A34;
hence w in FS by A36; :: thesis:

end;

suppose j = 3 ; :: thesis:

then h . j = z2 by A31, A19;
hence w in FS by A36; :: thesis:

end;

suppose j = 4 ; :: thesis:

then h . j = z3 by A31, A6;
hence w in FS by A36; :: thesis:

end;

suppose j = 5 ; :: thesis:

then h . j = v by A31, A33;
hence w in FS by A36; :: thesis:

end;

then reconsider h = h as FinSequence of FS by FINSEQ_1:def 4;
reconsider h = h as non empty FinSequence of FS by A30;
A37: h . 1 = x by A31, A7;
A38: for j being Element of NAT st 1 <= j & j < len h holds
( ( j is odd implies [(h . j),(h . (j + 1))] in e1 ) & ( j is even implies [(h . j),(h . (j + 1))] in e2 ) )

proof

let j be Element of NAT ; :: thesis:
assume ( 1 <= j & j < len h ) ; :: thesis:
then not not j = 1 & ... & not j = 4 by A32, Lm2;

per cases ;

suppose A39: j = 1 ; :: thesis:

[u,z1] in e19 by A16, A20;
then [(h . 1),z1] in e19 by A31, A7;
hence ( ( j is odd implies [(h . j),(h . (j + 1))] in e1 ) & ( j is even implies [(h . j),(h . (j + 1))] in e2 ) ) by A10, A15, A31, A34, A39; :: thesis:

end;

suppose A40: j = 3 ; :: thesis:

[z2,z3] in e19 by A16, A21;
then A41: [(h . 3),z3] in e19 by A31, A19;
(2 * 1) + 1 = j by A40;
hence ( ( j is odd implies [(h . j),(h . (j + 1))] in e1 ) & ( j is even implies [(h . j),(h . (j + 1))] in e2 ) ) by A10, A15, A31, A6, A41; :: thesis:

end;

suppose A42: j = 2 ; :: thesis:

[z1,z2] in e29 by A18, A22;
then A43: [(h . 2),z2] in e29 by A31, A34;
2 * 1 = j by A42;
hence ( ( j is odd implies [(h . j),(h . (j + 1))] in e1 ) & ( j is even implies [(h . j),(h . (j + 1))] in e2 ) ) by A12, A17, A31, A19, A43; :: thesis:

end;

suppose A44: j = 4 ; :: thesis:

[z3,v] in e29 by A18, A23;
then A45: [(h . 4),v] in e29 by A31, A6;
2 * 2 = j by A44;
hence ( ( j is odd implies [(h . j),(h . (j + 1))] in e1 ) & ( j is even implies [(h . j),(h . (j + 1))] in e2 ) ) by A12, A17, A31, A33, A45; :: thesis:

end;

take h ; :: thesis:
thus len h = 3 + 2 by A30, FINSEQ_1:def 3; :: thesis:
h . (len h) = h . 5 by A30, FINSEQ_1:def 3
.= y by A31, A33 ;
hence x,y are_joint_by h,e1,e2 by A37, A38; :: thesis: