let A be non empty set ; :: thesis: ( EnsCat A is transitive & EnsCat A is associative & EnsCat A is with_units )

set G = the Arrows of (EnsCat A);

set C = the Comp of (EnsCat A);

thus A1: EnsCat A is transitive :: thesis: ( EnsCat A is associative & EnsCat A is with_units )

( e in the Arrows of (EnsCat A) . (i,i) & ( for j being Element of the carrier of (EnsCat A)

for f being set st f in the Arrows of (EnsCat A) . (i,j) holds

( the Comp of (EnsCat A) . (i,i,j)) . (f,e) = f ) )

reconsider i9 = i as Object of (EnsCat A) ;

take id i ; :: thesis: ( id i in the Arrows of (EnsCat A) . (i,i) & ( for j being Element of the carrier of (EnsCat A)

for f being set st f in the Arrows of (EnsCat A) . (i,j) holds

( the Comp of (EnsCat A) . (i,i,j)) . (f,(id i)) = f ) )

A16: <^i9,i9^> = Funcs (i,i) by Def14;

hence id i in the Arrows of (EnsCat A) . (i,i) by FUNCT_2:126; :: thesis: for j being Element of the carrier of (EnsCat A)

for f being set st f in the Arrows of (EnsCat A) . (i,j) holds

( the Comp of (EnsCat A) . (i,i,j)) . (f,(id i)) = f

reconsider I = id i as Morphism of i9,i9 by A16, FUNCT_2:126;

let j be Element of (EnsCat A); :: thesis: for f being set st f in the Arrows of (EnsCat A) . (i,j) holds

( the Comp of (EnsCat A) . (i,i,j)) . (f,(id i)) = f

let f be set ; :: thesis: ( f in the Arrows of (EnsCat A) . (i,j) implies ( the Comp of (EnsCat A) . (i,i,j)) . (f,(id i)) = f )

reconsider j9 = j as Object of (EnsCat A) ;

assume A17: f in the Arrows of (EnsCat A) . (i,j) ; :: thesis: ( the Comp of (EnsCat A) . (i,i,j)) . (f,(id i)) = f

then reconsider f99 = f as Morphism of i9,j9 ;

<^i9,j9^> = Funcs (i,j) by Def14;

then reconsider f9 = f as Function of i,j by A17, FUNCT_2:66;

thus ( the Comp of (EnsCat A) . (i,i,j)) . (f,(id i)) = f99 * I by A16, A17, Def8

.= f9 * (id i) by A16, A17, Th10

.= f by FUNCT_2:17 ; :: thesis: verum

set G = the Arrows of (EnsCat A);

set C = the Comp of (EnsCat A);

thus A1: EnsCat A is transitive :: thesis: ( EnsCat A is associative & EnsCat A is with_units )

proof

thus
EnsCat A is associative
:: thesis: EnsCat A is with_units
let o1, o2, o3 be Object of (EnsCat A); :: according to ALTCAT_1:def 2 :: thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies <^o1,o3^> <> {} )

assume ( <^o1,o2^> <> {} & <^o2,o3^> <> {} ) ; :: thesis: <^o1,o3^> <> {}

then ( Funcs (o1,o2) <> {} & Funcs (o2,o3) <> {} ) by Def14;

then Funcs (o1,o3) <> {} by FUNCT_2:129;

hence <^o1,o3^> <> {} by Def14; :: thesis: verum

end;assume ( <^o1,o2^> <> {} & <^o2,o3^> <> {} ) ; :: thesis: <^o1,o3^> <> {}

then ( Funcs (o1,o2) <> {} & Funcs (o2,o3) <> {} ) by Def14;

then Funcs (o1,o3) <> {} by FUNCT_2:129;

hence <^o1,o3^> <> {} by Def14; :: thesis: verum

proof

thus
the Comp of (EnsCat A) is with_left_units
:: according to ALTCAT_1:def 16 :: thesis: the Comp of (EnsCat A) is with_right_units
let i, j, k, l be Element of (EnsCat A); :: according to ALTCAT_1:def 5,ALTCAT_1:def 15 :: thesis: for f, g, h being set st f in the Arrows of (EnsCat A) . (i,j) & g in the Arrows of (EnsCat A) . (j,k) & h in the Arrows of (EnsCat A) . (k,l) holds

( the Comp of (EnsCat A) . (i,k,l)) . (h,(( the Comp of (EnsCat A) . (i,j,k)) . (g,f))) = ( the Comp of (EnsCat A) . (i,j,l)) . ((( the Comp of (EnsCat A) . (j,k,l)) . (h,g)),f)

