defpred S_{1}[ object , object ] means ex D2 being set st

( D2 = $2 & ( for x being set holds

( x in D2 iff ex o1, o2 being Object of C ex m being Morphism of o1,o2 st

( $1 = [o1,o2] & <^o1,o2^> <> {} & <^o2,o1^> <> {} & x = m & m is retraction ) ) ) );

set I = the carrier of C;

A1: for i being object st i in [: the carrier of C, the carrier of C:] holds

ex X being object st S_{1}[i,X]

A8: for i being object st i in [: the carrier of C, the carrier of C:] holds

S_{1}[i,Ar . i]
from PBOOLE:sch 3(A1);

defpred S_{2}[ object , object ] means ex p1, p2, p3 being Object of C st

( $1 = [p1,p2,p3] & $2 = ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] );

A9: for i being object st i in [: the carrier of C, the carrier of C, the carrier of C:] holds

ex j being object st S_{2}[i,j]

A12: for i being object st i in [: the carrier of C, the carrier of C, the carrier of C:] holds

S_{2}[i,Co . i]
from PBOOLE:sch 3(A9);

A13: Ar cc= the Arrows of C

set IT = AltCatStr(# the carrier of C,Ar,Co #);

set J = the carrier of AltCatStr(# the carrier of C,Ar,Co #);

AltCatStr(# the carrier of C,Ar,Co #) is SubCatStr of C

IT is transitive

take IT ; :: thesis: ( the carrier of IT = the carrier of C & the Arrows of IT cc= the Arrows of C & ( for o1, o2 being Object of C

for m being Morphism of o1,o2 holds

( m in the Arrows of IT . (o1,o2) iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction ) ) ) )

thus the carrier of IT = the carrier of C ; :: thesis: ( the Arrows of IT cc= the Arrows of C & ( for o1, o2 being Object of C

for m being Morphism of o1,o2 holds

( m in the Arrows of IT . (o1,o2) iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction ) ) ) )

thus the Arrows of IT cc= the Arrows of C by A13; :: thesis: for o1, o2 being Object of C

for m being Morphism of o1,o2 holds

( m in the Arrows of IT . (o1,o2) iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction ) )

let o1, o2 be Object of C; :: thesis: for m being Morphism of o1,o2 holds

( m in the Arrows of IT . (o1,o2) iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction ) )

let m be Morphism of o1,o2; :: thesis: ( m in the Arrows of IT . (o1,o2) iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction ) )

A71: [o1,o2] in [: the carrier of C, the carrier of C:] by ZFMISC_1:def 2;

thus ( m in the Arrows of IT . (o1,o2) implies ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction ) ) :: thesis: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction implies m in the Arrows of IT . (o1,o2) )

S_{1}[[o1,o2],Ar . [o1,o2]]
by A8, A71;

hence m in the Arrows of IT . (o1,o2) by A75; :: thesis: verum

( D2 = $2 & ( for x being set holds

( x in D2 iff ex o1, o2 being Object of C ex m being Morphism of o1,o2 st

( $1 = [o1,o2] & <^o1,o2^> <> {} & <^o2,o1^> <> {} & x = m & m is retraction ) ) ) );

set I = the carrier of C;

A1: for i being object st i in [: the carrier of C, the carrier of C:] holds

ex X being object st S

proof

consider Ar being ManySortedSet of [: the carrier of C, the carrier of C:] such that
let i be object ; :: thesis: ( i in [: the carrier of C, the carrier of C:] implies ex X being object st S_{1}[i,X] )

assume i in [: the carrier of C, the carrier of C:] ; :: thesis: ex X being object st S_{1}[i,X]

then consider o1, o2 being object such that

A2: ( o1 in the carrier of C & o2 in the carrier of C ) and

A3: i = [o1,o2] by ZFMISC_1:84;

reconsider o1 = o1, o2 = o2 as Object of C by A2;

defpred S_{2}[ object ] means ex m being Morphism of o1,o2 st

( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m = $1 & m is retraction );

consider X being set such that

A4: for x being object holds

( x in X iff ( x in the Arrows of C . (o1,o2) & S_{2}[x] ) )
from XBOOLE_0:sch 1();

take X ; :: thesis: S_{1}[i,X]

take X ; :: thesis: ( X = X & ( for x being set holds

( x in X iff ex o1, o2 being Object of C ex m being Morphism of o1,o2 st

( i = [o1,o2] & <^o1,o2^> <> {} & <^o2,o1^> <> {} & x = m & m is retraction ) ) ) )

thus X = X ; :: thesis: for x being set holds

( x in X iff ex o1, o2 being Object of C ex m being Morphism of o1,o2 st

( i = [o1,o2] & <^o1,o2^> <> {} & <^o2,o1^> <> {} & x = m & m is retraction ) )

let x be set ; :: thesis: ( x in X iff ex o1, o2 being Object of C ex m being Morphism of o1,o2 st

( i = [o1,o2] & <^o1,o2^> <> {} & <^o2,o1^> <> {} & x = m & m is retraction ) )

thus ( x in X implies ex o1, o2 being Object of C ex m being Morphism of o1,o2 st

( i = [o1,o2] & <^o1,o2^> <> {} & <^o2,o1^> <> {} & x = m & m is retraction ) ) :: thesis: ( ex o1, o2 being Object of C ex m being Morphism of o1,o2 st

( i = [o1,o2] & <^o1,o2^> <> {} & <^o2,o1^> <> {} & x = m & m is retraction ) implies x in X )

