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 set ; :: 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) & e2 in the carrier of (Image f) ) and
A4: [x,y] in e1 "\/" e2 ; :: thesis:
Image f = subrelstr (rng f) by YELLOW_2:def 2;
then A5: the carrier of (Image f) = rng f by YELLOW_0:def 15;
then consider a being set such that
A6: a in dom f and
A7: e1 = f . a by A3, FUNCT_1:def 5;
consider b being set such that
A8: b in dom f and
A9: e2 = f . b by A3, A5, FUNCT_1:def 5;
reconsider a = a, b = b as Element of L by A6, A8;
field (e1 "\/" e2) = FS by ORDERS_1:97;
then reconsider u = x, v = y as Element of FS by A4, RELAT_1:30;
reconsider a = a, b = b as Element of L ;
consider e1' being Equivalence_Relation of FS such that
A10: e1' = f . a and
A11: for u, v being Element of FS holds
( [u,v] in e1' iff FD . u,v <= a ) by A1, Def9;
consider e2' being Equivalence_Relation of FS such that
A12: e2' = f . b and
A13: for u, v being Element of FS holds
( [u,v] in e2' iff FD . u,v <= b ) by A1, Def9;
consider e being Equivalence_Relation of FS such that
A14: e = f . (a "\/" b) and
A15: for u, v being Element of FS holds
( [u,v] in e iff FD . u,v <= a "\/" b ) by A1, Def9;
e = (f . a) "\/" (f . b) by A14, WAYBEL_6:2
.= e1 "\/" e2 by A7, A9, Th10 ;
then FD . u,v <= a "\/" b by A4, A15;
then consider z1, z2, z3 being Element of FS such that
A16: FD . u,z1 = a and
A17: FD . z2,z3 = a and
A18: FD . z1,z2 = b and
A19: FD . z3,v = b by A2, Th45;
defpred S₁[ set , set ] 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 ) );
A21: for m being Nat st m in Seg 5 holds
ex w being set st S₁[m,w]

proof

let m be Nat; :: thesis:
assume A22: m in Seg 5 ; :: thesis:

per cases by A22, Lm3;

suppose A23: m = 1 ; :: thesis:

take w = x; :: thesis:
thus S₁[m,w] by A23; :: thesis:

end;

suppose A24: m = 2 ; :: thesis:

take w = z1; :: thesis:
thus S₁[m,w] by A24; :: thesis:

end;

suppose A25: m = 3 ; :: thesis:

take w = z2; :: thesis:
thus S₁[m,w] by A25; :: thesis:

end;

suppose A26: m = 4 ; :: thesis:

take w = z3; :: thesis:
thus S₁[m,w] by A26; :: thesis:

end;

suppose A27: m = 5 ; :: thesis:

take w = y; :: thesis:
thus S₁[m,w] by A27; :: 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(A21);
then consider h being FinSequence such that
A28: dom h = Seg 5 and
A29: 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 ) ) ;
A30: ( 1 in Seg 5 & 2 in Seg 5 & 3 in Seg 5 & 4 in Seg 5 & 5 in Seg 5 ) ;
A31: len h = 5 by A28, FINSEQ_1:def 3;
rng h c= FS

proof

let w be set ; :: according to TARSKI:def 3 :: thesis:
assume w in rng h ; :: thesis:
then consider j being set such that
A32: ( j in dom h & w = h . j ) by FUNCT_1:def 5;

per cases by A28, A32, Lm3;

suppose j = 1 ; :: thesis:

then h . j = u by A29, A30;
hence w in FS by A32; :: thesis:

end;

suppose j = 2 ; :: thesis:

then h . j = z1 by A29, A30;
hence w in FS by A32; :: thesis:

end;

suppose j = 3 ; :: thesis:

then h . j = z2 by A29, A30;
hence w in FS by A32; :: thesis:

end;

suppose j = 4 ; :: thesis:

then h . j = z3 by A29, A30;
hence w in FS by A32; :: thesis:

end;

suppose j = 5 ; :: thesis:

then h . j = v by A29, A30;
hence w in FS by A32; :: thesis:

end;

then reconsider h = h as FinSequence of FS by FINSEQ_1:def 4;
len h <> 0 by A28, FINSEQ_1:def 3;
then reconsider h = h as non empty FinSequence of FS ;
take h ; :: thesis:
thus len h = 3 + 2 by A28, FINSEQ_1:def 3; :: thesis:
A33: h . 1 = x by A29, A30;
A34: h . (len h) = h . 5 by A28, FINSEQ_1:def 3
.= y by A29, A30 ;
for j being Element of NAT st 1 <= j & j < len h holds
( ( not j is even 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 A35: ( 1 <= j & j < len h ) ; :: thesis:

per cases by A31, A35, Lm2;

suppose j = 1 ; :: thesis:

then A36: (2 * 0 ) + 1 = j ;
[u,z1] in e1' by A11, A16;
then [(h . 1),z1] in e1' by A29, A30;
hence ( ( not j is even implies [(h . j),(h . (j + 1))] in e1 ) & ( j is even implies [(h . j),(h . (j + 1))] in e2 ) ) by A7, A10, A29, A30, A36; :: thesis:

end;

suppose j = 3 ; :: thesis:

then A37: (2 * 1) + 1 = j ;
[z2,z3] in e1' by A11, A17;
then [(h . 3),z3] in e1' by A29, A30;
hence ( ( not j is even implies [(h . j),(h . (j + 1))] in e1 ) & ( j is even implies [(h . j),(h . (j + 1))] in e2 ) ) by A7, A10, A29, A30, A37; :: thesis:

end;

suppose j = 2 ; :: thesis:

then A38: 2 * 1 = j ;
[z1,z2] in e2' by A13, A18;
then [(h . 2),z2] in e2' by A29, A30;
hence ( ( not j is even implies [(h . j),(h . (j + 1))] in e1 ) & ( j is even implies [(h . j),(h . (j + 1))] in e2 ) ) by A9, A12, A29, A30, A38; :: thesis:

end;

suppose j = 4 ; :: thesis:

then A39: 2 * 2 = j ;
[z3,v] in e2' by A13, A19;
then [(h . 4),v] in e2' by A29, A30;
hence ( ( not j is even implies [(h . j),(h . (j + 1))] in e1 ) & ( j is even implies [(h . j),(h . (j + 1))] in e2 ) ) by A9, A12, A29, A30, A39; :: thesis:

end;

hence x,y are_joint_by h,e1,e2 by A33, A34, Def3; :: thesis: