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 )
assume A1: pai1 . k = pai2 . 0 ; :: thesis: PathConc pai1,pai2,k is inf_path of R
set pai = PathConc pai1,pai2,k;
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

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

end;

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

A6: (PathConc pai1,pai2,k) . (n + 1) = PathChange pai1,pai2,k,(n + 1) by Def69
.= pai2 . ((n + 1) - k) by A5, Def68
.= pai1 . (n + 1) by A1, A5 ;
A7: n < k by A5, NAT_1:13;
(PathConc pai1,pai2,k) . n = PathChange pai1,pai2,k,n by Def69
.= pai1 . n by A7, Def68 ;
hence [((PathConc pai1,pai2,k) . n),((PathConc pai1,pai2,k) . (n + 1))] in R by A6, Def39; :: 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 = PathChange pai1,pai2,k,n by Def69
.= pai2 . m by A9, Def68 ;
(PathConc pai1,pai2,k) . (n + 1) = PathChange pai1,pai2,k,(n + 1) by Def69
.= pai2 . ((n + 1) - k) by A8, Def68
.= pai2 . (m + 1) ;
hence [((PathConc pai1,pai2,k) . n),((PathConc pai1,pai2,k) . (n + 1))] in R by A10, Def39; :: thesis: verum

end;

end;

end;

hence PathConc pai1,pai2,k is inf_path of R by Def39; :: thesis: verum