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 ;
then A2: cod (@ f) = @ b by Def10;
dom f = a by ;
then dom (@ f) = @ a by Def9;
hence x in Maps ((@ a),(@ b)) by ; :: 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 ;
then A4: cod (@ m) = b by Def10;
dom m = @ a by ;
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