let C be category; :: thesis: ( C is quasi-functional implies C is para-functional )
assume A1: for a1, a2 being Object of C holds <^a1,a2^> c= Funcs (a1,a2) ; :: according to ALTCAT_1:def 11 :: thesis: C is para-functional
reconsider F = id the carrier of C as ManySortedSet of C ;
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 a1, a2 be Object of C; :: thesis: <^a1,a2^> c= Funcs ((F . a1),(F . a2))
thus <^a1,a2^> c= Funcs ((F . a1),(F . a2)) by A1; :: thesis: verum