set C = DiscrCat A;
thus DiscrCat A is pseudo-functional :: thesis:

let o1, o2, o3 be object of (DiscrCat A); :: according to ALTCAT_1:def 15 :: thesis:
A1: id o1 in Funcs o1,o1 by Th2;

per cases ;

suppose A2: ( o1 = o2 & o2 = o3 ) ; :: thesis:

then A3: ( <^o2,o3^> = {(id o1)} & <^o1,o2^> = {(id o1)} ) by Def22;
then A4: ( <^o1,o2^> c= Funcs o1,o2 & <^o2,o3^> c= Funcs o2,o3 ) by A1, A2, ZFMISC_1:37;
thus the Comp of (DiscrCat A) . o1,o2,o3 = (id o1),(id o1) :-> (id o1) by A2, Th29
.= FuncComp {(id o1)},{(id o1)} by Th15
.= (FuncComp (Funcs o1,o2),(Funcs o2,o3)) | [:<^o2,o3^>,<^o1,o2^>:] by A3, A4, Th16 ; :: thesis:

end;

suppose A5: ( o1 <> o2 or o2 <> o3 ) ; :: thesis:

then ( <^o2,o3^> = {} or <^o1,o2^> = {} ) by Def20;
then A6: [:<^o2,o3^>,<^o1,o2^>:] = {} ;
thus the Comp of (DiscrCat A) . o1,o2,o3 = {} by A5, Th28
.= (FuncComp (Funcs o1,o2),(Funcs o2,o3)) | [:<^o2,o3^>,<^o1,o2^>:] by A6 ; :: thesis:

end;

thus DiscrCat A is pseudo-discrete :: thesis:

let i be object of (DiscrCat A); :: according to ALTCAT_1:def 21 :: thesis:
<^i,i^> = {(id i)} by Def22;
hence <^i,i^> is trivial ; :: thesis:

end;

thus DiscrCat A is with_units :: thesis:

thus the Comp of (DiscrCat A) is with_left_units :: according to ALTCAT_1:def 18 :: thesis:

let j be Element of (DiscrCat A); :: according to ALTCAT_1:def 9 :: thesis:
reconsider j' = j as object of (DiscrCat A) ;
take id j' ; :: thesis:
the Arrows of (DiscrCat A) . j,j = <^j',j'^>
.= {(id j')} by Def22 ;
hence id j' in the Arrows of (DiscrCat A) . j,j by TARSKI:def 1; :: thesis:
let i be Element of (DiscrCat A); :: thesis:
let f be set ; :: thesis:
assume A7: f in the Arrows of (DiscrCat A) . i,j ; :: thesis:
reconsider i' = i as object of (DiscrCat A) ;
A8: the Arrows of (DiscrCat A) . i,j = <^i',j'^> ;
then A9: i' = j' by A7, Def20;
then f in {(id i')} by A7, A8, Def22;
then A10: f = id i' by TARSKI:def 1;
thus (the Comp of (DiscrCat A) . i,j,j) . (id j'),f = ((id i'),(id i') :-> (id i')) . (id j'),f by A9, Th29
.= f by A9, A10, Th12 ; :: thesis:

end;

let j be Element of (DiscrCat A); :: according to ALTCAT_1:def 8 :: thesis:
reconsider j' = j as object of (DiscrCat A) ;
take id j' ; :: thesis:
the Arrows of (DiscrCat A) . j,j = <^j',j'^>
.= {(id j')} by Def22 ;
hence id j' in the Arrows of (DiscrCat A) . j,j by TARSKI:def 1; :: thesis:
let i be Element of (DiscrCat A); :: thesis:
let f be set ; :: thesis:
assume A11: f in the Arrows of (DiscrCat A) . j,i ; :: thesis:
reconsider i' = i as object of (DiscrCat A) ;
A12: the Arrows of (DiscrCat A) . j,i = <^j',i'^> ;
then A13: i' = j' by A11, Def20;
then f in {(id i')} by A11, A12, Def22;
then A14: f = id i' by TARSKI:def 1;
thus (the Comp of (DiscrCat A) . j,j,i) . f,(id j') = ((id i'),(id i') :-> (id i')) . f,(id j') by A13, Th29
.= f by A13, A14, Th12 ; :: thesis:

end;

thus DiscrCat A is associative :: thesis:

set G = the Arrows of (DiscrCat A);
set c = the Comp of (DiscrCat A);
let i, j, k, l be Element of (DiscrCat A); :: according to ALTCAT_1:def 7,ALTCAT_1:def 17 :: thesis:
reconsider i' = i, j' = j, k' = k, l' = l as object of (DiscrCat A) ;
let f, g, h be set ; :: thesis:
assume A15: ( f in the Arrows of (DiscrCat A) . i,j & g in the Arrows of (DiscrCat A) . j,k & h in the Arrows of (DiscrCat A) . k,l ) ; :: thesis:
then ( f in <^i',j'^> & g in <^j',k'^> & h in <^k',l'^> ) ;
then A16: ( i' = j' & j' = k' & k' = l' ) by Def20;
<^i',i'^> = {(id i')} by Def22;
then A17: ( f = id i' & g = id i' & h = id i' ) by A15, A16, TARSKI:def 1;
the Comp of (DiscrCat A) . i',i',i' = (id i'),(id i') :-> (id i') by Th29;
hence (the Comp of (DiscrCat A) . i,k,l) . h,((the Comp of (DiscrCat A) . i,j,k) . g,f) = (the Comp of (DiscrCat A) . i,j,l) . ((the Comp of (DiscrCat A) . j,k,l) . h,g),f by A16, A17, Th12; :: thesis:

end;