A7: ( <^p1,p2^> <> {} & <^p2,p1^> <> {} & x = m & m is retraction ) ; :: thesis: x in X

( o1 = p1 & o2 = p2 ) by A3, A6, XTUPLE_0:1;

hence x in X by A4, A7; :: thesis: verum

end;assume i in [: the carrier of C, the carrier of C:] ; :: thesis: ex X being object st S

then consider o1, o2 being object such that

A2: ( o1 in the carrier of C & o2 in the carrier of C ) and

A3: i = [o1,o2] by ZFMISC_1:84;

reconsider o1 = o1, o2 = o2 as Object of C by A2;

defpred S

( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m = $1 & m is retraction );

consider X being set such that

A4: for x being object holds

( x in X iff ( x in the Arrows of C . (o1,o2) & S

take X ; :: thesis: S

take X ; :: thesis: ( X = X & ( for x being set holds

( x in X iff ex o1, o2 being Object of C ex m being Morphism of o1,o2 st

( i = [o1,o2] & <^o1,o2^> <> {} & <^o2,o1^> <> {} & x = m & m is retraction ) ) ) )

thus X = X ; :: thesis: for x being set holds

( x in X iff ex o1, o2 being Object of C ex m being Morphism of o1,o2 st

( i = [o1,o2] & <^o1,o2^> <> {} & <^o2,o1^> <> {} & x = m & m is retraction ) )

let x be set ; :: thesis: ( x in X iff ex o1, o2 being Object of C ex m being Morphism of o1,o2 st

( i = [o1,o2] & <^o1,o2^> <> {} & <^o2,o1^> <> {} & x = m & m is retraction ) )

thus ( x in X implies ex o1, o2 being Object of C ex m being Morphism of o1,o2 st

( i = [o1,o2] & <^o1,o2^> <> {} & <^o2,o1^> <> {} & x = m & m is retraction ) ) :: thesis: ( ex o1, o2 being Object of C ex m being Morphism of o1,o2 st

( i = [o1,o2] & <^o1,o2^> <> {} & <^o2,o1^> <> {} & x = m & m is retraction ) implies x in X )

proof

given p1, p2 being Object of C, m being Morphism of p1,p2 such that A6:
i = [p1,p2]
and
assume
x in X
; :: thesis: ex o1, o2 being Object of C ex m being Morphism of o1,o2 st

( i = [o1,o2] & <^o1,o2^> <> {} & <^o2,o1^> <> {} & x = m & m is retraction )

then consider m being Morphism of o1,o2 such that

A5: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m = x & m is retraction ) by A4;

take o1 ; :: thesis: ex o2 being Object of C ex m being Morphism of o1,o2 st

( i = [o1,o2] & <^o1,o2^> <> {} & <^o2,o1^> <> {} & x = m & m is retraction )

take o2 ; :: thesis: ex m being Morphism of o1,o2 st

( i = [o1,o2] & <^o1,o2^> <> {} & <^o2,o1^> <> {} & x = m & m is retraction )

take m ; :: thesis: ( i = [o1,o2] & <^o1,o2^> <> {} & <^o2,o1^> <> {} & x = m & m is retraction )

thus ( i = [o1,o2] & <^o1,o2^> <> {} & <^o2,o1^> <> {} & x = m & m is retraction ) by A3, A5; :: thesis: verum

end;( i = [o1,o2] & <^o1,o2^> <> {} & <^o2,o1^> <> {} & x = m & m is retraction )

then consider m being Morphism of o1,o2 such that

A5: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m = x & m is retraction ) by A4;

take o1 ; :: thesis: ex o2 being Object of C ex m being Morphism of o1,o2 st

( i = [o1,o2] & <^o1,o2^> <> {} & <^o2,o1^> <> {} & x = m & m is retraction )

take o2 ; :: thesis: ex m being Morphism of o1,o2 st

( i = [o1,o2] & <^o1,o2^> <> {} & <^o2,o1^> <> {} & x = m & m is retraction )

take m ; :: thesis: ( i = [o1,o2] & <^o1,o2^> <> {} & <^o2,o1^> <> {} & x = m & m is retraction )

thus ( i = [o1,o2] & <^o1,o2^> <> {} & <^o2,o1^> <> {} & x = m & m is retraction ) by A3, A5; :: thesis: verum

A7: ( <^p1,p2^> <> {} & <^p2,p1^> <> {} & x = m & m is retraction ) ; :: thesis: x in X

( o1 = p1 & o2 = p2 ) by A3, A6, XTUPLE_0:1;

hence x in X by A4, A7; :: thesis: verum

A8: for i being object st i in [: the carrier of C, the carrier of C:] holds

S

defpred S

( $1 = [p1,p2,p3] & $2 = ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] );

A9: for i being object st i in [: the carrier of C, the carrier of C, the carrier of C:] holds

ex j being object st S

proof

consider Co being ManySortedSet of [: the carrier of C, the carrier of C, the carrier of C:] such that
let i be object ; :: thesis: ( i in [: the carrier of C, the carrier of C, the carrier of C:] implies ex j being object st S_{2}[i,j] )

