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