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 13 :: 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 FUNCT_2:126;

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 Def20;
then A4: <^o1,o2^> c= Funcs (o1,o2) by A1, A2, ZFMISC_1:31;
thus the Comp of (DiscrCat A) . (o1,o2,o3) = ((id o1),(id o1)) :-> (id o1) by A2, Th19
.= FuncComp ({(id o1)},{(id o1)}) by Th7
.= (FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) | [:<^o2,o3^>,<^o1,o2^>:] by A2, A3, A4, Th8 ; :: 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 Def18;
thus the Comp of (DiscrCat A) . (o1,o2,o3) = {} by A5, Th18
.= (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 19 :: thesis: <^i,i^> is trivial
<^i,i^> = {(id i)} by Def20;
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 16 :: thesis: the Comp of (DiscrCat A) is with_right_units

proof

let j be Element of (DiscrCat A); :: according to ALTCAT_1:def 7 :: 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 Def20 ;
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, Def18;
then f in {(id i9)} by A7, A8, Def20;
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, Th19
.= f by A9, A10, FUNCT_4:80 ; :: thesis: verum

end;

let j be Element of (DiscrCat A); :: according to ALTCAT_1:def 6 :: 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 Def20 ;
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, Def18;
then f in {(id i9)} by A11, A12, Def20;
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, Th19
.= f by A13, A14, FUNCT_4:80 ; :: 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 5,ALTCAT_1:def 15 :: 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 Def18;
A19: <^i9,i9^> = {(id i9)} by Def20;
then A20: f = id i9 by A15, A18, TARSKI:def 1;
g in <^j9,k9^> by A16;
then A21: j9 = k9 by Def18;
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 Th19;
h in <^k9,l9^> by A17;
then A24: k9 = l9 by Def18;
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, FUNCT_4:80; :: thesis: verum

end;