let X be non empty set ; :: thesis: for x, y being set
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 set ; :: 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 & 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 A3:
( len f = n & 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 )
A4:
f . (len f) = y
by A3, Def3;
per cases
( n < m or n = m )
by A1, XXREAL_0:1;
suppose A5:
n < m
;
:: thesis: ex h being non empty FinSequence of X st
( len h = m & x,y are_joint_by h,R1,R2 )reconsider i =
m - n as
Element of
NAT by A1, INT_1:18;
A6:
i > 0
by A5, XREAL_1:52;
len f in dom f
by FINSEQ_5:6;
then
y in rng f
by A4, FUNCT_1:def 5;
then reconsider y' =
y as
Element of
X ;
reconsider g =
i |-> y' as
FinSequence of
X ;
len g <> 0
by A6;
then reconsider g =
g as non
empty FinSequence of
X ;
A7:
( 1
in dom g &
len g in dom g )
by FINSEQ_5:6;
A8:
y,
y are_joint_by g,
R1,
R2
by A2, Th12;
reconsider h =
f ^ g as non
empty FinSequence of
X ;
take
h
;
:: thesis: ( len h = m & x,y are_joint_by h,R1,R2 )thus len h =
(len f) + (len g)
by FINSEQ_1:35
.=
n + (m - n)
by A3, FINSEQ_1:def 18
.=
m
;
:: thesis: x,y are_joint_by h,R1,R2A9:
len g = m - n
by FINSEQ_1:def 18;
thus
x,
y are_joint_by h,
R1,
R2
:: thesis: verumproof
rng f <> {}
;
then
1
in dom f
by FINSEQ_3:34;
hence h . 1 =
f . 1
by FINSEQ_1:def 7
.=
x
by A3, Def3
;
:: according to LATTICE5:def 3 :: thesis: ( h . (len h) = y & ( for i being Element of NAT st 1 <= i & i < len h holds
( ( not i is even 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:35
.=
g . (len g)
by A7, FINSEQ_1:def 7
.=
y
by A8, Def3
;
:: thesis: for i being Element of NAT st 1 <= i & i < len h holds
( ( not i is even 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 ( ( not j is even implies [(h . j),(h . (j + 1))] in R1 ) & ( j is even implies [(h . j),(h . (j + 1))] in R2 ) ) )
assume A10:
( 1
<= j &
j < len h )
;
:: thesis: ( ( not j is even implies [(h . j),(h . (j + 1))] in R1 ) & ( j is even implies [(h . j),(h . (j + 1))] in R2 ) )
A11:
dom f = Seg (len f)
by FINSEQ_1:def 3;
thus
( not
j is
even implies
[(h . j),(h . (j + 1))] in R1 )
:: thesis: ( j is even implies [(h . j),(h . (j + 1))] in R2 )proof
assume A12:
not
j is
even
;
:: 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 A10, Lm1, FINSEQ_1:35;
suppose A17:
(
(len f) + 1
<= j &
j < (len f) + (len g) )
;
:: thesis: [(h . j),(h . (j + 1))] in R1then A18:
1
<= j - (len f)
by XREAL_1:21;
A19:
j - (len f) < ((len f) + (len g)) - (len f)
by A17, XREAL_1:11;
0 < j - (len f)
by A18, XXREAL_0:2;
then A20:
0 + (len f) < (j - (len f)) + (len f)
by XREAL_1:8;
then reconsider k =
j - (len f) as
Element of
NAT by INT_1:18;
A21:
( 1
<= k + 1 &
k + 1
<= len g )
by A18, A19, NAT_1:13;
k in Seg (len g)
by A18, A19;
then A22:
g . k = y
by A9, FUNCOP_1:13;
k + 1
in Seg (len g)
by A21;
then A23:
g . (k + 1) = y
by A9, FUNCOP_1:13;
A24:
j < j + 1
by XREAL_1:31;
j + 1
<= (len f) + (len g)
by A17, NAT_1:13;
then
(
len f < j + 1 &
j + 1
<= len h )
by A20, A24, FINSEQ_1:35, XXREAL_0:2;
then A25:
h . (j + 1) =
g . ((j + 1) - (len f))
by FINSEQ_1:37
.=
g . (k + 1)
;
h . j = y
by A17, A22, FINSEQ_1:36;
hence
[(h . j),(h . (j + 1))] in R1
by A2, A23, A25, RELAT_2:def 1;
:: thesis: verum end;
end;
assume A26:
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 A10, Lm1, FINSEQ_1:35;
suppose A31:
(
(len f) + 1
<= j &
j < (len f) + (len g) )
;
:: thesis: [(h . j),(h . (j + 1))] in R2then A32:
1
<= j - (len f)
by XREAL_1:21;
A33:
j - (len f) < ((len f) + (len g)) - (len f)
by A31, XREAL_1:11;
0 < j - (len f)
by A32, XXREAL_0:2;
then A34:
0 + (len f) < (j - (len f)) + (len f)
by XREAL_1:8;
then reconsider k =
j - (len f) as
Element of
NAT by INT_1:18;
A35:
( 1
<= k + 1 &
k + 1
<= len g )
by A32, A33, NAT_1:13;
k in Seg (len g)
by A32, A33;
then A36:
g . k = y
by A9, FUNCOP_1:13;
k + 1
in Seg (len g)
by A35;
then A37:
g . (k + 1) = y
by A9, FUNCOP_1:13;
A38:
j < j + 1
by XREAL_1:31;
j + 1
<= (len f) + (len g)
by A31, NAT_1:13;
then
(
len f < j + 1 &
j + 1
<= len h )
by A34, A38, FINSEQ_1:35, XXREAL_0:2;
then A39:
h . (j + 1) =
g . ((j + 1) - (len f))
by FINSEQ_1:37
.=
g . (k + 1)
;
h . j = y
by A31, A36, FINSEQ_1:36;
hence
[(h . j),(h . (j + 1))] in R2
by A2, A37, A39, RELAT_2:def 1;
:: thesis: verum end;
end; end;