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 A2: ( <^o2,o3^> = {} or <^o1,o2^> = {} ) ; :: thesis: the Comp of C . o1,o2,o3 = (FuncComp (Funcs o1,o2),(Funcs o2,o3)) | [:<^o2,o3^>,<^o1,o2^>:]

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

end;

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

then A4: <^o1,o3^> <> {} by A1, Def4;
then A5: dom (the Comp of C . o1,o2,o3) = [:<^o2,o3^>,<^o1,o2^>:] by FUNCT_2:def 1;
A6: ( <^o2,o3^> c= Funcs o2,o3 & <^o1,o2^> c= Funcs o1,o2 ) by A1, Def13;
dom (FuncComp (Funcs o1,o2),(Funcs o2,o3)) = [:(Funcs o2,o3),(Funcs o1,o2):] by PARTFUN1:def 4;
then 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;
then A7: dom (the Comp of C . o1,o2,o3) = dom ((FuncComp (Funcs o1,o2),(Funcs o2,o3)) | [:<^o2,o3^>,<^o1,o2^>:]) by A6, A5, 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 A8: 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
A9: i1 in <^o2,o3^> and
A10: i2 in <^o1,o2^> and
A11: i = [i1,i2] by A5, ZFMISC_1:103;
reconsider a2 = i2 as Morphism of o1,o2 by A10;
reconsider a1 = i1 as Morphism of o2,o3 by A9;
reconsider g = i1, h = i2 as Function by A6, A9, A10;
thus (the Comp of C . o1,o2,o3) . i = (the Comp of C . o1,o2,o3) . a1,a2 by A11
.= a1 * a2 by A3, Def10
.= g * h by A1, A3, A4, Def14
.= (FuncComp (Funcs o1,o2),(Funcs o2,o3)) . g,h by A6, A9, A10, Th13
.= ((FuncComp (Funcs o1,o2),(Funcs o2,o3)) | [:<^o2,o3^>,<^o1,o2^>:]) . i by A7, A8, A11, 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 A7, FUNCT_1:9; :: thesis: verum

end;

end;