( the carrier of TX = the carrier of (NTop2Top TX) & the carrier of TY = the carrier of (NTop2Top TY) ) by FINTOPO7:def 16;
hence f is Function of (NTop2Top TX),(NTop2Top TY) ; :: thesis: verum