let C be category; :: thesis: ( C is para-functional iff for a1, a2 being Object of C holds <^a1,a2^> c= Funcs ((the_carrier_of a1),(the_carrier_of a2)) )
thus ( C is para-functional implies for a1, a2 being Object of C holds <^a1,a2^> c= Funcs ((the_carrier_of a1),(the_carrier_of a2)) ) :: thesis: ( ( for a1, a2 being Object of C holds <^a1,a2^> c= Funcs ((the_carrier_of a1),(the_carrier_of a2)) ) implies C is para-functional )

proof

given F being ManySortedSet of C such that A1: for a1, a2 being Object of C holds <^a1,a2^> c= Funcs ((F . a1),(F . a2)) ; :: according to YELLOW18:def 7 :: thesis: for a1, a2 being Object of C holds <^a1,a2^> c= Funcs ((the_carrier_of a1),(the_carrier_of a2))
let a1, a2 be Object of C; :: thesis: <^a1,a2^> c= Funcs ((the_carrier_of a1),(the_carrier_of a2))
A2: idm a1 in <^a1,a1^> ;
A3: <^a1,a1^> c= Funcs ((F . a1),(F . a1)) by A1;
A4: <^a2,a2^> c= Funcs ((F . a2),(F . a2)) by A1;
A5: idm a2 in <^a2,a2^> ;
A6: ex f1 being Function st
( idm a1 = f1 & dom f1 = F . a1 & rng f1 c= F . a1 ) by A2, A3, FUNCT_2:def 2;
ex f2 being Function st
( idm a2 = f2 & dom f2 = F . a2 & rng f2 c= F . a2 ) by A4, A5, FUNCT_2:def 2;
hence <^a1,a2^> c= Funcs ((the_carrier_of a1),(the_carrier_of a2)) by A1, A6; :: thesis: verum

end;

assume A7: for a1, a2 being Object of C holds <^a1,a2^> c= Funcs ((the_carrier_of a1),(the_carrier_of a2)) ; :: thesis: C is para-functional
deffunc H₁( set ) -> set = C -carrier_of $1;
consider F being ManySortedSet of the carrier of C such that
A8: for a being Element of C holds F . a = H₁(a) from PBOOLE:sch 5();
take F ; :: according to YELLOW18:def 7 :: thesis: for a1, a2 being Object of C holds <^a1,a2^> c= Funcs ((F . a1),(F . a2))
let a, b be Object of C; :: thesis: <^a,b^> c= Funcs ((F . a),(F . b))
A9: F . a = the_carrier_of a by A8;
F . b = the_carrier_of b by A8;
hence <^a,b^> c= Funcs ((F . a),(F . b)) by A7, A9; :: thesis: verum