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:8; :: thesis: verum