reconsider i9 = i, j9 = j, k9 = k, l9 = l as Object of (EnsCat A) ;

let f, g, h be set ; :: thesis: ( f in the Arrows of (EnsCat A) . (i,j) & g in the Arrows of (EnsCat A) . (j,k) & h in the Arrows of (EnsCat A) . (k,l) implies ( the Comp of (EnsCat A) . (i,k,l)) . (h,(( the Comp of (EnsCat A) . (i,j,k)) . (g,f))) = ( the Comp of (EnsCat A) . (i,j,l)) . ((( the Comp of (EnsCat A) . (j,k,l)) . (h,g)),f) )

assume that

A2: f in the Arrows of (EnsCat A) . (i,j) and

A3: g in the Arrows of (EnsCat A) . (j,k) and

A4: h in the Arrows of (EnsCat A) . (k,l) ; :: thesis: ( the Comp of (EnsCat A) . (i,k,l)) . (h,(( the Comp of (EnsCat A) . (i,j,k)) . (g,f))) = ( the Comp of (EnsCat A) . (i,j,l)) . ((( the Comp of (EnsCat A) . (j,k,l)) . (h,g)),f)

reconsider h99 = h as Morphism of k9,l9 by A4;

reconsider g99 = g as Morphism of j9,k9 by A3;

A5: <^k9,l9^> = Funcs (k,l) by Def14;

( <^i9,j9^> = Funcs (i,j) & <^j9,k9^> = Funcs (j,k) ) by Def14;

then reconsider f9 = f, g9 = g, h9 = h as Function by A2, A3, A4, A5;

A6: the Arrows of (EnsCat A) . (k,l) = <^k9,l9^> ;

A7: <^j9,k9^> <> {} by A3;

then A8: <^j9,l9^> <> {} by A1, A4, A6;

then A9: h99 * g99 = h9 * g9 by A3, A4, Th10;

reconsider f99 = f as Morphism of i9,j9 by A2;

the Arrows of (EnsCat A) . (i,j) = <^i9,j9^> ;

then A10: <^i9,k9^> <> {} by A1, A2, A7;

then A11: g99 * f99 = g9 * f9 by A2, A3, Th10;

A12: <^i9,l9^> <> {} by A1, A4, A6, A10;

A13: ( the Comp of (EnsCat A) . (j,k,l)) . (h,g) = h99 * g99 by A3, A4, Def8;

( the Comp of (EnsCat A) . (i,j,k)) . (g,f) = g99 * f99 by A2, A3, Def8;

hence ( the Comp of (EnsCat A) . (i,k,l)) . (h,(( the Comp of (EnsCat A) . (i,j,k)) . (g,f))) = h99 * (g99 * f99) by A4, A10, Def8

.= h9 * (g9 * f9) by A4, A10, A12, A11, Th10

.= (h9 * g9) * f9 by RELAT_1:36

.= (h99 * g99) * f99 by A2, A8, A12, A9, Th10

.= ( the Comp of (EnsCat A) . (i,j,l)) . ((( the Comp of (EnsCat A) . (j,k,l)) . (h,g)),f) by A2, A8, A13, Def8 ;

:: thesis: verum

end;( the Comp of (EnsCat A) . (i,k,l)) . (h,(( the Comp of (EnsCat A) . (i,j,k)) . (g,f))) = ( the Comp of (EnsCat A) . (i,j,l)) . ((( the Comp of (EnsCat A) . (j,k,l)) . (h,g)),f)

reconsider i9 = i, j9 = j, k9 = k, l9 = l as Object of (EnsCat A) ;

let f, g, h be set ; :: thesis: ( f in the Arrows of (EnsCat A) . (i,j) & g in the Arrows of (EnsCat A) . (j,k) & h in the Arrows of (EnsCat A) . (k,l) implies ( the Comp of (EnsCat A) . (i,k,l)) . (h,(( the Comp of (EnsCat A) . (i,j,k)) . (g,f))) = ( the Comp of (EnsCat A) . (i,j,l)) . ((( the Comp of (EnsCat A) . (j,k,l)) . (h,g)),f) )

assume that

A2: f in the Arrows of (EnsCat A) . (i,j) and

A3: g in the Arrows of (EnsCat A) . (j,k) and

A4: h in the Arrows of (EnsCat A) . (k,l) ; :: thesis: ( the Comp of (EnsCat A) . (i,k,l)) . (h,(( the Comp of (EnsCat A) . (i,j,k)) . (g,f))) = ( the Comp of (EnsCat A) . (i,j,l)) . ((( the Comp of (EnsCat A) . (j,k,l)) . (h,g)),f)

