let S be non empty set ; :: thesis: for R being total Relation of S,S
for pai1, pai2 being inf_path of R
for k being Element of NAT st pai1 . k = pai2 . 0 holds
PathConc (pai1,pai2,k) is inf_path of R
let R be total Relation of S,S; :: thesis: for pai1, pai2 being inf_path of R
for k being Element of NAT st pai1 . k = pai2 . 0 holds
PathConc (pai1,pai2,k) is inf_path of R
let pai1, pai2 be inf_path of R; :: thesis: for k being Element of NAT st pai1 . k = pai2 . 0 holds
PathConc (pai1,pai2,k) is inf_path of R
let k be Element of NAT ; :: thesis: ( pai1 . k = pai2 . 0 implies PathConc (pai1,pai2,k) is inf_path of R )
set pai = PathConc (pai1,pai2,k);
assume A1: pai1 . k = pai2 . 0 ; :: thesis: PathConc (pai1,pai2,k) is inf_path of R
for n being Element of NAT holds [((PathConc (pai1,pai2,k)) . n),((PathConc (pai1,pai2,k)) . (n + 1))] in R

proof

let n be Element of NAT ; :: thesis: [((PathConc (pai1,pai2,k)) . n),((PathConc (pai1,pai2,k)) . (n + 1))] in R
set n1 = n + 1;

per cases ( n + 1 < k or n + 1 = k or k < n + 1 ) by XXREAL_0:1;

suppose A2: n + 1 < k ; :: thesis: [((PathConc (pai1,pai2,k)) . n),((PathConc (pai1,pai2,k)) . (n + 1))] in R

then A3: n < k by NAT_1:13;
A4: (PathConc (pai1,pai2,k)) . n = PathChange (pai1,pai2,k,n) by Def71
.= pai1 . n by A3, Def70 ;
(PathConc (pai1,pai2,k)) . (n + 1) = PathChange (pai1,pai2,k,(n + 1)) by Def71
.= pai1 . (n + 1) by A2, Def70 ;
hence [((PathConc (pai1,pai2,k)) . n),((PathConc (pai1,pai2,k)) . (n + 1))] in R by A4, Def41; :: thesis: verum

end;

suppose A5: n + 1 = k ; :: thesis: [((PathConc (pai1,pai2,k)) . n),((PathConc (pai1,pai2,k)) . (n + 1))] in R

then A6: n < k by NAT_1:13;
A7: (PathConc (pai1,pai2,k)) . n = PathChange (pai1,pai2,k,n) by Def71
.= pai1 . n by A6, Def70 ;
(PathConc (pai1,pai2,k)) . (n + 1) = PathChange (pai1,pai2,k,(n + 1)) by Def71
.= pai2 . ((n + 1) - k) by A5, Def70
.= pai1 . (n + 1) by A1, A5 ;
hence [((PathConc (pai1,pai2,k)) . n),((PathConc (pai1,pai2,k)) . (n + 1))] in R by A7, Def41; :: thesis: verum

end;

suppose A8: k < n + 1 ; :: thesis: [((PathConc (pai1,pai2,k)) . n),((PathConc (pai1,pai2,k)) . (n + 1))] in R

then A9: k <= n by NAT_1:13;
then reconsider m = n - k as Element of NAT by NAT_1:21;
A10: (PathConc (pai1,pai2,k)) . (n + 1) = PathChange (pai1,pai2,k,(n + 1)) by Def71
.= pai2 . ((n + 1) - k) by A8, Def70
.= pai2 . (m + 1) ;
(PathConc (pai1,pai2,k)) . n = PathChange (pai1,pai2,k,n) by Def71
.= pai2 . m by A9, Def70 ;
hence [((PathConc (pai1,pai2,k)) . n),((PathConc (pai1,pai2,k)) . (n + 1))] in R by A10, Def41; :: thesis: verum

end;

end;

end;

hence PathConc (pai1,pai2,k) is inf_path of R by Def41; :: thesis: verum