let f be Function; :: thesis: for n being Nat
for m being non zero Nat holds (f | (n + m)) . n = f . n
let n be Nat; :: thesis: for m being non zero Nat holds (f | (n + m)) . n = f . n
let m be non zero Nat; :: thesis: (f | (n + m)) . n = f . n
set g = f | (n + m);
n + 0 < n + m by XREAL_1:6;
then n in Segm (n + m) by NAT_1:44;
hence (f | (n + m)) . n = f . n by FUNCT_1:49; :: thesis: verum