let R be Relation; :: thesis: R [*] is_transitive_in field R
set X = field R;
set S = R [*] ;

now

let x, y, z be set ; :: thesis: ( x in field R & y in field R & z in field R & [x,y] in R [*] & [y,z] in R [*] implies [x,z] in R [*] )
assume C7: ( x in field R & y in field R & z in field R ) ; :: thesis: ( [x,y] in R [*] & [y,z] in R [*] implies [x,z] in R [*] )
assume C0: ( [x,y] in R [*] & [y,z] in R [*] ) ; :: thesis: [x,z] in R [*]
consider p1 being FinSequence such that
C1: ( len p1 >= 1 & p1 . 1 = x & p1 . (len p1) = y & ( for i being Nat st i >= 1 & i < len p1 holds
[(p1 . i),(p1 . (i + 1))] in R ) ) by C0, FINSEQ_1:def 16;
consider m being Nat such that
C5: len p1 = m + 1 by C1, NAT_1:6;
consider p2 being FinSequence such that
C2: ( len p2 >= 1 & p2 . 1 = y & p2 . (len p2) = z & ( for i being Nat st i >= 1 & i < len p2 holds
[(p2 . i),(p2 . (i + 1))] in R ) ) by C0, FINSEQ_1:def 16;
C6: 1 in dom p2 by C2, FINSEQ_3:25;
reconsider l1 = len p1, l2 = len p2 as non zero Nat by C1, C2;
reconsider p11 = p1 | (Seg m) as FinSequence ;
set p = p11 ^ p2;
Z1: m + 0 < m + 1 by XREAL_1:8;
C21: len p11 = m by Z1, C5, FINSEQ_1:17;
Z11: m + l2 >= 0 + 1 by C2, XREAL_1:7;
C3: for n being Nat st n >= 1 & n <= len p2 holds
(p11 ^ p2) . (m + n) = p2 . n

proof

let n be Nat; :: thesis: ( n >= 1 & n <= len p2 implies (p11 ^ p2) . (m + n) = p2 . n )
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
D0: nn = n ;
assume ( n >= 1 & n <= len p2 ) ; :: thesis: (p11 ^ p2) . (m + n) = p2 . n
then n in Seg (len p2) by D0;
then n in dom p2 by FINSEQ_1:def 3;
hence (p11 ^ p2) . (m + n) = p2 . n by C21, FINSEQ_1:def 7; :: thesis: verum

end;

C11: (p11 ^ p2) . 1 = x

proof

per cases ( m = 0 or m <> 0 ) ;

suppose D0: m = 0 ; :: thesis: (p11 ^ p2) . 1 = x

thus (p11 ^ p2) . 1 = x by D0, C5, C1, C3, C2; :: thesis: verum

end;

suppose m <> 0 ; :: thesis: (p11 ^ p2) . 1 = x

then 0 + 1 <= m by INT_1:7;
then 1 in Seg m ;
then E0: 1 in dom p11 by Z1, C5, FINSEQ_1:17;
hence (p11 ^ p2) . 1 = p11 . 1 by FINSEQ_1:def 7
.= x by C1, E0, FUNCT_1:47 ;
:: thesis: verum

end;

end;

end;

l2 in Seg l2 by C2;
then l2 in dom p2 by FINSEQ_1:def 3;
then Z13: (p11 ^ p2) . ((len p11) + (len p2)) = z by C2, FINSEQ_1:def 7;
C13: for i being Nat st i >= 1 & i < len (p11 ^ p2) holds
[((p11 ^ p2) . i),((p11 ^ p2) . (i + 1))] in R

proof

let i be Nat; :: thesis: ( i >= 1 & i < len (p11 ^ p2) implies [((p11 ^ p2) . i),((p11 ^ p2) . (i + 1))] in R )
assume Z9: ( i >= 1 & i < len (p11 ^ p2) ) ; :: thesis: [((p11 ^ p2) . i),((p11 ^ p2) . (i + 1))] in R
then D1: ( i + 1 >= 1 & i >= 1 & i < len (p11 ^ p2) ) by NAT_1:11;

