hereby :: thesis: ( ( for n being Nat holds S . n is Path-like ) implies S is Path-like )

assume A1: S is Path-like ; :: thesis: for x being Nat holds S . x is Path-like
let x be Nat; :: thesis: S . x is Path-like
x in dom S by Lm2;
hence S . x is Path-like by A1; :: thesis: verum

end;

assume A2: for x being Nat holds S . x is Path-like ; :: thesis: S is Path-like
let x be Element of dom S; :: according to GLPACY00:def 3 :: thesis: S . x is Path-like
thus S . x is Path-like by A2; :: thesis: verum