consider f being Element of Funcs V, A, B being Element of V such that
A1: m = [[A,B],f] and
( ( B = {} implies A = {} ) & f is Function of A,B ) by Th4;
[A,B] = m `1 by A1, MCART_1:7;
hence (m `1 ) `1 is Element of V by MCART_1:7; :: thesis: verum