for pai1, pai2 being inf_path of R st ( for n being Element of NAT holds pai1 . n = pai . (n + k) ) & ( for n being Element of NAT holds pai2 . n = pai . (n + k) ) holds
pai1 = pai2

proof

let pai1, pai2 be inf_path of R; :: thesis: ( ( for n being Element of NAT holds pai1 . n = pai . (n + k) ) & ( for n being Element of NAT holds pai2 . n = pai . (n + k) ) implies pai1 = pai2 )
assume that
A6: for n being Element of NAT holds pai1 . n = pai . (n + k) and
A7: for n being Element of NAT holds pai2 . n = pai . (n + k) ; :: thesis: pai1 = pai2
for x being object st x in NAT holds
pai1 . x = pai2 . x

proof

let x be object ; :: thesis: ( x in NAT implies pai1 . x = pai2 . x )
assume x in NAT ; :: thesis: pai1 . x = pai2 . x
then reconsider x = x as Element of NAT ;
pai1 . x = pai . (x + k) by A6
.= pai2 . x by A7 ;
hence pai1 . x = pai2 . x ; :: thesis: verum

end;

hence pai1 = pai2 by FUNCT_2:12; :: thesis: verum

end;

hence for b₁, b₂ being inf_path of R st ( for n being Element of NAT holds b₁ . n = pai . (n + k) ) & ( for n being Element of NAT holds b₂ . n = pai . (n + k) ) holds
b₁ = b₂ ; :: thesis: verum