let R be Relation; for a, b, c being object st R reduces a,b & R reduces b,c holds
R reduces a,c
let a, b, c be object ; ( 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
and
A2:
p . (len p) = b
; REWRITE1:def 3 ( not R reduces b,c or R reduces a,c )
given q being RedSequence of R such that A3:
q . 1 = b
and
A4:
q . (len q) = c
; REWRITE1:def 3 R reduces a,c
reconsider r = p $^ q as RedSequence of R by A2, A3, Th8;
take
r
; REWRITE1:def 3 ( r . 1 = a & r . (len r) = c )
consider p1 being FinSequence, x being object such that
A5:
p = p1 ^ <*x*>
by FINSEQ_1:46;
0 + 1 <= len q
by NAT_1:13;
then
len q in Seg (len q)
by FINSEQ_1:1;
then A6:
len q in dom q
by FINSEQ_1:def 3;
A7:
r = p1 ^ q
by A5, Th2;
( p1 = {} or len p1 >= 0 + 1 )
by NAT_1:13;
then
( ( r = q & p = <*x*> ) or 1 in Seg (len p1) )
by A5, A7, FINSEQ_1:1, FINSEQ_1:34;
then
( 1 in dom p1 or ( len p = 1 & r = q ) )
by FINSEQ_1:40, FINSEQ_1:def 3;
then
( ( r . 1 = p1 . 1 & p1 . 1 = a ) or ( r . 1 = b & b = a ) )
by A1, A2, A3, A5, A7, FINSEQ_1:def 7;
hence
r . 1 = a
; r . (len r) = c
len r = (len p1) + (len q)
by A7, FINSEQ_1:22;
hence
r . (len r) = c
by A4, A7, A6, FINSEQ_1:def 7; verum