let X be non empty set ; :: thesis: for x, y being object
for R1, R2 being Relation
for n, m being Element of NAT st n <= m & R1 is_reflexive_in X & R2 is_reflexive_in X & ex f being non empty FinSequence of X st
( len f = n & x,y are_joint_by f,R1,R2 ) holds
ex h being non empty FinSequence of X st
( len h = m & x,y are_joint_by h,R1,R2 )
let x, y be object ; :: thesis: for R1, R2 being Relation
for n, m being Element of NAT st n <= m & R1 is_reflexive_in X & R2 is_reflexive_in X & ex f being non empty FinSequence of X st
( len f = n & x,y are_joint_by f,R1,R2 ) holds
ex h being non empty FinSequence of X st
( len h = m & x,y are_joint_by h,R1,R2 )
let R1, R2 be Relation; :: thesis: for n, m being Element of NAT st n <= m & R1 is_reflexive_in X & R2 is_reflexive_in X & ex f being non empty FinSequence of X st
( len f = n & x,y are_joint_by f,R1,R2 ) holds
ex h being non empty FinSequence of X st
( len h = m & x,y are_joint_by h,R1,R2 )
let n, m be Element of NAT ; :: thesis: ( n <= m & R1 is_reflexive_in X & R2 is_reflexive_in X & ex f being non empty FinSequence of X st
( len f = n & x,y are_joint_by f,R1,R2 ) implies ex h being non empty FinSequence of X st
( len h = m & x,y are_joint_by h,R1,R2 ) )
assume that
A1: n <= m and
A2: R1 is_reflexive_in X and
A3: R2 is_reflexive_in X ; :: thesis: ( for f being non empty FinSequence of X holds
( not len f = n or not x,y are_joint_by f,R1,R2 ) or ex h being non empty FinSequence of X st
( len h = m & x,y are_joint_by h,R1,R2 ) )
given f being non empty FinSequence of X such that A4: len f = n and
A5: x,y are_joint_by f,R1,R2 ; :: thesis: ex h being non empty FinSequence of X st
( len h = m & x,y are_joint_by h,R1,R2 )
A6: f . (len f) = y by A5;

per cases ( n < m or n = m ) by A1, XXREAL_0:1;

suppose A7: n < m ; :: thesis: ex h being non empty FinSequence of X st
( len h = m & x,y are_joint_by h,R1,R2 )

len f in dom f by FINSEQ_5:6;
then y in rng f by A6, FUNCT_1:def 3;
then reconsider y9 = y as Element of X ;
reconsider i = m - n as Element of NAT by A1, INT_1:5;
reconsider g = i |-> y9 as FinSequence of X ;
i > 0 by A7, XREAL_1:50;
then reconsider g = g as non empty FinSequence of X ;
A8: 1 in dom g by FINSEQ_5:6;
reconsider h = f ^ g as non empty FinSequence of X ;
take h ; :: thesis: ( len h = m & x,y are_joint_by h,R1,R2 )
A9: len g = m - n by CARD_1:def 7;
A10: y,y are_joint_by g,R1,R2 by A2, A3, Th11;
thus len h = (len f) + (len g) by FINSEQ_1:22
.= n + (m - n) by A4, CARD_1:def 7
.= m ; :: thesis: x,y are_joint_by h,R1,R2
A11: len g in dom g by FINSEQ_5:6;
thus x,y are_joint_by h,R1,R2 :: thesis: verum

proof

rng f <> {} ;
then 1 in dom f by FINSEQ_3:32;
hence h . 1 = f . 1 by FINSEQ_1:def 7
.= x by A5 ;
:: according to LATTICE5:def 3 :: thesis: ( h . (len h) = y & ( for i being Element of NAT st 1 <= i & i < len h holds
( ( i is odd implies [(h . i),(h . (i + 1))] in R1 ) & ( i is even implies [(h . i),(h . (i + 1))] in R2 ) ) ) )
thus h . (len h) = h . ((len f) + (len g)) by FINSEQ_1:22
.= g . (len g) by A11, FINSEQ_1:def 7
.= y by A10 ; :: thesis: for i being Element of NAT st 1 <= i & i < len h holds
( ( i is odd implies [(h . i),(h . (i + 1))] in R1 ) & ( i is even implies [(h . i),(h . (i + 1))] in R2 ) )
let j be Element of NAT ; :: thesis: ( 1 <= j & j < len h implies ( ( j is odd implies [(h . j),(h . (j + 1))] in R1 ) & ( j is even implies [(h . j),(h . (j + 1))] in R2 ) ) )
A12: dom f = Seg (len f) by FINSEQ_1:def 3;
assume A13: ( 1 <= j & j < len h ) ; :: thesis: ( ( j is odd implies [(h . j),(h . (j + 1))] in R1 ) & ( j is even implies [(h . j),(h . (j + 1))] in R2 ) )
thus ( j is odd implies [(h . j),(h . (j + 1))] in R1 ) :: thesis: ( j is even implies [(h . j),(h . (j + 1))] in R2 )

proof

assume A14: j is odd ; :: thesis: [(h . j),(h . (j + 1))] in R1

per cases ( ( 1 <= j & j < len f ) or j = len f or ( (len f) + 1 <= j & j < (len f) + (len g) ) ) by A13, Lm1, FINSEQ_1:22;

suppose A15: ( 1 <= j & j < len f ) ; :: thesis: [(h . j),(h . (j + 1))] in R1

