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 13 :: 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;
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;
dom (FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) = [:(Funcs (o2,o3)),(Funcs (o1,o2)):] by PARTFUN1:def 2;
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:61;
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:96;

now :: thesis: for i being object st i in dom ( the Comp of C . (o1,o2,o3)) holds
( the Comp of C . (o1,o2,o3)) . i = ((FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) | [:<^o2,o3^>,<^o1,o2^>:]) . i

let i be object ; :: 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 object such that
A9: i1 in <^o2,o3^> and
A10: i2 in <^o1,o2^> and
A11: i = [i1,i2] by ZFMISC_1:84;
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, Def8
.= g * h by A1, A3, A4
.= (FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) . (g,h) by A6, A9, A10, Th5
.= ((FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) | [:<^o2,o3^>,<^o1,o2^>:]) . i by A7, A8, A11, FUNCT_1:47 ; :: 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:2; :: thesis: verum

end;

end;