rng f = [#] T by A1, FUNCT_2:def 3;
hence f " is Function of T,S by A1, FUNCT_2:25; :: thesis: verum