assume i in [: the carrier of C, the carrier of C, the carrier of C:] ; :: thesis: ex j being object st S_{2}[i,j]

then consider p1, p2, p3 being object such that

A10: ( p1 in the carrier of C & p2 in the carrier of C & p3 in the carrier of C ) and

A11: i = [p1,p2,p3] by MCART_1:68;

reconsider p1 = p1, p2 = p2, p3 = p3 as Object of C by A10;

take ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] ; :: thesis: S_{2}[i,( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):]]

take p1 ; :: thesis: ex p2, p3 being Object of C st

( i = [p1,p2,p3] & ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] = ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] )

take p2 ; :: thesis: ex p3 being Object of C st

( i = [p1,p2,p3] & ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] = ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] )

take p3 ; :: thesis: ( i = [p1,p2,p3] & ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] = ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] )

thus i = [p1,p2,p3] by A11; :: thesis: ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] = ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):]

thus ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] = ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] ; :: thesis: verum

end;assume i in [: the carrier of C, the carrier of C, the carrier of C:] ; :: thesis: ex j being object st S

then consider p1, p2, p3 being object such that

A10: ( p1 in the carrier of C & p2 in the carrier of C & p3 in the carrier of C ) and

A11: i = [p1,p2,p3] by MCART_1:68;

reconsider p1 = p1, p2 = p2, p3 = p3 as Object of C by A10;

take ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] ; :: thesis: S

take p1 ; :: thesis: ex p2, p3 being Object of C st

( i = [p1,p2,p3] & ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] = ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] )

take p2 ; :: thesis: ex p3 being Object of C st

( i = [p1,p2,p3] & ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] = ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] )

take p3 ; :: thesis: ( i = [p1,p2,p3] & ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] = ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] )

thus i = [p1,p2,p3] by A11; :: thesis: ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] = ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):]

thus ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] = ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] ; :: thesis: verum

A12: for i being object st i in [: the carrier of C, the carrier of C, the carrier of C:] holds

S

A13: Ar cc= the Arrows of C

proof

Co is ManySortedFunction of {|Ar,Ar|},{|Ar|}
thus
[: the carrier of C, the carrier of C:] c= [: the carrier of C, the carrier of C:]
; :: according to ALTCAT_2:def 2 :: thesis: for b_{1} being set holds

( not b_{1} in [: the carrier of C, the carrier of C:] or Ar . b_{1} c= the Arrows of C . b_{1} )

let i be set ; :: thesis: ( not i in [: the carrier of C, the carrier of C:] or Ar . i c= the Arrows of C . i )

assume A14: i in [: the carrier of C, the carrier of C:] ; :: thesis: Ar . i c= the Arrows of C . i

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in Ar . i or q in the Arrows of C . i )

assume A15: q in Ar . i ; :: thesis: q in the Arrows of C . i

S_{1}[i,Ar . i]
by A8, A14;

then ex p1, p2 being Object of C ex m being Morphism of p1,p2 st

( i = [p1,p2] & <^p1,p2^> <> {} & <^p2,p1^> <> {} & q = m & m is retraction ) by A15;

hence q in the Arrows of C . i ; :: thesis: verum

end;( not b

let i be set ; :: thesis: ( not i in [: the carrier of C, the carrier of C:] or Ar . i c= the Arrows of C . i )

assume A14: i in [: the carrier of C, the carrier of C:] ; :: thesis: Ar . i c= the Arrows of C . i

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in Ar . i or q in the Arrows of C . i )

assume A15: q in Ar . i ; :: thesis: q in the Arrows of C . i

S

then ex p1, p2 being Object of C ex m being Morphism of p1,p2 st

( i = [p1,p2] & <^p1,p2^> <> {} & <^p2,p1^> <> {} & q = m & m is retraction ) by A15;

hence q in the Arrows of C . i ; :: thesis: verum

proof

then reconsider Co = Co as BinComp of Ar ;
let i be object ; :: according to PBOOLE:def 15 :: thesis: ( not i in [: the carrier of C, the carrier of C, the carrier of C:] or Co . i is M3( bool [:({|Ar,Ar|} . i),({|Ar|} . i):]) )

assume i in [: the carrier of C, the carrier of C, the carrier of C:] ; :: thesis: Co . i is M3( bool [:({|Ar,Ar|} . i),({|Ar|} . i):])

then consider p1, p2, p3 being Object of C such that

A16: i = [p1,p2,p3] and

A17: Co . i = ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] by A12;

A18: [p1,p2] in [: the carrier of C, the carrier of C:] by ZFMISC_1:def 2;

then A19: Ar . [p1,p2] c= the Arrows of C . (p1,p2) by A13;

A20: [p2,p3] in [: the carrier of C, the carrier of C:] by ZFMISC_1:def 2;

then Ar . [p2,p3] c= the Arrows of C . (p2,p3) by A13;

then A21: [:(Ar . (p2,p3)),(Ar . (p1,p2)):] c= [:( the Arrows of C . (p2,p3)),( the Arrows of C . (p1,p2)):] by A19, ZFMISC_1:96;

( the Arrows of C . (p1,p3) = {} implies [:( the Arrows of C . (p2,p3)),( the Arrows of C . (p1,p2)):] = {} ) by Lm1;

