let V be non empty set ; :: thesis: for A, B being Element of V
for m being Element of Maps V st m in Maps A,B holds
m `2 in Funcs A,B
let A, B be Element of V; :: thesis: for m being Element of Maps V st m in Maps A,B holds
m `2 in Funcs A,B
let m be Element of Maps V; :: thesis: ( m in Maps A,B implies m `2 in Funcs A,B )
assume A1: m in Maps A,B ; :: thesis: m `2 in Funcs A,B
then A2: m = [[A,B],(m `2 )] by Th16;
then A3: m `2 is Function of A,B by A1, Lm4;
( B = {} implies A = {} ) by A1, A2, Lm4;
hence m `2 in Funcs A,B by A3, FUNCT_2:11; :: thesis: verum