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 :: thesis: for x being object holds
( ( x in Hom (a,b) implies x in Maps ((@ a),(@ b)) ) & ( x in Maps ((@ a),(@ b)) implies x in Hom (a,b) ) )

let x be object ; :: 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:1;
then A2: cod (@ f) = @ b by Def10;
dom f = a by A1, CAT_1:1;
then dom (@ f) = @ a by Def9;
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 Def10;
dom m = @ a by A3, Th19;
then dom (@ m) = a by Def9;
hence x in Hom (a,b) by A4; :: thesis: verum

end;

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