let C be non empty AltCatStr ; :: thesis: ( C is quasi-functional & C is semi-functional & C is transitive implies C is pseudo-functional )
assume A1: ( C is quasi-functional & C is semi-functional & C is transitive ) ; :: thesis: C is pseudo-functional
let o1, o2, o3 be object of C; :: according to ALTCAT_1:def 15 :: thesis: the Comp of C . o1,o2,o3 = (FuncComp (Funcs o1,o2),(Funcs o2,o3)) | [:<^o2,o3^>,<^o1,o2^>:]
set c = the Comp of C . o1,o2,o3;
set f = (FuncComp (Funcs o1,o2),(Funcs o2,o3)) | [:<^o2,o3^>,<^o1,o2^>:];

per cases ( <^o2,o3^> = {} or <^o1,o2^> = {} or ( <^o2,o3^> <> {} & <^o1,o2^> <> {} ) ) ;

suppose ( <^o2,o3^> = {} or <^o1,o2^> = {} ) ; :: thesis: the Comp of C . o1,o2,o3 = (FuncComp (Funcs o1,o2),(Funcs o2,o3)) | [:<^o2,o3^>,<^o1,o2^>:]

then A3: [:<^o2,o3^>,<^o1,o2^>:] = {} ;
hence the Comp of C . o1,o2,o3 = {}
.= (FuncComp (Funcs o1,o2),(Funcs o2,o3)) | [:<^o2,o3^>,<^o1,o2^>:] by A3 ;
:: thesis: verum

end;

suppose A4: ( <^o2,o3^> <> {} & <^o1,o2^> <> {} ) ; :: thesis: the Comp of C . o1,o2,o3 = (FuncComp (Funcs o1,o2),(Funcs o2,o3)) | [:<^o2,o3^>,<^o1,o2^>:]

then A5: <^o1,o3^> <> {} by A1, Def4;
dom (FuncComp (Funcs o1,o2),(Funcs o2,o3)) = [:(Funcs o2,o3),(Funcs o1,o2):] by PARTFUN1:def 4;
then A6: dom ((FuncComp (Funcs o1,o2),(Funcs o2,o3)) | [:<^o2,o3^>,<^o1,o2^>:]) = [:(Funcs o2,o3),(Funcs o1,o2):] /\ [:<^o2,o3^>,<^o1,o2^>:] by RELAT_1:90;
A7: ( <^o2,o3^> c= Funcs o2,o3 & <^o1,o2^> c= Funcs o1,o2 ) by A1, Def13;
A8: dom (the Comp of C . o1,o2,o3) = [:<^o2,o3^>,<^o1,o2^>:] by A5, FUNCT_2:def 1;
then A9: dom (the Comp of C . o1,o2,o3) = dom ((FuncComp (Funcs o1,o2),(Funcs o2,o3)) | [:<^o2,o3^>,<^o1,o2^>:]) by A6, A7, XBOOLE_1:28, ZFMISC_1:119;

now

let i be set ; :: thesis: ( i in dom (the Comp of C . o1,o2,o3) implies (the Comp of C . o1,o2,o3) . i = ((FuncComp (Funcs o1,o2),(Funcs o2,o3)) | [:<^o2,o3^>,<^o1,o2^>:]) . i )
assume A10: i in dom (the Comp of C . o1,o2,o3) ; :: thesis: (the Comp of C . o1,o2,o3) . i = ((FuncComp (Funcs o1,o2),(Funcs o2,o3)) | [:<^o2,o3^>,<^o1,o2^>:]) . i
then consider i1, i2 being set such that
A11: ( i1 in <^o2,o3^> & i2 in <^o1,o2^> ) and
A12: i = [i1,i2] by A8, ZFMISC_1:103;
reconsider g = i1, h = i2 as Function by A7, A11;
reconsider a1 = i1 as Morphism of o2,o3 by A11;
reconsider a2 = i2 as Morphism of o1,o2 by A11;
thus (the Comp of C . o1,o2,o3) . i = (the Comp of C . o1,o2,o3) . a1,a2 by A12
.= a1 * a2 by A4, Def10
.= g * h by A1, A4, A5, Def14
.= (FuncComp (Funcs o1,o2),(Funcs o2,o3)) . g,h by A7, A11, Th13
.= ((FuncComp (Funcs o1,o2),(Funcs o2,o3)) | [:<^o2,o3^>,<^o1,o2^>:]) . i by A9, A10, A12, FUNCT_1:70 ; :: thesis: verum

end;

hence the Comp of C . o1,o2,o3 = (FuncComp (Funcs o1,o2),(Funcs o2,o3)) | [:<^o2,o3^>,<^o1,o2^>:] by A9, FUNCT_1:9; :: thesis: verum

end;

end;