( the carrier of S = the carrier of (Top2NTop S) & the carrier of T = the carrier of (Top2NTop T) ) by FINTOPO7:def 15;
hence f is Function of (Top2NTop S),(Top2NTop T) ; :: thesis: verum