set G = c (#) F;
thus c (#) F is finite ; :: thesis: ( c (#) F is INT -valued & c (#) F is T-Sequence-like )
thus rng (c (#) F) c= INT by VALUED_0:def 5; :: according to RELAT_1:def 19 :: thesis: c (#) F is T-Sequence-like
thus c (#) F is T-Sequence-like ; :: thesis: verum