let B be non empty subcategory of A; :: thesis: B is para-functional
consider F being ManySortedSet of A such that
A1: for a1, a2 being Object of A holds <^a1,a2^> c= Funcs ((F . a1),(F . a2)) by YELLOW18:def 7;
set G = F | the carrier of B;
A2: the carrier of B c= the carrier of A by ALTCAT_2:def 11;
dom F = the carrier of A by PARTFUN1:def 2;
then dom (F | the carrier of B) = the carrier of B by A2, RELAT_1:62;
then reconsider G = F | the carrier of B as ManySortedSet of B by PARTFUN1:def 2, RELAT_1:def 18;
take G ; :: according to YELLOW18:def 7 :: thesis: for b₁, b₂ being Element of the carrier of B holds <^b₁,b₂^> c= Funcs ((G . b₁),(G . b₂))
let a1, a2 be Object of B; :: thesis: <^a1,a2^> c= Funcs ((G . a1),(G . a2))
reconsider b1 = a1, b2 = a2 as Object of A by A2;
( F . a1 = G . a1 & F . a2 = G . a2 ) by FUNCT_1:49;
then ( <^a1,a2^> c= <^b1,b2^> & <^b1,b2^> c= Funcs ((G . a1),(G . a2)) ) by A1, ALTCAT_2:31;
hence <^a1,a2^> c= Funcs ((G . a1),(G . a2)) ; :: thesis: verum