set C = DiscrCat A;
thus DiscrCat A is pseudo-functional :: thesis: ( DiscrCat A is pseudo-discrete & DiscrCat A is with_units & DiscrCat A is associative )

proof

let o1, o2, o3 be object of (DiscrCat A); :: according to ALTCAT_1:def 15 :: thesis: the Comp of (DiscrCat A) . o1,o2,o3 = (FuncComp (Funcs o1,o2),(Funcs o2,o3)) | [:<^o2,o3^>,<^o1,o2^>:]
A1: id o1 in Funcs o1,o1 by Th2;

per cases ( ( o1 = o2 & o2 = o3 ) or o1 <> o2 or o2 <> o3 ) ;

suppose A2: ( o1 = o2 & o2 = o3 ) ; :: thesis: the Comp of (DiscrCat A) . o1,o2,o3 = (FuncComp (Funcs o1,o2),(Funcs o2,o3)) | [:<^o2,o3^>,<^o1,o2^>:]

then A3: <^o2,o3^> = {(id o1)} by Def22;
then A4: <^o1,o2^> c= Funcs o1,o2 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 A2, A3, A4, Th16 ; :: thesis: verum

end;

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

then A6: ( <^o2,o3^> = {} or <^o1,o2^> = {} ) by Def20;
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: verum

end;

end;

end;

thus DiscrCat A is pseudo-discrete :: thesis: ( DiscrCat A is with_units & DiscrCat A is associative )

proof

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

end;

thus DiscrCat A is with_units :: thesis: DiscrCat A is associative

proof

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

proof

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

end;

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

end;

thus DiscrCat A is associative :: thesis: verum

proof

let i, j, k, l be Element of (DiscrCat A); :: according to ALTCAT_1:def 7,ALTCAT_1:def 17 :: thesis: for f, g, h being set st 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 holds
(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
set G = the Arrows of (DiscrCat A);
set c = the Comp of (DiscrCat A);
reconsider i9 = i, j9 = j, k9 = k, l9 = l as object of (DiscrCat A) ;
let f, g, h be set ; :: thesis: ( 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 implies (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 )
assume that
A15: f in the Arrows of (DiscrCat A) . i,j and
A16: g in the Arrows of (DiscrCat A) . j,k and
A17: h in the Arrows of (DiscrCat A) . k,l ; :: thesis: (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
f in <^i9,j9^> by A15;
then A18: i9 = j9 by Def20;
A19: <^i9,i9^> = {(id i9)} by Def22;
then A20: f = id i9 by A15, A18, TARSKI:def 1;
g in <^j9,k9^> by A16;
then A21: j9 = k9 by Def20;
then A22: g = id i9 by A16, A18, A19, TARSKI:def 1;
A23: the Comp of (DiscrCat A) . i9,i9,i9 = (id i9),(id i9) :-> (id i9) by Th29;
h in <^k9,l9^> by A17;
then A24: k9 = l9 by Def20;
then h = id i9 by A17, A18, A21, A19, TARSKI:def 1;
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 A18, A21, A24, A20, A22, A23, Th12; :: thesis: verum

end;