( the carrier of [:L1,L2:] = [: the carrier of L1, the carrier of L2:] & the carrier of [:T1,T2:] = [: the carrier of T1, the carrier of T2:] ) by YELLOW_3:def 2;
hence [:f,g:] is Function of [:L1,L2:],[:T1,T2:] ; :: thesis: verum