let R be Relation; :: thesis: R [*] is_transitive_in field R
set X = field R;
set S = R [*] ;
now :: thesis: for x, y, z being object st x in field R & y in field R & z in field R & [x,y] in R [*] & [y,z] in R [*] holds
[x,z] in R [*]
let x, y, z be object ; :: 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 A1: ( 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 A2: ( [x,y] in R [*] & [y,z] in R [*] ) ; :: thesis: [x,z] in R [*]
consider p1 being FinSequence such that
A3: ( 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 A2, FINSEQ_1:def 16;
consider m being Nat such that
A4: len p1 = m + 1 by NAT_1:6, A3;
consider p2 being FinSequence such that
A5: ( 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 A2, FINSEQ_1:def 16;
A6: 1 in dom p2 by FINSEQ_3:25, A5;
reconsider l1 = len p1, l2 = len p2 as non zero Nat by A3, A5;
reconsider p11 = p1 | (Seg m) as FinSequence ;
set p = p11 ^ p2;
A7: m + 0 < m + 1 by XREAL_1:8;
A8: len p11 = m by A7, A4, FINSEQ_1:17;
A9: m + l2 >= 0 + 1 by A5, XREAL_1:7;
A10: 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;
assume ( n >= 1 & n <= len p2 ) ; :: thesis: (p11 ^ p2) . (m + n) = p2 . n
then n in Seg (len p2) ;
then n in dom p2 by FINSEQ_1:def 3;
hence (p11 ^ p2) . (m + n) = p2 . n by FINSEQ_1:def 7, A8; :: thesis: verum
end;
A11: (p11 ^ p2) . 1 = x
proof
per cases ( m = 0 or m <> 0 ) ;
suppose A12: m = 0 ; :: thesis: (p11 ^ p2) . 1 = x
thus (p11 ^ p2) . 1 = x by A12, A4, A3, A10, A5; :: 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 A13: 1 in dom p11 by A7, A4, FINSEQ_1:17;
hence (p11 ^ p2) . 1 = p11 . 1 by FINSEQ_1:def 7
.= x by A3, FUNCT_1:47, A13 ;
:: thesis: verum
end;
end;
end;
l2 in Seg l2 by A5;
then l2 in dom p2 by FINSEQ_1:def 3;
then A14: (p11 ^ p2) . ((len p11) + (len p2)) = z by FINSEQ_1:def 7, A5;
A15: 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 A16: ( i >= 1 & i < len (p11 ^ p2) ) ; :: thesis: [((p11 ^ p2) . i),((p11 ^ p2) . (i + 1))] in R
then A17: ( 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 A18: ( i < l1 & i < m & i + 1 <= m ) by INT_1:7, A7, A4, XXREAL_0:2;
then ( i in Seg m & i + 1 in Seg m ) by A17;
then A19: ( i in dom p11 & i + 1 in dom p11 ) by A7, A4, 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 A19, FUNCT_1:47;
hence [((p11 ^ p2) . i),((p11 ^ p2) . (i + 1))] in R by A3, A16, A18; :: thesis: verum
end;
suppose A20: i = m ; :: thesis: [((p11 ^ p2) . i),((p11 ^ p2) . (i + 1))] in R
A21: m in dom p11 by A20, A16, A8, FINSEQ_3:25;
then A22: (p11 ^ p2) . m = p11 . m by FINSEQ_1:def 7
.= p1 . m by FUNCT_1:47, A21 ;
A23: (p11 ^ p2) . (m + 1) = p1 . (m + 1) by A3, A6, A4, A8, FINSEQ_1:def 7, A5;
thus [((p11 ^ p2) . i),((p11 ^ p2) . (i + 1))] in R by A20, A22, A23, A3, A16, A7, A4; :: thesis: verum
end;
suppose A24: i > m ; :: thesis: [((p11 ^ p2) . i),((p11 ^ p2) . (i + 1))] in R
then consider j being Nat such that
A25: i = m + j by NAT_1:10;
j <> 0 by A24, A25;
then A26: j >= 0 + 1 by INT_1:7;
then A27: ( j >= 1 & j + 1 >= 1 + 0 ) by XREAL_1:7;
m + j < m + l2 by A25, A16, A8, FINSEQ_1:22;
then A28: j < l2 by XREAL_1:7;
then A29: ( j <= l2 & j + 1 <= l2 ) by INT_1:7;
( j in Seg l2 & j + 1 in Seg l2 ) by A29, A27;
then A30: ( j in dom p2 & j + 1 in dom p2 ) by FINSEQ_1:def 3;
A31: (p11 ^ p2) . i = p2 . j by FINSEQ_1:def 7, A30, A25, A8;
A32: (p11 ^ p2) . (i + 1) = (p11 ^ p2) . ((len p11) + (j + 1)) by A25, A8
.= p2 . (j + 1) by FINSEQ_1:def 7, A30 ;
thus [((p11 ^ p2) . i),((p11 ^ p2) . (i + 1))] in R by A31, A32, A5, A28, A26; :: 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 A1, A9, A8, FINSEQ_1:22, A11, A14, A15;
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