let R be Relation; :: thesis: for a, b, c being set st R reduces a,b & R reduces b,c holds
R reduces a,c
let a, b, c be set ; :: thesis: ( R reduces a,b & R reduces b,c implies R reduces a,c )
given p being RedSequence of R such that A1: ( p . 1 = a & p . (len p) = b ) ; :: according to REWRITE1:def 3 :: thesis: ( not R reduces b,c or R reduces a,c )
given q being RedSequence of R such that A2: ( q . 1 = b & q . (len q) = c ) ; :: according to REWRITE1:def 3 :: thesis: R reduces a,c
reconsider r = p $^ q as RedSequence of R by A1, A2, Th9;
take r ; :: according to REWRITE1:def 3 :: thesis: ( r . 1 = a & r . (len r) = c )
consider p1 being FinSequence, x being set such that
A4: p = p1 ^ <*x*> by FINSEQ_1:63;
A5: r = p1 ^ q by A4, Th2;
then A6: len r = (len p1) + (len q) by FINSEQ_1:35;
( p1 = {} or len p1 >= 0 + 1 ) by NAT_1:13;
then ( ( r = q & p = <*x*> ) or 1 in Seg (len p1) ) by A4, A5, FINSEQ_1:3, FINSEQ_1:47;
then ( 1 in dom p1 or ( len p = 1 & r = q ) ) by FINSEQ_1:57, FINSEQ_1:def 3;
then ( ( r . 1 = p1 . 1 & p1 . 1 = a ) or ( r . 1 = b & b = a ) ) by A1, A2, A4, A5, FINSEQ_1:def 7;
hence r . 1 = a ; :: thesis: r . (len r) = c
0 + 1 <= len q by NAT_1:13;
then len q in Seg (len q) by FINSEQ_1:3;
then len q in dom q by FINSEQ_1:def 3;
hence r . (len r) = c by A2, A5, A6, FINSEQ_1:def 7; :: thesis: verum