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

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

end;

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