then ( 1 <= j + 1 & j + 1 <= len f ) by NAT_1:13;
then j + 1 in dom f by A12;
then A16: f . (j + 1) = h . (j + 1) by FINSEQ_1:def 7;
j in dom f by A12, A15;
then f . j = h . j by FINSEQ_1:def 7;
hence [(h . j),(h . (j + 1))] in R1 by A5, A14, A15, A16; :: thesis: verum

end;

suppose A17: j = len f ; :: thesis: [(h . j),(h . (j + 1))] in R1

then j in dom f by FINSEQ_5:6;
then A18: h . j = y by A6, A17, FINSEQ_1:def 7;
h . (j + 1) = g . 1 by A8, A17, FINSEQ_1:def 7
.= y by A10 ;
hence [(h . j),(h . (j + 1))] in R1 by A2, A18, RELAT_2:def 1; :: thesis: verum

end;

suppose A19: ( (len f) + 1 <= j & j < (len f) + (len g) ) ; :: thesis: [(h . j),(h . (j + 1))] in R1

then j + 1 <= (len f) + (len g) by NAT_1:13;
then A20: j + 1 <= len h by FINSEQ_1:22;
A21: 1 <= j - (len f) by A19, XREAL_1:19;
then 0 < j - (len f) by XXREAL_0:2;
then A22: 0 + (len f) < (j - (len f)) + (len f) by XREAL_1:6;
then reconsider k = j - (len f) as Element of NAT by INT_1:5;
A23: j - (len f) < ((len f) + (len g)) - (len f) by A19, XREAL_1:9;
then A24: k + 1 <= len g by NAT_1:13;
j < j + 1 by XREAL_1:29;
then len f < j + 1 by A22, XXREAL_0:2;
then A25: h . (j + 1) = g . ((j + 1) - (len f)) by A20, FINSEQ_1:24
.= g . (k + 1) ;
1 <= k + 1 by A21, NAT_1:13;
then k + 1 in Seg (len g) by A24;
then A26: g . (k + 1) = y by A9, FUNCOP_1:7;
k in Seg (len g) by A21, A23;
then g . k = y by A9, FUNCOP_1:7;
then h . j = y by A19, FINSEQ_1:23;
hence [(h . j),(h . (j + 1))] in R1 by A2, A26, A25, RELAT_2:def 1; :: thesis: verum

end;

end;

end;

assume A27: j is even ; :: thesis: [(h . j),(h . (j + 1))] in R2

per cases ( ( 1 <= j & j < len f ) or j = len f or ( (len f) + 1 <= j & j < (len f) + (len g) ) ) by A13, Lm1, FINSEQ_1:22;

suppose A28: ( 1 <= j & j < len f ) ; :: thesis: [(h . j),(h . (j + 1))] in R2

then ( 1 <= j + 1 & j + 1 <= len f ) by NAT_1:13;
then j + 1 in dom f by A12;
then A29: f . (j + 1) = h . (j + 1) by FINSEQ_1:def 7;
j in dom f by A12, A28;
then f . j = h . j by FINSEQ_1:def 7;
hence [(h . j),(h . (j + 1))] in R2 by A5, A27, A28, A29; :: thesis: verum

end;

suppose A30: j = len f ; :: thesis: [(h . j),(h . (j + 1))] in R2

then j in dom f by FINSEQ_5:6;
then A31: h . j = y by A6, A30, FINSEQ_1:def 7;
h . (j + 1) = g . 1 by A8, A30, FINSEQ_1:def 7
.= y by A10 ;
hence [(h . j),(h . (j + 1))] in R2 by A3, A31, RELAT_2:def 1; :: thesis: verum

end;

suppose A32: ( (len f) + 1 <= j & j < (len f) + (len g) ) ; :: thesis: [(h . j),(h . (j + 1))] in R2

then j + 1 <= (len f) + (len g) by NAT_1:13;
then A33: j + 1 <= len h by FINSEQ_1:22;
A34: 1 <= j - (len f) by A32, XREAL_1:19;
then 0 < j - (len f) by XXREAL_0:2;
then A35: 0 + (len f) < (j - (len f)) + (len f) by XREAL_1:6;
then reconsider k = j - (len f) as Element of NAT by INT_1:5;
A36: j - (len f) < ((len f) + (len g)) - (len f) by A32, XREAL_1:9;
then A37: k + 1 <= len g by NAT_1:13;
j < j + 1 by XREAL_1:29;
then len f < j + 1 by A35, XXREAL_0:2;
then A38: h . (j + 1) = g . ((j + 1) - (len f)) by A33, FINSEQ_1:24
.= g . (k + 1) ;
1 <= k + 1 by A34, NAT_1:13;
then k + 1 in Seg (len g) by A37;
then A39: g . (k + 1) = y by A9, FUNCOP_1:7;
k in Seg (len g) by A34, A36;
then g . k = y by A9, FUNCOP_1:7;
then h . j = y by A32, FINSEQ_1:23;
hence [(h . j),(h . (j + 1))] in R2 by A3, A39, A38, RELAT_2:def 1; :: thesis: verum

end;

end;

end;

end;

suppose n = m ; :: thesis: ex h being non empty FinSequence of X st
( len h = m & x,y are_joint_by h,R1,R2 )

hence ex h being non empty FinSequence of X st
( len h = m & x,y are_joint_by h,R1,R2 ) by A4, A5; :: thesis: verum

end;

end;