then reconsider f = Co . i as Function of [:(Ar . (p2,p3)),(Ar . (p1,p2)):],( the Arrows of C . (p1,p3)) by A17, A21, FUNCT_2:32;

A22: Ar . [p1,p2] c= the Arrows of C . [p1,p2] by A13, A18;

A23: Ar . [p2,p3] c= the Arrows of C . [p2,p3] by A13, A20;

A24: ( the Arrows of C . (p1,p3) = {} implies [:(Ar . (p2,p3)),(Ar . (p1,p2)):] = {} )

A29: rng f c= {|Ar|} . i

then [:(Ar . (p2,p3)),(Ar . (p1,p2)):] = {|Ar,Ar|} . i by A16, MULTOP_1:def 1;

hence Co . i is M3( bool [:({|Ar,Ar|} . i),({|Ar|} . i):]) by A24, A29, FUNCT_2:6; :: thesis: verum

end;assume i in [: the carrier of C, the carrier of C, the carrier of C:] ; :: thesis: Co . i is M3( bool [:({|Ar,Ar|} . i),({|Ar|} . i):])

then consider p1, p2, p3 being Object of C such that

A16: i = [p1,p2,p3] and

A17: Co . i = ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] by A12;

A18: [p1,p2] in [: the carrier of C, the carrier of C:] by ZFMISC_1:def 2;

then A19: Ar . [p1,p2] c= the Arrows of C . (p1,p2) by A13;

A20: [p2,p3] in [: the carrier of C, the carrier of C:] by ZFMISC_1:def 2;

then Ar . [p2,p3] c= the Arrows of C . (p2,p3) by A13;

then A21: [:(Ar . (p2,p3)),(Ar . (p1,p2)):] c= [:( the Arrows of C . (p2,p3)),( the Arrows of C . (p1,p2)):] by A19, ZFMISC_1:96;

( the Arrows of C . (p1,p3) = {} implies [:( the Arrows of C . (p2,p3)),( the Arrows of C . (p1,p2)):] = {} ) by Lm1;

then reconsider f = Co . i as Function of [:(Ar . (p2,p3)),(Ar . (p1,p2)):],( the Arrows of C . (p1,p3)) by A17, A21, FUNCT_2:32;

A22: Ar . [p1,p2] c= the Arrows of C . [p1,p2] by A13, A18;

A23: Ar . [p2,p3] c= the Arrows of C . [p2,p3] by A13, A20;

A24: ( the Arrows of C . (p1,p3) = {} implies [:(Ar . (p2,p3)),(Ar . (p1,p2)):] = {} )

proof

A28:
{|Ar|} . (p1,p2,p3) = Ar . (p1,p3)
by ALTCAT_1:def 3;
assume A25:
the Arrows of C . (p1,p3) = {}
; :: thesis: [:(Ar . (p2,p3)),(Ar . (p1,p2)):] = {}

assume [:(Ar . (p2,p3)),(Ar . (p1,p2)):] <> {} ; :: thesis: contradiction

then consider k being object such that

A26: k in [:(Ar . (p2,p3)),(Ar . (p1,p2)):] by XBOOLE_0:def 1;

consider u1, u2 being object such that

A27: ( u1 in Ar . (p2,p3) & u2 in Ar . (p1,p2) ) and

k = [u1,u2] by A26, ZFMISC_1:def 2;

( u1 in <^p2,p3^> & u2 in <^p1,p2^> ) by A23, A22, A27;

then <^p1,p3^> <> {} by ALTCAT_1:def 2;

hence contradiction by A25; :: thesis: verum

end;assume [:(Ar . (p2,p3)),(Ar . (p1,p2)):] <> {} ; :: thesis: contradiction

then consider k being object such that

A26: k in [:(Ar . (p2,p3)),(Ar . (p1,p2)):] by XBOOLE_0:def 1;

consider u1, u2 being object such that

A27: ( u1 in Ar . (p2,p3) & u2 in Ar . (p1,p2) ) and

k = [u1,u2] by A26, ZFMISC_1:def 2;

( u1 in <^p2,p3^> & u2 in <^p1,p2^> ) by A23, A22, A27;

then <^p1,p3^> <> {} by ALTCAT_1:def 2;

hence contradiction by A25; :: thesis: verum

A29: rng f c= {|Ar|} . i

proof

{|Ar,Ar|} . (p1,p2,p3) = [:(Ar . (p2,p3)),(Ar . (p1,p2)):]
by ALTCAT_1:def 4;
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in rng f or q in {|Ar|} . i )

assume q in rng f ; :: thesis: q in {|Ar|} . i

then consider x being object such that

A30: x in dom f and

A31: q = f . x by FUNCT_1:def 3;

A32: dom f = [:(Ar . (p2,p3)),(Ar . (p1,p2)):] by A24, FUNCT_2:def 1;

then consider m1, m2 being object such that

A33: m1 in Ar . (p2,p3) and

A34: m2 in Ar . (p1,p2) and

A35: x = [m1,m2] by A30, ZFMISC_1:84;

[p2,p3] in [: the carrier of C, the carrier of C:] by ZFMISC_1:def 2;

then S_{1}[[p2,p3],Ar . [p2,p3]]
by A8;

then consider q2, q3 being Object of C, qq being Morphism of q2,q3 such that

A36: [p2,p3] = [q2,q3] and

A37: <^q2,q3^> <> {} and

