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))

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) ) )

hence
Hom (a,b) = Maps ((@ a),(@ b))
by TARSKI:2; :: thesis: verum( ( 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) )

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;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 A3:
x in Maps ((@ a),(@ b))
; :: thesis: x in Hom (a,b)
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;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

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