let B be non empty subcategory of A; :: thesis: B is para-functional
consider F being ManySortedSet of 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: ( dom F = the carrier of A & the carrier of B c= the carrier of A ) by ALTCAT_2:def 11, PARTFUN1:def 4;
then dom (F | the carrier of B) = the carrier of B by RELAT_1:91;
then reconsider G = F | the carrier of B as ManySortedSet of by PARTFUN1:def 4, 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)
( a1 in the carrier of B & a2 in the carrier of B ) ;
then reconsider b1 = a1, b2 = a2 as object of A by A2;
( F . a1 = G . a1 & F . a2 = G . a2 ) by FUNCT_1:72;
then ( <^a1,a2^> c= <^b1,b2^> & <^b1,b2^> c= Funcs (G . a1),(G . a2) ) by A1, ALTCAT_2:32;
hence <^a1,a2^> c= Funcs (G . a1),(G . a2) by XBOOLE_1:1; :: thesis: verum