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