A1: rng (s ^\ k) c= rng s by Lm1;
rng s c= X by RELAT_1:def 19;
hence rng (s ^\ k) c= X by A1; :: according to RELAT_1:def 19 :: thesis: verum