deffunc H1( Object of A) -> Element of bool the carrier' of B = Hom ((F1 . $1),(F2 . $1));
A2: for a being Object of A holds the carrier' of B meets H1(a)
proof
let a be Object of A; :: thesis: the carrier' of B meets H1(a)
set x = the Element of Hom ((F1 . a),(F2 . a));
A3: Hom ((F1 . a),(F2 . a)) <> {} by A1;
now :: thesis: ex x being Element of Hom ((F1 . a),(F2 . a)) st
( x in the carrier' of B & x in Hom ((F1 . a),(F2 . a)) )
take x = the Element of Hom ((F1 . a),(F2 . a)); :: thesis: ( x in the carrier' of B & x in Hom ((F1 . a),(F2 . a)) )
thus ( x in the carrier' of B & x in Hom ((F1 . a),(F2 . a)) ) by A3, TARSKI:def 3; :: thesis: verum
end;
hence the carrier' of B meets H1(a) by XBOOLE_0:3; :: thesis: verum
end;
consider t being Function of the carrier of A, the carrier' of B such that
A4: for a being Object of A holds t . a in H1(a) from FUNCT_2:sch 10(A2);
 take t ; :: thesis: for a being Object of A holds t . a is Morphism of F1 . a,F2 . a
let a be Object of A; :: thesis: t . a is Morphism of F1 . a,F2 . a
t . a in Hom ((F1 . a),(F2 . a)) by A4;
hence t . a is Morphism of F1 . a,F2 . a by CAT_1:def 5; :: thesis: verum