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_{1}, b_{2} being Element of the carrier of B holds <^b_{1},b_{2}^> c= Funcs ((G . b_{1}),(G . b_{2}))

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

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

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