A38: <^q3,q2^> <> {} and

A39: m1 = qq and

A40: qq is retraction by A33;

[p1,p2] in [: the carrier of C, the carrier of C:] by ZFMISC_1:def 2;

then S_{1}[[p1,p2],Ar . [p1,p2]]
by A8;

then consider r1, r2 being Object of C, rr being Morphism of r1,r2 such that

A41: [p1,p2] = [r1,r2] and

A42: <^r1,r2^> <> {} and

A43: <^r2,r1^> <> {} and

A44: m2 = rr and

A45: rr is retraction by A34;

A46: ex o1, o3 being Object of C ex m being Morphism of o1,o3 st

( [p1,p3] = [o1,o3] & <^o1,o3^> <> {} & <^o3,o1^> <> {} & q = m & m is retraction )

then S_{1}[[p1,p3],Ar . [p1,p3]]
by A8;

then q in Ar . [p1,p3] by A46;

hence q in {|Ar|} . i by A16, A28, MULTOP_1:def 1; :: thesis: verum

end;assume q in rng f ; :: thesis: q in {|Ar|} . i

then consider x being object such that

A30: x in dom f and

A31: q = f . x by FUNCT_1:def 3;

A32: dom f = [:(Ar . (p2,p3)),(Ar . (p1,p2)):] by A24, FUNCT_2:def 1;

then consider m1, m2 being object such that

A33: m1 in Ar . (p2,p3) and

A34: m2 in Ar . (p1,p2) and

A35: x = [m1,m2] by A30, ZFMISC_1:84;

[p2,p3] in [: the carrier of C, the carrier of C:] by ZFMISC_1:def 2;

then S

then consider q2, q3 being Object of C, qq being Morphism of q2,q3 such that

A36: [p2,p3] = [q2,q3] and

A37: <^q2,q3^> <> {} and

A38: <^q3,q2^> <> {} and

A39: m1 = qq and

A40: qq is retraction by A33;

[p1,p2] in [: the carrier of C, the carrier of C:] by ZFMISC_1:def 2;

then S

then consider r1, r2 being Object of C, rr being Morphism of r1,r2 such that

A41: [p1,p2] = [r1,r2] and

A42: <^r1,r2^> <> {} and

A43: <^r2,r1^> <> {} and

A44: m2 = rr and

A45: rr is retraction by A34;

A46: ex o1, o3 being Object of C ex m being Morphism of o1,o3 st

( [p1,p3] = [o1,o3] & <^o1,o3^> <> {} & <^o3,o1^> <> {} & q = m & m is retraction )

proof

[p1,p3] in [: the carrier of C, the carrier of C:]
by ZFMISC_1:def 2;
A47:
p2 = q2
by A36, XTUPLE_0:1;

then reconsider mm = qq as Morphism of r2,q3 by A41, XTUPLE_0:1;

take r1 ; :: thesis: ex o3 being Object of C ex m being Morphism of r1,o3 st

( [p1,p3] = [r1,o3] & <^r1,o3^> <> {} & <^o3,r1^> <> {} & q = m & m is retraction )

take q3 ; :: thesis: ex m being Morphism of r1,q3 st

( [p1,p3] = [r1,q3] & <^r1,q3^> <> {} & <^q3,r1^> <> {} & q = m & m is retraction )

take mm * rr ; :: thesis: ( [p1,p3] = [r1,q3] & <^r1,q3^> <> {} & <^q3,r1^> <> {} & q = mm * rr & mm * rr is retraction )

A48: p1 = r1 by A41, XTUPLE_0:1;

hence [p1,p3] = [r1,q3] by A36, XTUPLE_0:1; :: thesis: ( <^r1,q3^> <> {} & <^q3,r1^> <> {} & q = mm * rr & mm * rr is retraction )

A49: r2 = p2 by A41, XTUPLE_0:1;

hence A50: ( <^r1,q3^> <> {} & <^q3,r1^> <> {} ) by A37, A38, A42, A43, A47, ALTCAT_1:def 2; :: thesis: ( q = mm * rr & mm * rr is retraction )

A51: p3 = q3 by A36, XTUPLE_0:1;

thus q = ( the Comp of C . (p1,p2,p3)) . (mm,rr) by A17, A30, A31, A32, A35, A39, A44, FUNCT_1:49

.= mm * rr by A36, A37, A42, A49, A48, A51, ALTCAT_1:def 8 ; :: thesis: mm * rr is retraction

thus mm * rr is retraction by A37, A40, A42, A45, A49, A47, A50, ALTCAT_3:18; :: thesis: verum

end;then reconsider mm = qq as Morphism of r2,q3 by A41, XTUPLE_0:1;

take r1 ; :: thesis: ex o3 being Object of C ex m being Morphism of r1,o3 st

( [p1,p3] = [r1,o3] & <^r1,o3^> <> {} & <^o3,r1^> <> {} & q = m & m is retraction )

take q3 ; :: thesis: ex m being Morphism of r1,q3 st

( [p1,p3] = [r1,q3] & <^r1,q3^> <> {} & <^q3,r1^> <> {} & q = m & m is retraction )

take mm * rr ; :: thesis: ( [p1,p3] = [r1,q3] & <^r1,q3^> <> {} & <^q3,r1^> <> {} & q = mm * rr & mm * rr is retraction )

