let V be non empty set ; :: thesis: for a, b being Object of (Ens V) st Hom (a,b) <> {} holds
Funcs ((@ a),(@ b)) <> {}
let a, b be Object of (Ens V); :: thesis: ( Hom (a,b) <> {} implies Funcs ((@ a),(@ b)) <> {} )
set m = the Element of Maps ((@ a),(@ b));
assume Hom (a,b) <> {} ; :: thesis: Funcs ((@ a),(@ b)) <> {}
then A1: Maps ((@ a),(@ b)) <> {} by Th26;
reconsider m = the Element of Maps ((@ a),(@ b)) as Element of Maps V by A1, Th17, TARSKI:def 3;
m `2 in Funcs ((@ a),(@ b)) by A1, Th20;
hence Funcs ((@ a),(@ b)) <> {} ; :: thesis: verum