let X be non empty set ; for x being set
for o being Element of NAT
for R1, R2 being Relation
for f being non empty FinSequence of X st R1 is_reflexive_in X & R2 is_reflexive_in X & f = o |-> x holds
x,x are_joint_by f,R1,R2
let x be set ; for o being Element of NAT
for R1, R2 being Relation
for f being non empty FinSequence of X st R1 is_reflexive_in X & R2 is_reflexive_in X & f = o |-> x holds
x,x are_joint_by f,R1,R2
let o be Element of NAT ; for R1, R2 being Relation
for f being non empty FinSequence of X st R1 is_reflexive_in X & R2 is_reflexive_in X & f = o |-> x holds
x,x are_joint_by f,R1,R2
let R1, R2 be Relation; for f being non empty FinSequence of X st R1 is_reflexive_in X & R2 is_reflexive_in X & f = o |-> x holds
x,x are_joint_by f,R1,R2
let f be non empty FinSequence of X; ( R1 is_reflexive_in X & R2 is_reflexive_in X & f = o |-> x implies x,x are_joint_by f,R1,R2 )
assume that
A1:
R1 is_reflexive_in X
and
A2:
R2 is_reflexive_in X
and
A3:
f = o |-> x
; x,x are_joint_by f,R1,R2
A4:
dom f = Seg o
by A3;
then A5:
f . 1 = x
by A3, FINSEQ_5:6, FUNCOP_1:7;
A6:
for i being Element of NAT st 1 <= i & i < len f holds
( ( i is odd implies [(f . i),(f . (i + 1))] in R1 ) & ( i is even implies [(f . i),(f . (i + 1))] in R2 ) )
proof
let i be
Element of
NAT ;
( 1 <= i & i < len f implies ( ( i is odd implies [(f . i),(f . (i + 1))] in R1 ) & ( i is even implies [(f . i),(f . (i + 1))] in R2 ) ) )
assume that A7:
1
<= i
and A8:
i < len f
;
( ( i is odd implies [(f . i),(f . (i + 1))] in R1 ) & ( i is even implies [(f . i),(f . (i + 1))] in R2 ) )
A9:
(
i is
even implies
[(f . i),(f . (i + 1))] in R2 )
proof
( 1
<= i + 1 &
i + 1
<= len f )
by A7, A8, NAT_1:13;
then
i + 1
in Seg (len f)
;
then
i + 1
in Seg o
by A3, CARD_1:def 7;
then A10:
f . (i + 1) = x
by A3, FUNCOP_1:7;
assume
i is
even
;
[(f . i),(f . (i + 1))] in R2
i <= o
by A3, A8, CARD_1:def 7;
then
i in Seg o
by A7;
then A11:
f . i = x
by A3, FUNCOP_1:7;
x in X
by A4, A5, FINSEQ_2:11, FINSEQ_5:6;
hence
[(f . i),(f . (i + 1))] in R2
by A2, A10, A11, RELAT_2:def 1;
verum
end;
(
i is
odd implies
[(f . i),(f . (i + 1))] in R1 )
proof
( 1
<= i + 1 &
i + 1
<= len f )
by A7, A8, NAT_1:13;
then
i + 1
in Seg (len f)
;
then
i + 1
in Seg o
by A3, CARD_1:def 7;
then A12:
f . (i + 1) = x
by A3, FUNCOP_1:7;
assume
i is
odd
;
[(f . i),(f . (i + 1))] in R1
i <= o
by A3, A8, CARD_1:def 7;
then
i in Seg o
by A7;
then A13:
f . i = x
by A3, FUNCOP_1:7;
x in X
by A4, A5, FINSEQ_2:11, FINSEQ_5:6;
hence
[(f . i),(f . (i + 1))] in R1
by A1, A12, A13, RELAT_2:def 1;
verum
end;
hence
( (
i is
odd implies
[(f . i),(f . (i + 1))] in R1 ) & (
i is
even implies
[(f . i),(f . (i + 1))] in R2 ) )
by A9;
verum
end;
len f in Seg o
by A4, FINSEQ_5:6;
then
f . (len f) = x
by A3, FUNCOP_1:7;
hence
x,x are_joint_by f,R1,R2
by A5, A6; verum