let V be non empty set ; :: thesis: for a, b being Object of (Ens V) holds Hom a,b = Maps (@ a),(@ b)
let a, b be Object of (Ens V); :: thesis: Hom a,b = Maps (@ a),(@ b)

now

let x be set ; :: thesis: ( ( x in Hom a,b implies x in Maps (@ a),(@ b) ) & ( x in Maps (@ a),(@ b) implies x in Hom a,b ) )
thus ( x in Hom a,b implies x in Maps (@ a),(@ b) ) :: thesis: ( x in Maps (@ a),(@ b) implies x in Hom a,b )

proof

assume A1: x in Hom a,b ; :: thesis: x in Maps (@ a),(@ b)
then reconsider f = x as Morphism of (Ens V) ;
cod f = b by A1, CAT_1:18;
then A2: cod (@ f) = @ b by Def11;
dom f = a by A1, CAT_1:18;
then dom (@ f) = @ a by Def10;
hence x in Maps (@ a),(@ b) by A2, Th19; :: thesis: verum

end;

assume A3: x in Maps (@ a),(@ b) ; :: thesis: x in Hom a,b
Maps (@ a),(@ b) c= Maps V by Th17;
then reconsider m = x as Element of Maps V by A3;
cod m = @ b by A3, Th19;
then A4: cod (@ m) = b by Def11;
dom m = @ a by A3, Th19;
then dom (@ m) = a by Def10;
hence x in Hom a,b by A4; :: thesis: verum

end;

hence Hom a,b = Maps (@ a),(@ b) by TARSKI:2; :: thesis: verum