per cases ( i < m or i = m or i > m ) by XXREAL_0:1;

suppose i < m ; :: thesis: [((p11 ^ p2) . i),((p11 ^ p2) . (i + 1))] in R

then E1: ( i < l1 & i < m & i + 1 <= m ) by Z1, C5, INT_1:7, XXREAL_0:2;
then ( i in Seg m & i + 1 in Seg m ) by D1, FINSEQ_1:1;
then E0: ( i in dom p11 & i + 1 in dom p11 ) by Z1, C5, FINSEQ_1:17;
then ( (p11 ^ p2) . i = p11 . i & (p11 ^ p2) . (i + 1) = p11 . (i + 1) ) by FINSEQ_1:def 7;
then ( (p11 ^ p2) . i = p1 . i & (p11 ^ p2) . (i + 1) = p1 . (i + 1) ) by E0, FUNCT_1:47;
hence [((p11 ^ p2) . i),((p11 ^ p2) . (i + 1))] in R by C1, Z9, E1; :: thesis: verum

end;

suppose E0: i = m ; :: thesis: [((p11 ^ p2) . i),((p11 ^ p2) . (i + 1))] in R

E10: m in dom p11 by E0, Z9, C21, FINSEQ_3:25;
then E1: (p11 ^ p2) . m = p11 . m by FINSEQ_1:def 7
.= p1 . m by E10, FUNCT_1:47 ;
E2: (p11 ^ p2) . (m + 1) = p1 . (m + 1) by C1, C6, C5, C21, C2, FINSEQ_1:def 7;
thus [((p11 ^ p2) . i),((p11 ^ p2) . (i + 1))] in R by E0, E1, E2, C1, Z9, Z1, C5; :: thesis: verum

end;

suppose E4: i > m ; :: thesis: [((p11 ^ p2) . i),((p11 ^ p2) . (i + 1))] in R

then consider j being Nat such that
E3: i = m + j by NAT_1:10;
j <> 0 by E4, E3;
then Z12: j >= 0 + 1 by INT_1:7;
then E7: ( j >= 1 & j + 1 >= 1 + 0 ) by XREAL_1:7;
m + j < m + l2 by E3, Z9, C21, FINSEQ_1:22;
then E5: j < l2 by XREAL_1:7;
then E6: ( j <= l2 & j + 1 <= l2 ) by INT_1:7;
( j in Seg l2 & j + 1 in Seg l2 ) by E6, E7, FINSEQ_1:1;
then E0: ( j in dom p2 & j + 1 in dom p2 ) by FINSEQ_1:def 3;
E1: (p11 ^ p2) . i = p2 . j by E0, E3, C21, FINSEQ_1:def 7;
E2: (p11 ^ p2) . (i + 1) = (p11 ^ p2) . ((len p11) + (j + 1)) by E3, C21
.= p2 . (j + 1) by E0, FINSEQ_1:def 7 ;
thus [((p11 ^ p2) . i),((p11 ^ p2) . (i + 1))] in R by E1, E2, C2, E5, Z12; :: thesis: verum

end;

end;

end;

( x in field R & z in field R & len (p11 ^ p2) >= 1 & (p11 ^ p2) . 1 = x & (p11 ^ p2) . (len (p11 ^ p2)) = z & ( for i being Nat st i >= 1 & i < len (p11 ^ p2) holds
[((p11 ^ p2) . i),((p11 ^ p2) . (i + 1))] in R ) ) by C7, Z11, C21, C11, Z13, C13, FINSEQ_1:22;
hence [x,z] in R [*] by FINSEQ_1:def 16; :: thesis: verum

end;

hence R [*] is_transitive_in field R by RELAT_2:def 8; :: thesis: verum