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

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