rng (canFS X) = X by FUNCT_2:def 3;
hence rng (canFS X) c= A ; :: according to RELAT_1:def 19 :: thesis: verum