let S be non empty set ; :: thesis: for R being total Relation of S,S
for s0, s1 being Element of S st [s0,s1] in R holds
ex pai being inf_path of R st
( pai . 0 = s0 & pai . 1 = s1 )
let R be total Relation of S,S; :: thesis: for s0, s1 being Element of S st [s0,s1] in R holds
ex pai being inf_path of R st
( pai . 0 = s0 & pai . 1 = s1 )
let s0, s1 be Element of S; :: thesis: ( [s0,s1] in R implies ex pai being inf_path of R st
( pai . 0 = s0 & pai . 1 = s1 ) )
assume A1: [s0,s1] in R ; :: thesis: ex pai being inf_path of R st
( pai . 0 = s0 & pai . 1 = s1 )
consider pai1 being inf_path of R such that
A2: pai1 . 0 = s1 by Th25;
deffunc H₁( set ) -> Element of S = PrePath $1,s0,pai1;
A3: for x being set st x in NAT holds
H₁(x) in S ;
consider pai being Function of NAT ,S such that
A4: for n being set st n in NAT holds
pai . n = H₁(n) from FUNCT_2:sch 2(A3);
for n being Element of NAT holds [(pai . n),(pai . (n + 1))] in R

proof

let n be Element of NAT ; :: thesis: [(pai . n),(pai . (n + 1))] in R
set n1 = n + 1;
set n0 = n - 1;

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

suppose A5: n = 0 ; :: thesis: [(pai . n),(pai . (n + 1))] in R

A6: pai . n = H₁(n) by A4
.= s0 by A5, Def61 ;
A7: k_nat ((k_nat (n + 1)) - 1) = k_nat (1 - 1) by A5, Def2
.= 0 by Def2 ;
pai . (n + 1) = H₁(n + 1) by A4
.= s1 by A2, A7, Def61 ;
hence [(pai . n),(pai . (n + 1))] in R by A1, A6; :: thesis: verum

end;

suppose A8: n <> 0 ; :: thesis: [(pai . n),(pai . (n + 1))] in R

then n > 0 ;
then reconsider n0 = n - 1 as Element of NAT by NAT_1:20;
A9: pai . n = H₁(n) by A4
.= pai1 . (k_nat ((k_nat n) - 1)) by A8, Def61
.= pai1 . (k_nat (n - 1)) by Def2
.= pai1 . n0 by Def2 ;
pai . (n + 1) = H₁(n + 1) by A4
.= pai1 . (k_nat ((k_nat (n + 1)) - 1)) by Def61
.= pai1 . (k_nat ((n + 1) - 1)) by Def2
.= pai1 . (n0 + 1) by Def2 ;
hence [(pai . n),(pai . (n + 1))] in R by A9, Def39; :: thesis: verum

end;

end;

end;

then reconsider pai = pai as inf_path of R by Def39;
take pai ; :: thesis: ( pai . 0 = s0 & pai . 1 = s1 )
A10: pai . 0 = H₁( 0 ) by A4
.= s0 by Def61 ;
pai . 1 = H₁(1) by A4
.= pai1 . (k_nat ((k_nat 1) - 1)) by Def61
.= pai1 . (k_nat (1 - 1)) by Def2
.= s1 by A2, Def2 ;
hence ( pai . 0 = s0 & pai . 1 = s1 ) by A10; :: thesis: verum