A48: p1 = r1 by A41, XTUPLE_0:1;

hence [p1,p3] = [r1,q3] by A36, XTUPLE_0:1; :: thesis: ( <^r1,q3^> <> {} & <^q3,r1^> <> {} & q = mm * rr & mm * rr is retraction )

A49: r2 = p2 by A41, XTUPLE_0:1;

hence A50: ( <^r1,q3^> <> {} & <^q3,r1^> <> {} ) by A37, A38, A42, A43, A47, ALTCAT_1:def 2; :: thesis: ( q = mm * rr & mm * rr is retraction )

A51: p3 = q3 by A36, XTUPLE_0:1;

thus q = ( the Comp of C . (p1,p2,p3)) . (mm,rr) by A17, A30, A31, A32, A35, A39, A44, FUNCT_1:49

.= mm * rr by A36, A37, A42, A49, A48, A51, ALTCAT_1:def 8 ; :: thesis: mm * rr is retraction

thus mm * rr is retraction by A37, A40, A42, A45, A49, A47, A50, ALTCAT_3:18; :: thesis: verum

then S

then q in Ar . [p1,p3] by A46;

hence q in {|Ar|} . i by A16, A28, MULTOP_1:def 1; :: thesis: verum

then [:(Ar . (p2,p3)),(Ar . (p1,p2)):] = {|Ar,Ar|} . i by A16, MULTOP_1:def 1;

hence Co . i is M3( bool [:({|Ar,Ar|} . i),({|Ar|} . i):]) by A24, A29, FUNCT_2:6; :: thesis: verum