reconsider h99 = h as Morphism of k9,l9 by A4;

reconsider g99 = g as Morphism of j9,k9 by A3;

A5: <^k9,l9^> = Funcs (k,l) by Def14;

( <^i9,j9^> = Funcs (i,j) & <^j9,k9^> = Funcs (j,k) ) by Def14;

then reconsider f9 = f, g9 = g, h9 = h as Function by A2, A3, A4, A5;

A6: the Arrows of (EnsCat A) . (k,l) = <^k9,l9^> ;

A7: <^j9,k9^> <> {} by A3;

then A8: <^j9,l9^> <> {} by A1, A4, A6;

then A9: h99 * g99 = h9 * g9 by A3, A4, Th10;

reconsider f99 = f as Morphism of i9,j9 by A2;

the Arrows of (EnsCat A) . (i,j) = <^i9,j9^> ;

then A10: <^i9,k9^> <> {} by A1, A2, A7;

then A11: g99 * f99 = g9 * f9 by A2, A3, Th10;

A12: <^i9,l9^> <> {} by A1, A4, A6, A10;

A13: ( the Comp of (EnsCat A) . (j,k,l)) . (h,g) = h99 * g99 by A3, A4, Def8;

( the Comp of (EnsCat A) . (i,j,k)) . (g,f) = g99 * f99 by A2, A3, Def8;

hence ( the Comp of (EnsCat A) . (i,k,l)) . (h,(( the Comp of (EnsCat A) . (i,j,k)) . (g,f))) = h99 * (g99 * f99) by A4, A10, Def8

.= h9 * (g9 * f9) by A4, A10, A12, A11, Th10

.= (h9 * g9) * f9 by RELAT_1:36

.= (h99 * g99) * f99 by A2, A8, A12, A9, Th10

.= ( the Comp of (EnsCat A) . (i,j,l)) . ((( the Comp of (EnsCat A) . (j,k,l)) . (h,g)),f) by A2, A8, A13, Def8 ;

:: thesis: verum

proof

let i be Element of (EnsCat A); :: according to ALTCAT_1:def 6 :: thesis: ex e being set st
let i be Element of (EnsCat A); :: according to ALTCAT_1:def 7 :: thesis: ex e being set st

( e in the Arrows of (EnsCat A) . (i,i) & ( for i being Element of the carrier of (EnsCat A)

for f being set st f in the Arrows of (EnsCat A) . (i,i) holds

( the Comp of (EnsCat A) . (i,i,i)) . (e,f) = f ) )

reconsider i9 = i as Object of (EnsCat A) ;

take id i ; :: thesis: ( id i in the Arrows of (EnsCat A) . (i,i) & ( for i being Element of the carrier of (EnsCat A)

for f being set st f in the Arrows of (EnsCat A) . (i,i) holds

( the Comp of (EnsCat A) . (i,i,i)) . ((id i),f) = f ) )

A14: <^i9,i9^> = Funcs (i,i) by Def14;

hence id i in the Arrows of (EnsCat A) . (i,i) by FUNCT_2:126; :: thesis: for i being Element of the carrier of (EnsCat A)

for f being set st f in the Arrows of (EnsCat A) . (i,i) holds

( the Comp of (EnsCat A) . (i,i,i)) . ((id i),f) = f

reconsider I = id i as Morphism of i9,i9 by A14, FUNCT_2:126;

let j be Element of (EnsCat A); :: thesis: for f being set st f in the Arrows of (EnsCat A) . (j,i) holds

( the Comp of (EnsCat A) . (j,i,i)) . ((id i),f) = f

let f be set ; :: thesis: ( f in the Arrows of (EnsCat A) . (j,i) implies ( the Comp of (EnsCat A) . (j,i,i)) . ((id i),f) = f )

reconsider j9 = j as Object of (EnsCat A) ;

assume A15: f in the Arrows of (EnsCat A) . (j,i) ; :: thesis: ( the Comp of (EnsCat A) . (j,i,i)) . ((id i),f) = f

then reconsider f99 = f as Morphism of j9,i9 ;

<^j9,i9^> = Funcs (j,i) by Def14;

then reconsider f9 = f as Function of j,i by A15, FUNCT_2:66;

thus ( the Comp of (EnsCat A) . (j,i,i)) . ((id i),f) = I * f99 by A14, A15, Def8

.= (id i) * f9 by A14, A15, Th10

