let X be non empty set ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: ( ( 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 ; :: thesis: [(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; :: thesis: 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 ; :: thesis: [(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; :: thesis: 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; :: thesis: 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; :: thesis: verum