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) ;
( dom f = a & cod f = b ) by A1, CAT_1:18;
then ( dom (@ f) = @ a & cod (@ f) = @ b ) by Def10, Def11;
hence x in Maps (@ a),(@ b) by Th19; :: thesis: verum

end;

assume A2: 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 A2;
( dom m = @ a & cod m = @ b ) by A2, Th19;
then ( dom (@ m) = a & cod (@ m) = b ) by Def10, Def11;
hence x in Hom a,b ; :: thesis: verum

end;

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