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 13 :: 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)
A2: F . a1 = a1 by FUNCT_1:35;
F . a2 = a2 by FUNCT_1:35;
hence <^a1,a2^> c= Funcs (F . a1),(F . a2) by A1, A2; :: thesis: verum