.= f by FUNCT_2:17 ; :: thesis: verum

end;( e in the Arrows of (EnsCat A) . (i,i) & ( for i being Element of the carrier of (EnsCat A)

for f being set st f in the Arrows of (EnsCat A) . (i,i) holds

( the Comp of (EnsCat A) . (i,i,i)) . (e,f) = f ) )

reconsider i9 = i as Object of (EnsCat A) ;

take id i ; :: thesis: ( id i in the Arrows of (EnsCat A) . (i,i) & ( for i being Element of the carrier of (EnsCat A)

for f being set st f in the Arrows of (EnsCat A) . (i,i) holds

( the Comp of (EnsCat A) . (i,i,i)) . ((id i),f) = f ) )

A14: <^i9,i9^> = Funcs (i,i) by Def14;

hence id i in the Arrows of (EnsCat A) . (i,i) by FUNCT_2:126; :: thesis: for i being Element of the carrier of (EnsCat A)

for f being set st f in the Arrows of (EnsCat A) . (i,i) holds

( the Comp of (EnsCat A) . (i,i,i)) . ((id i),f) = f

reconsider I = id i as Morphism of i9,i9 by A14, FUNCT_2:126;

let j be Element of (EnsCat A); :: thesis: for f being set st f in the Arrows of (EnsCat A) . (j,i) holds

( the Comp of (EnsCat A) . (j,i,i)) . ((id i),f) = f

let f be set ; :: thesis: ( f in the Arrows of (EnsCat A) . (j,i) implies ( the Comp of (EnsCat A) . (j,i,i)) . ((id i),f) = f )

reconsider j9 = j as Object of (EnsCat A) ;

assume A15: f in the Arrows of (EnsCat A) . (j,i) ; :: thesis: ( the Comp of (EnsCat A) . (j,i,i)) . ((id i),f) = f

then reconsider f99 = f as Morphism of j9,i9 ;

<^j9,i9^> = Funcs (j,i) by Def14;

then reconsider f9 = f as Function of j,i by A15, FUNCT_2:66;

thus ( the Comp of (EnsCat A) . (j,i,i)) . ((id i),f) = I * f99 by A14, A15, Def8

.= (id i) * f9 by A14, A15, Th10

.= f by FUNCT_2:17 ; :: thesis: verum

( e in the Arrows of (EnsCat A) . (i,i) & ( for j being Element of the carrier of (EnsCat A)

for f being set st f in the Arrows of (EnsCat A) . (i,j) holds

( the Comp of (EnsCat A) . (i,i,j)) . (f,e) = f ) )

reconsider i9 = i as Object of (EnsCat A) ;

take id i ; :: thesis: ( id i in the Arrows of (EnsCat A) . (i,i) & ( for j being Element of the carrier of (EnsCat A)

for f being set st f in the Arrows of (EnsCat A) . (i,j) holds

( the Comp of (EnsCat A) . (i,i,j)) . (f,(id i)) = f ) )

A16: <^i9,i9^> = Funcs (i,i) by Def14;

hence id i in the Arrows of (EnsCat A) . (i,i) by FUNCT_2:126; :: thesis: for j being Element of the carrier of (EnsCat A)

for f being set st f in the Arrows of (EnsCat A) . (i,j) holds

( the Comp of (EnsCat A) . (i,i,j)) . (f,(id i)) = f

reconsider I = id i as Morphism of i9,i9 by A16, FUNCT_2:126;

let j be Element of (EnsCat A); :: thesis: for f being set st f in the Arrows of (EnsCat A) . (i,j) holds

( the Comp of (EnsCat A) . (i,i,j)) . (f,(id i)) = f

let f be set ; :: thesis: ( f in the Arrows of (EnsCat A) . (i,j) implies ( the Comp of (EnsCat A) . (i,i,j)) . (f,(id i)) = f )

reconsider j9 = j as Object of (EnsCat A) ;

assume A17: f in the Arrows of (EnsCat A) . (i,j) ; :: thesis: ( the Comp of (EnsCat A) . (i,i,j)) . (f,(id i)) = f

then reconsider f99 = f as Morphism of i9,j9 ;

<^i9,j9^> = Funcs (i,j) by Def14;

then reconsider f9 = f as Function of i,j by A17, FUNCT_2:66;

thus ( the Comp of (EnsCat A) . (i,i,j)) . (f,(id i)) = f99 * I by A16, A17, Def8

.= f9 * (id i) by A16, A17, Th10

.= f by FUNCT_2:17 ; :: thesis: verum