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) <> {} )
consider m being Element of Maps (@ a),(@ b);
assume Hom a,b <> {} ; :: thesis: Funcs (@ a),(@ b) <> {}
then A1: Maps (@ a),(@ b) <> {} by Th27;
Maps (@ a),(@ b) c= Maps V by Th17;
then reconsider m = m as Element of Maps V by A1, TARSKI:def 3;
m `2 in Funcs (@ a),(@ b) by A1, Th20;
hence Funcs (@ a),(@ b) <> {} ; :: thesis: verum