set IT = AltCatStr(# the carrier of C,Ar,Co #);

set J = the carrier of AltCatStr(# the carrier of C,Ar,Co #);

AltCatStr(# the carrier of C,Ar,Co #) is SubCatStr of C

proof

then reconsider IT = AltCatStr(# the carrier of C,Ar,Co #) as non empty strict SubCatStr of C ;
thus
the carrier of AltCatStr(# the carrier of C,Ar,Co #) c= the carrier of C
; :: according to ALTCAT_2:def 11 :: thesis: ( the Arrows of AltCatStr(# the carrier of C,Ar,Co #) cc= the Arrows of C & the Comp of AltCatStr(# the carrier of C,Ar,Co #) cc= the Comp of C )

thus the Arrows of AltCatStr(# the carrier of C,Ar,Co #) cc= the Arrows of C by A13; :: thesis: the Comp of AltCatStr(# the carrier of C,Ar,Co #) cc= the Comp of C

thus [: the carrier of AltCatStr(# the carrier of C,Ar,Co #), the carrier of AltCatStr(# the carrier of C,Ar,Co #), the carrier of AltCatStr(# the carrier of C,Ar,Co #):] c= [: the carrier of C, the carrier of C, the carrier of C:] ; :: according to ALTCAT_2:def 2 :: thesis: for b_{1} being set holds

( not b_{1} in [: the carrier of AltCatStr(# the carrier of C,Ar,Co #), the carrier of AltCatStr(# the carrier of C,Ar,Co #), the carrier of AltCatStr(# the carrier of C,Ar,Co #):] or the Comp of AltCatStr(# the carrier of C,Ar,Co #) . b_{1} c= the Comp of C . b_{1} )

let i be set ; :: thesis: ( not i in [: the carrier of AltCatStr(# the carrier of C,Ar,Co #), the carrier of AltCatStr(# the carrier of C,Ar,Co #), the carrier of AltCatStr(# the carrier of C,Ar,Co #):] or the Comp of AltCatStr(# the carrier of C,Ar,Co #) . i c= the Comp of C . i )

assume i in [: the carrier of AltCatStr(# the carrier of C,Ar,Co #), the carrier of AltCatStr(# the carrier of C,Ar,Co #), the carrier of AltCatStr(# the carrier of C,Ar,Co #):] ; :: thesis: the Comp of AltCatStr(# the carrier of C,Ar,Co #) . i c= the Comp of C . i

then consider p1, p2, p3 being Object of C such that

A52: i = [p1,p2,p3] and

A53: Co . i = ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] by A12;

A54: ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] c= the Comp of C . (p1,p2,p3) by RELAT_1:59;

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in the Comp of AltCatStr(# the carrier of C,Ar,Co #) . i or q in the Comp of C . i )

assume q in the Comp of AltCatStr(# the carrier of C,Ar,Co #) . i ; :: thesis: q in the Comp of C . i

then q in the Comp of C . (p1,p2,p3) by A53, A54;

hence q in the Comp of C . i by A52, MULTOP_1:def 1; :: thesis: verum

end;thus the Arrows of AltCatStr(# the carrier of C,Ar,Co #) cc= the Arrows of C by A13; :: thesis: the Comp of AltCatStr(# the carrier of C,Ar,Co #) cc= the Comp of C

thus [: the carrier of AltCatStr(# the carrier of C,Ar,Co #), the carrier of AltCatStr(# the carrier of C,Ar,Co #), the carrier of AltCatStr(# the carrier of C,Ar,Co #):] c= [: the carrier of C, the carrier of C, the carrier of C:] ; :: according to ALTCAT_2:def 2 :: thesis: for b

( not b

let i be set ; :: thesis: ( not i in [: the carrier of AltCatStr(# the carrier of C,Ar,Co #), the carrier of AltCatStr(# the carrier of C,Ar,Co #), the carrier of AltCatStr(# the carrier of C,Ar,Co #):] or the Comp of AltCatStr(# the carrier of C,Ar,Co #) . i c= the Comp of C . i )

assume i in [: the carrier of AltCatStr(# the carrier of C,Ar,Co #), the carrier of AltCatStr(# the carrier of C,Ar,Co #), the carrier of AltCatStr(# the carrier of C,Ar,Co #):] ; :: thesis: the Comp of AltCatStr(# the carrier of C,Ar,Co #) . i c= the Comp of C . i

then consider p1, p2, p3 being Object of C such that

A52: i = [p1,p2,p3] and

A53: Co . i = ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] by A12;

A54: ( the Comp of C . (p1,p2,p3)) | [:(Ar . (p2,p3)),(Ar . (p1,p2)):] c= the Comp of C . (p1,p2,p3) by RELAT_1:59;

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in the Comp of AltCatStr(# the carrier of C,Ar,Co #) . i or q in the Comp of C . i )

assume q in the Comp of AltCatStr(# the carrier of C,Ar,Co #) . i ; :: thesis: q in the Comp of C . i

then q in the Comp of C . (p1,p2,p3) by A53, A54;

hence q in the Comp of C . i by A52, MULTOP_1:def 1; :: thesis: verum

IT is transitive

proof

then reconsider IT = IT as non empty transitive strict SubCatStr of C ;
let p1, p2, p3 be Object of IT; :: according to ALTCAT_1:def 2 :: thesis: ( <^p1,p2^> = {} or <^p2,p3^> = {} or not <^p1,p3^> = {} )

assume that

A55: <^p1,p2^> <> {} and

A56: <^p2,p3^> <> {} ; :: thesis: not <^p1,p3^> = {}

consider m2 being object such that

A57: m2 in <^p1,p2^> by A55, XBOOLE_0:def 1;

consider m1 being object such that

A58: m1 in <^p2,p3^> by A56, XBOOLE_0:def 1;

[p2,p3] in [: the carrier of C, the carrier of C:] by ZFMISC_1:def 2;

then S_{1}[[p2,p3],Ar . [p2,p3]]
by A8;

then consider q2, q3 being Object of C, qq being Morphism of q2,q3 such that

A59: [p2,p3] = [q2,q3] and

A60: <^q2,q3^> <> {} and

A61: <^q3,q2^> <> {} and

m1 = qq and

A62: qq is retraction by A58;

[p1,p2] in [: the carrier of C, the carrier of C:] by ZFMISC_1:def 2;

then S_{1}[[p1,p2],Ar . [p1,p2]]
by A8;

then consider r1, r2 being Object of C, rr being Morphism of r1,r2 such that

A63: [p1,p2] = [r1,r2] and

A64: <^r1,r2^> <> {} and

A65: <^r2,r1^> <> {} and

m2 = rr and

A66: rr is retraction by A57;

A67: p2 = q2 by A59, XTUPLE_0:1;

then reconsider mm = qq as Morphism of r2,q3 by A63, XTUPLE_0:1;

A68: r2 = p2 by A63, XTUPLE_0:1;

A69: ex o1, o3 being Object of C ex m being Morphism of o1,o3 st

( [p1,p3] = [o1,o3] & <^o1,o3^> <> {} & <^o3,o1^> <> {} & mm * rr = m & m is retraction )

then S_{1}[[p1,p3],Ar . [p1,p3]]
by A8;

hence not <^p1,p3^> = {} by A69; :: thesis: verum

end;assume that

A55: <^p1,p2^> <> {} and

A56: <^p2,p3^> <> {} ; :: thesis: not <^p1,p3^> = {}

consider m2 being object such that

A57: m2 in <^p1,p2^> by A55, XBOOLE_0:def 1;

consider m1 being object such that

A58: m1 in <^p2,p3^> by A56, XBOOLE_0:def 1;

[p2,p3] in [: the carrier of C, the carrier of C:] by ZFMISC_1:def 2;

then S

then consider q2, q3 being Object of C, qq being Morphism of q2,q3 such that

A59: [p2,p3] = [q2,q3] and

A60: <^q2,q3^> <> {} and

A61: <^q3,q2^> <> {} and

m1 = qq and

A62: qq is retraction by A58;

[p1,p2] in [: the carrier of C, the carrier of C:] by ZFMISC_1:def 2;

then S

then consider r1, r2 being Object of C, rr being Morphism of r1,r2 such that

A63: [p1,p2] = [r1,r2] and

A64: <^r1,r2^> <> {} and

A65: <^r2,r1^> <> {} and

m2 = rr and

A66: rr is retraction by A57;

A67: p2 = q2 by A59, XTUPLE_0:1;

then reconsider mm = qq as Morphism of r2,q3 by A63, XTUPLE_0:1;

A68: r2 = p2 by A63, XTUPLE_0:1;

A69: ex o1, o3 being Object of C ex m being Morphism of o1,o3 st

( [p1,p3] = [o1,o3] & <^o1,o3^> <> {} & <^o3,o1^> <> {} & mm * rr = m & m is retraction )

proof

[p1,p3] in [: the carrier of C, the carrier of C:]
by ZFMISC_1:def 2;
take
r1
; :: thesis: ex o3 being Object of C ex m being Morphism of r1,o3 st

( [p1,p3] = [r1,o3] & <^r1,o3^> <> {} & <^o3,r1^> <> {} & mm * rr = m & m is retraction )

take q3 ; :: thesis: ex m being Morphism of r1,q3 st

( [p1,p3] = [r1,q3] & <^r1,q3^> <> {} & <^q3,r1^> <> {} & mm * rr = m & m is retraction )

take mm * rr ; :: thesis: ( [p1,p3] = [r1,q3] & <^r1,q3^> <> {} & <^q3,r1^> <> {} & mm * rr = mm * rr & mm * rr is retraction )

p1 = r1 by A63, XTUPLE_0:1;

hence [p1,p3] = [r1,q3] by A59, XTUPLE_0:1; :: thesis: ( <^r1,q3^> <> {} & <^q3,r1^> <> {} & mm * rr = mm * rr & mm * rr is retraction )

thus A70: ( <^r1,q3^> <> {} & <^q3,r1^> <> {} ) by A60, A61, A64, A65, A68, A67, ALTCAT_1:def 2; :: thesis: ( mm * rr = mm * rr & mm * rr is retraction )

thus mm * rr = mm * rr ; :: thesis: mm * rr is retraction

thus mm * rr is retraction by A60, A62, A64, A66, A68, A67, A70, ALTCAT_3:18; :: thesis: verum

end;( [p1,p3] = [r1,o3] & <^r1,o3^> <> {} & <^o3,r1^> <> {} & mm * rr = m & m is retraction )

take q3 ; :: thesis: ex m being Morphism of r1,q3 st

( [p1,p3] = [r1,q3] & <^r1,q3^> <> {} & <^q3,r1^> <> {} & mm * rr = m & m is retraction )

take mm * rr ; :: thesis: ( [p1,p3] = [r1,q3] & <^r1,q3^> <> {} & <^q3,r1^> <> {} & mm * rr = mm * rr & mm * rr is retraction )

p1 = r1 by A63, XTUPLE_0:1;

hence [p1,p3] = [r1,q3] by A59, XTUPLE_0:1; :: thesis: ( <^r1,q3^> <> {} & <^q3,r1^> <> {} & mm * rr = mm * rr & mm * rr is retraction )

thus A70: ( <^r1,q3^> <> {} & <^q3,r1^> <> {} ) by A60, A61, A64, A65, A68, A67, ALTCAT_1:def 2; :: thesis: ( mm * rr = mm * rr & mm * rr is retraction )

thus mm * rr = mm * rr ; :: thesis: mm * rr is retraction

thus mm * rr is retraction by A60, A62, A64, A66, A68, A67, A70, ALTCAT_3:18; :: thesis: verum

then S

hence not <^p1,p3^> = {} by A69; :: thesis: verum

take IT ; :: thesis: ( the carrier of IT = the carrier of C & the Arrows of IT cc= the Arrows of C & ( for o1, o2 being Object of C

for m being Morphism of o1,o2 holds

( m in the Arrows of IT . (o1,o2) iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction ) ) ) )

thus the carrier of IT = the carrier of C ; :: thesis: ( the Arrows of IT cc= the Arrows of C & ( for o1, o2 being Object of C

for m being Morphism of o1,o2 holds

( m in the Arrows of IT . (o1,o2) iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction ) ) ) )

thus the Arrows of IT cc= the Arrows of C by A13; :: thesis: for o1, o2 being Object of C

for m being Morphism of o1,o2 holds

( m in the Arrows of IT . (o1,o2) iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction ) )

let o1, o2 be Object of C; :: thesis: for m being Morphism of o1,o2 holds

( m in the Arrows of IT . (o1,o2) iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction ) )

let m be Morphism of o1,o2; :: thesis: ( m in the Arrows of IT . (o1,o2) iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction ) )

A71: [o1,o2] in [: the carrier of C, the carrier of C:] by ZFMISC_1:def 2;

thus ( m in the Arrows of IT . (o1,o2) implies ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction ) ) :: thesis: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction implies m in the Arrows of IT . (o1,o2) )

proof

assume A75:
( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction )
; :: thesis: m in the Arrows of IT . (o1,o2)
assume A72:
m in the Arrows of IT . (o1,o2)
; :: thesis: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction )

S_{1}[[o1,o2],Ar . [o1,o2]]
by A8, A71;

then consider p1, p2 being Object of C, n being Morphism of p1,p2 such that

A73: [o1,o2] = [p1,p2] and

A74: ( <^p1,p2^> <> {} & <^p2,p1^> <> {} & m = n & n is retraction ) by A72;

( o1 = p1 & o2 = p2 ) by A73, XTUPLE_0:1;

hence ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction ) by A74; :: thesis: verum

end;S

then consider p1, p2 being Object of C, n being Morphism of p1,p2 such that

A73: [o1,o2] = [p1,p2] and

A74: ( <^p1,p2^> <> {} & <^p2,p1^> <> {} & m = n & n is retraction ) by A72;

( o1 = p1 & o2 = p2 ) by A73, XTUPLE_0:1;

hence ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction ) by A74; :: thesis: verum

S

hence m in the Arrows of IT . (o1,o2) by A75; :: thesis: verum