:: ALTCAT_2 semantic presentation

theorem Th1: :: ALTCAT_2:1
for b1, b2, b3, b4 being set holds [:(b1 --> b3),(b2 --> b4):] = [:b1,b2:] --> [b3,b4]
proof
let c1, c2 be set ;
let c3, c4 be set ;
E1: ( dom (c1 --> c3) = c1 & dom (c2 --> c4) = c2 ) by FUNCOP_1:19;
then E2: dom ([:c1,c2:] --> [c3,c4]) = [:(dom (c1 --> c3)),(dom (c2 --> c4)):] by FUNCOP_1:19;
now
let c5, c6 be set ;
assume E3: ( c5 in dom (c1 --> c3) & c6 in dom (c2 --> c4) ) ;
then E4: ( (c1 --> c3) . c5 = c3 & (c2 --> c4) . c6 = c4 ) by E1, FUNCOP_1:13;
[c5,c6] in dom ([:c1,c2:] --> [c3,c4]) by E2, E3, ZFMISC_1:106;
then [c5,c6] in [:c1,c2:] by FUNCOP_1:19;
hence ([:c1,c2:] --> [c3,c4]) . [c5,c6] = [((c1 --> c3) . c5),((c2 --> c4) . c6)] by E4, FUNCOP_1:13;
end;
hence [:(c1 --> c3),(c2 --> c4):] = [:c1,c2:] --> [c3,c4] by E2, FUNCT_3:def 9;
end;

registration
let c1 be set ;
cluster [0] a1 -> Function-yielding ;
coherence
[0] c1 is Function-yielding
proof
let c2 be set ; :: according to FUNCOP_1:def 6
assume c2 in dom ([0] c1) ;
thus ([0] c1) . c2 is Function by PBOOLE:5;
end;
end;

theorem Th2: :: ALTCAT_2:2
for b1, b2 being Function holds ~ (b2 * b1) = b2 * (~ b1)
proof
let c1, c2 be Function;
E1: now
let c3 be set ;
hereby
assume E2: c3 in dom (c2 * (~ c1)) ;
then c3 in dom (~ c1) by FUNCT_1:21;
then consider c4, c5 being set such that
E3: c3 = [c5,c4] and
E4: [c4,c5] in dom c1 by FUNCT_4:def 2;
take c6 = c4;
take c7 = c5;
thus c3 = [c7,c6] by E3;
(~ c1) . c3 in dom c2 by E2, FUNCT_1:21;
then c1 . [c6,c7] in dom c2 by E3, E4, FUNCT_4:def 2;
hence [c6,c7] in dom (c2 * c1) by E4, FUNCT_1:21;
end;
given c4, c5 being set such that E2: c3 = [c5,c4] and
E3: [c4,c5] in dom (c2 * c1) ;
E4: [c4,c5] in dom c1 by E3, FUNCT_1:21;
c1 . [c4,c5] in dom c2 by E3, FUNCT_1:21;
then E5: (~ c1) . c3 in dom c2 by E2, E4, FUNCT_4:def 2;
c3 in dom (~ c1) by E2, E4, FUNCT_4:def 2;
hence c3 in dom (c2 * (~ c1)) by E5, FUNCT_1:21;
end;
now
let c3, c4 be set ;
assume E2: [c3,c4] in dom (c2 * c1) ;
then [c3,c4] in dom c1 by FUNCT_1:21;
then E3: [c4,c3] in dom (~ c1) by FUNCT_4:43;
hence (c2 * (~ c1)) . [c4,c3] = c2 . ((~ c1) . [c4,c3]) by FUNCT_1:23
.= c2 . (c1 . [c3,c4]) by E3, FUNCT_4:44
.= (c2 * c1) . [c3,c4] by E2, FUNCT_1:22 ;

end;
hence ~ (c2 * c1) = c2 * (~ c1) by E1, FUNCT_4:def 2;
end;

theorem Th3: :: ALTCAT_2:3
for b1, b2, b3 being Function holds ~ (b1 * [:b2,b3:]) = (~ b1) * [:b3,b2:]
proof
let c1, c2, c3 be Function;
E1: now
let c4 be set ;
hereby
assume E2: c4 in dom ((~ c1) * [:c3,c2:]) ;
then c4 in dom [:c3,c2:] by FUNCT_1:21;
then c4 in [:(dom c3),(dom c2):] by FUNCT_3:def 9;
then consider c5, c6 being set such that
E3: c5 in dom c3 and
E4: c6 in dom c2 and
E5: c4 = [c5,c6] by ZFMISC_1:103;
take c7 = c6;
take c8 = c5;
thus c4 = [c8,c7] by E5;
dom [:c2,c3:] = [:(dom c2),(dom c3):] by FUNCT_3:def 9;
then E6: [c7,c8] in dom [:c2,c3:] by E3, E4, ZFMISC_1:106;
E7: [:c3,c2:] . c4 = [(c3 . c8),(c2 . c7)] by E3, E4, E5, FUNCT_3:def 9;
E8: [:c2,c3:] . [c7,c8] = [(c2 . c7),(c3 . c8)] by E3, E4, FUNCT_3:def 9;
[:c3,c2:] . c4 in dom (~ c1) by E2, FUNCT_1:21;
then [:c2,c3:] . [c7,c8] in dom c1 by E7, E8, FUNCT_4:43;
hence [c7,c8] in dom (c1 * [:c2,c3:]) by E6, FUNCT_1:21;
end;
given c5, c6 being set such that E2: c4 = [c6,c5] and
E3: [c5,c6] in dom (c1 * [:c2,c3:]) ;
E4: [c5,c6] in dom [:c2,c3:] by E3, FUNCT_1:21;
dom [:c2,c3:] = [:(dom c2),(dom c3):] by FUNCT_3:def 9;
then E5: ( c5 in dom c2 & c6 in dom c3 ) by E4, ZFMISC_1:106;
dom [:c3,c2:] = [:(dom c3),(dom c2):] by FUNCT_3:def 9;
then E6: c4 in dom [:c3,c2:] by E2, E5, ZFMISC_1:106;
E7: [:c2,c3:] . [c5,c6] = [(c2 . c5),(c3 . c6)] by E5, FUNCT_3:def 9;
E8: [:c3,c2:] . c4 = [(c3 . c6),(c2 . c5)] by E2, E5, FUNCT_3:def 9;
[:c2,c3:] . [c5,c6] in dom c1 by E3, FUNCT_1:21;
then [:c3,c2:] . c4 in dom (~ c1) by E7, E8, FUNCT_4:43;
hence c4 in dom ((~ c1) * [:c3,c2:]) by E6, FUNCT_1:21;
end;
now
let c4, c5 be set ;
assume E2: [c4,c5] in dom (c1 * [:c2,c3:]) ;
then [c4,c5] in dom [:c2,c3:] by FUNCT_1:21;
then [c4,c5] in [:(dom c2),(dom c3):] by FUNCT_3:def 9;
then E3: ( c4 in dom c2 & c5 in dom c3 ) by ZFMISC_1:106;
[:c2,c3:] . [c4,c5] in dom c1 by E2, FUNCT_1:21;
then E4: [(c2 . c4),(c3 . c5)] in dom c1 by E3, FUNCT_3:def 9;
[c5,c4] in [:(dom c3),(dom c2):] by E3, ZFMISC_1:106;
then [c5,c4] in dom [:c3,c2:] by FUNCT_3:def 9;
hence ((~ c1) * [:c3,c2:]) . [c5,c4] = (~ c1) . ([:c3,c2:] . [c5,c4]) by FUNCT_1:23
.= (~ c1) . [(c3 . c5),(c2 . c4)] by E3, FUNCT_3:def 9
.= c1 . [(c2 . c4),(c3 . c5)] by E4, FUNCT_4:def 2
.= c1 . ([:c2,c3:] . [c4,c5]) by E3, FUNCT_3:def 9
.= (c1 * [:c2,c3:]) . [c4,c5] by E2, FUNCT_1:22 ;

end;
hence ~ (c1 * [:c2,c3:]) = (~ c1) * [:c3,c2:] by E1, FUNCT_4:def 2;
end;

registration
let c1 be Function-yielding Function;
cluster ~ a1 -> Function-yielding ;
coherence
~ c1 is Function-yielding
proof
let c2 be set ; :: according to FUNCOP_1:def 6
assume c2 in dom (~ c1) ;
then consider c3, c4 being set such that
E1: c2 = [c4,c3] and
E2: [c3,c4] in dom c1 by FUNCT_4:def 2;
c1 . [c3,c4] = (~ c1) . c2 by E1, E2, FUNCT_4:def 2;
hence (~ c1) . c2 is Function ;
end;
end;

theorem Th4: :: ALTCAT_2:4
for b1 being set
for b2, b3, b4 being ManySortedSet of b1 holds
( b2 is_transformable_to b3 implies for b5 being ManySortedFunction of b2,b3
for b6 being ManySortedFunction of b3,b4 holds
b6 ** b5 is ManySortedFunction of b2,b4 )
proof
let c1 be set ;
let c2, c3, c4 be ManySortedSet of c1;
assume E1: c2 is_transformable_to c3 ;
let c5 be ManySortedFunction of c2,c3;
let c6 be ManySortedFunction of c3,c4;
reconsider c7 = c6 ** c5 as ManySortedFunction of c1 by MSSUBFAM:15;
c7 is ManySortedFunction of c2,c4
proof
let c8 be set ; :: according to PBOOLE:def 18
assume E2: c8 in c1 ;
then E3: ( c3 . c8 = {} implies c2 . c8 = {} ) by E1, PZFMISC1:def 3;
reconsider c9 = c6 . c8 as Function of c3 . c8,c4 . c8 by E2, PBOOLE:def 18;
reconsider c10 = c5 . c8 as Function of c2 . c8,c3 . c8 by E2, PBOOLE:def 18;
c8 in dom c7 by E2, PBOOLE:def 3;
then (c6 ** c5) . c8 = c9 * c10 by PBOOLE:def 24;
hence c7 . c8 is Function of c2 . c8,c4 . c8 by E3, FUNCT_2:19;
end;
hence c6 ** c5 is ManySortedFunction of c2,c4 ;
end;

definition
let c1 be set ;
let c2 be ManySortedSet of [:c1,c1:];
redefine func ~ as ~ c2 -> ManySortedSet of [:a1,a1:];
coherence
~ c2 is ManySortedSet of [:c1,c1:]
proof
thus dom (~ c2) = [:c1,c1:] by PBOOLE:def 3; :: according to PBOOLE:def 3
end;
end;

theorem Th5: :: ALTCAT_2:5
for b1 being set
for b2 being non empty set
for b3 being Function of b1,b2
for b4, b5 being ManySortedSet of b2
for b6 being ManySortedFunction of b4,b5 holds
b6 * b3 is ManySortedFunction of b4 * b3,b5 * b3
proof
let c1 be set ;
let c2 be non empty set ;
let c3 be Function of c1,c2;
let c4, c5 be ManySortedSet of c2;
let c6 be ManySortedFunction of c4,c5;
let c7 be set ; :: according to PBOOLE:def 18
assume E1: c7 in c1 ;
then E2: c7 in dom c3 by FUNCT_2:def 1;
then E3: ( c4 . (c3 . c7) = (c4 * c3) . c7 & c5 . (c3 . c7) = (c5 * c3) . c7 ) by FUNCT_1:23;
c3 . c7 in c2 by E1, FUNCT_2:7;
then c6 . (c3 . c7) is Function of c4 . (c3 . c7),c5 . (c3 . c7) by PBOOLE:def 18;
hence (c6 * c3) . c7 is Function of (c4 * c3) . c7,(c5 * c3) . c7 by E2, E3, FUNCT_1:23;
end;

definition
let c1 be set ;
let c2, c3 be ManySortedSet of [:c1,c1:];
let c4 be ManySortedFunction of c2,c3;
redefine func ~ as ~ c4 -> ManySortedFunction of ~ a2, ~ a3;
coherence
~ c4 is ManySortedFunction of ~ c2, ~ c3
proof
reconsider c5 = ~ c4 as ManySortedSet of [:c1,c1:] ;
c5 is ManySortedFunction of ~ c2, ~ c3
proof
let c6 be set ; :: according to PBOOLE:def 18
assume c6 in [:c1,c1:] ;
then consider c7, c8 being set such that
E1: ( c7 in c1 & c8 in c1 ) and
E2: c6 = [c7,c8] by ZFMISC_1:103;
E3: [c8,c7] in [:c1,c1:] by E1, ZFMISC_1:106;
dom c4 = [:c1,c1:] by PBOOLE:def 3;
then E4: c4 . [c8,c7] = c5 . c6 by E2, E3, FUNCT_4:def 2;
dom c2 = [:c1,c1:] by PBOOLE:def 3;
then E5: c2 . [c8,c7] = (~ c2) . c6 by E2, E3, FUNCT_4:def 2;
dom c3 = [:c1,c1:] by PBOOLE:def 3;
then c3 . [c8,c7] = (~ c3) . c6 by E2, E3, FUNCT_4:def 2;
hence c5 . c6 is Function of (~ c2) . c6,(~ c3) . c6 by E3, E4, E5, PBOOLE:def 18;
end;
hence ~ c4 is ManySortedFunction of ~ c2, ~ c3 ;
end;
end;

theorem Th6: :: ALTCAT_2:6
for b1, b2 being non empty set
for b3 being ManySortedSet of [:b1,b2:]
for b4 being Element of b1
for b5 being Element of b2 holds (~ b3) . b5,b4 = b3 . b4,b5
proof
let c1, c2 be non empty set ;
let c3 be ManySortedSet of [:c1,c2:];
let c4 be Element of c1;
let c5 be Element of c2;
[c4,c5] in [:c1,c2:] by ZFMISC_1:106;
then E1: [c4,c5] in dom c3 by PBOOLE:def 3;
thus (~ c3) . c5,c4 = c3 . c4,c5 by E1, FUNCT_4:def 2;
end;

definition
let c1 be set ;
let c2, c3 be ManySortedFunction of c1;
redefine func ** as c3 ** c2 -> ManySortedFunction of a1;
coherence
c3 ** c2 is ManySortedFunction of c1
proof
E1: ( dom c2 = c1 & dom c3 = c1 ) by PBOOLE:def 3;
dom (c3 ** c2) = (dom c3) /\ (dom c2) by PBOOLE:def 24
.= c1 by E1 ;
hence c3 ** c2 is ManySortedFunction of c1 by PBOOLE:def 3;
end;
end;

definition
let c1, c2 be Function;
pred c1 cc= c2 means :Def1: :: ALTCAT_2:def 1
( dom a1 c= dom a2 & ( for b1 being set holds
( b1 in dom a1 implies a1 . b1 c= a2 . b1 ) ) );
reflexivity
for b1 being Function holds
( dom b1 c= dom b1 & ( for b2 being set holds
( b2 in dom b1 implies b1 . b2 c= b1 . b2 ) ) ) ;
end;

:: deftheorem Def1 defines cc= ALTCAT_2:def 1 :
for b1, b2 being Function holds
( b1 cc= b2 iff ( dom b1 c= dom b2 & ( for b3 being set holds
( b3 in dom b1 implies b1 . b3 c= b2 . b3 ) ) ) );

definition
let c1, c2 be set ;
let c3 be ManySortedSet of c1;
let c4 be ManySortedSet of c2;
redefine pred cc= as c3 cc= c4 means :Def2: :: ALTCAT_2:def 2
( a1 c= a2 & ( for b1 being set holds
( b1 in a1 implies a3 . b1 c= a4 . b1 ) ) );
compatibility
( c3 cc= c4 iff ( c1 c= c2 & ( for b1 being set holds
( b1 in c1 implies c3 . b1 c= c4 . b1 ) ) ) )
proof
E2: ( dom c3 = c1 & dom c4 = c2 ) by PBOOLE:def 3;
hence ( c3 cc= c4 implies ( c1 c= c2 & ( for b1 being set holds
( b1 in c1 implies c3 . b1 c= c4 . b1 ) ) ) ) by Def1;
assume that
E3: c1 c= c2 and
E4: for b1 being set holds
( b1 in c1 implies c3 . b1 c= c4 . b1 ) ;
thus dom c3 c= dom c4 by E2, E3; :: according to ALTCAT_2:def 1
let c5 be set ;
assume c5 in dom c3 ;
hence c3 . c5 c= c4 . c5 by E2, E4;
end;
end;

:: deftheorem Def2 defines cc= ALTCAT_2:def 2 :
for b1, b2 being set
for b3 being ManySortedSet of b1
for b4 being ManySortedSet of b2 holds
( b3 cc= b4 iff ( b1 c= b2 & ( for b5 being set holds
( b5 in b1 implies b3 . b5 c= b4 . b5 ) ) ) );

theorem Th7: :: ALTCAT_2:7
canceled;

theorem Th8: :: ALTCAT_2:8
for b1, b2 being set
for b3 being ManySortedSet of b1
for b4 being ManySortedSet of b2 holds
( b3 cc= b4 & b4 cc= b3 implies b3 = b4 )
proof
let c1, c2 be set ;
let c3 be ManySortedSet of c1;
let c4 be ManySortedSet of c2;
assume that
E4: c3 cc= c4 and
E5: c4 cc= c3 ;
E6: ( c1 c= c2 & c2 c= c1 ) by E4, E5, Def2;
then reconsider c5 = c4 as ManySortedSet of c1 by XBOOLE_0:def 10;
now
let c6 be set ;
assume c6 in c1 ;
then ( c3 . c6 c= c4 . c6 & c4 . c6 c= c3 . c6 ) by E4, E5, E6, Def2;
hence c3 . c6 = c5 . c6 by XBOOLE_0:def 10;
end;
hence c3 = c4 by PBOOLE:3;
end;

theorem Th9: :: ALTCAT_2:9
for b1, b2, b3 being set
for b4 being ManySortedSet of b1
for b5 being ManySortedSet of b2
for b6 being ManySortedSet of b3 holds
( b4 cc= b5 & b5 cc= b6 implies b4 cc= b6 )
proof
let c1, c2, c3 be set ;
let c4 be ManySortedSet of c1;
let c5 be ManySortedSet of c2;
let c6 be ManySortedSet of c3;
assume that
E5: c4 cc= c5 and
E6: c5 cc= c6 ;
E7: c1 c= c2 by E5, Def2;
c2 c= c3 by E6, Def2;
hence c1 c= c3 by E7, XBOOLE_1:1; :: according to ALTCAT_2:def 2
let c7 be set ;
assume c7 in c1 ;
then ( c4 . c7 c= c5 . c7 & c5 . c7 c= c6 . c7 ) by E5, E6, E7, Def2;
hence c4 . c7 c= c6 . c7 by XBOOLE_1:1;
end;

theorem Th10: :: ALTCAT_2:10
for b1 being set
for b2, b3 being ManySortedSet of b1 holds
( b2 cc= b3 iff b2 c= b3 )
proof
let c1 be set ;
let c2, c3 be ManySortedSet of c1;
thus ( c2 cc= c3 implies c2 c= c3 )
proof
assume E5: c2 cc= c3 ;
let c4 be set ; :: according to PBOOLE:def 5
thus not ( c4 in c1 & not c2 . c4 c= c3 . c4 ) by E5, Def2;
end;
assume E5: c2 c= c3 ;
thus c1 c= c1 ; :: according to ALTCAT_2:def 2
thus for b1 being set holds
( b1 in c1 implies c2 . b1 c= c3 . b1 ) by E5, PBOOLE:def 5;
end;

scheme :: ALTCAT_2:sch 1
s1{ F1() -> non empty set , F2( set ) -> set , P1[ set ] } :
{ [b1,F2(b1)] where B is Element of F1() : P1[b1] } is Function
proof
set c1 = { [b1,F2(b1)] where B is Element of F1() : P1[b1] } ;
E5: { [b1,F2(b1)] where B is Element of F1() : P1[b1] } is Relation-like
proof
let c2 be set ; :: according to RELAT_1:def 1
assume c2 in { [b1,F2(b1)] where B is Element of F1() : P1[b1] } ;
then consider c3 being Element of F1() such that
E6: c2 = [c3,F2(c3)] and
P1[c3] ;
take c3 ;
take F2(c3) ;
thus c2 = [c3,F2(c3)] by E6;
end;
{ [b1,F2(b1)] where B is Element of F1() : P1[b1] } is Function-like
proof
let c2, c3, c4 be set ; :: according to FUNCT_1:def 1
assume [c2,c3] in { [b1,F2(b1)] where B is Element of F1() : P1[b1] } ;
then consider c5 being Element of F1() such that
E6: [c2,c3] = [c5,F2(c5)] and
P1[c5] ;
assume [c2,c4] in { [b1,F2(b1)] where B is Element of F1() : P1[b1] } ;
then consider c6 being Element of F1() such that
E7: [c2,c4] = [c6,F2(c6)] and
P1[c6] ;
( c5 = c2 & c6 = c2 ) by E6, E7, ZFMISC_1:33;
hence c3 = c4 by E6, E7, ZFMISC_1:33;
end;
hence { [b1,F2(b1)] where B is Element of F1() : P1[b1] } is Function by E5;
end;

scheme :: ALTCAT_2:sch 2
s2{ F1() -> non empty set , F2() -> Function, F3( set ) -> set , P1[ set ] } :
dom F2() = { b1 where B is Element of F1() : P1[b1] }
provided
E5: F2() = { [b1,F3(b1)] where B is Element of F1() : P1[b1] }
proof
set c1 = { b1 where B is Element of F1() : P1[b1] } ;
now
let c2 be set ;
hereby
assume c2 in { b1 where B is Element of F1() : P1[b1] } ;
then consider c3 being Element of F1() such that
E6: c2 = c3 and
E7: P1[c3] ;
take c4 = F3(c3);
thus [c2,c4] in F2() by E5, E6, E7;
end;
given c3 being set such that E6: [c2,c3] in F2() ;
consider c4 being Element of F1() such that
E7: [c2,c3] = [c4,F3(c4)] and
E8: P1[c4] by E5, E6;
c2 = c4 by E7, ZFMISC_1:33;
hence c2 in { b1 where B is Element of F1() : P1[b1] } by E8;
end;
hence dom F2() = { b1 where B is Element of F1() : P1[b1] } by RELAT_1:def 4;
end;

scheme :: ALTCAT_2:sch 3
s3{ F1() -> non empty set , F2() -> Function, F3() -> Element of F1(), F4( set ) -> set , P1[ set ] } :
F2() . F3() = F4(F3())
provided
E5: F2() = { [b1,F4(b1)] where B is Element of F1() : P1[b1] } and E6: P1[F3()]
proof
E7: F2() = { [b1,F4(b1)] where B is Element of F1() : P1[b1] } by E5;
dom F2() = { b1 where B is Element of F1() : P1[b1] } from ALTCAT_2:sch 2(E7);
 then E8: F3() in dom F2() by E6;
[F3(),F4(F3())] in { [b1,F4(b1)] where B is Element of F1() : P1[b1] } by E6;
hence F2() . F3() = F4(F3()) by E5, E8, FUNCT_1:def 4;
end;

theorem Th11: :: ALTCAT_2:11
for b1 being Category
for b2, b3, b4 being Object of b1 holds [:(Hom b3,b4),(Hom b2,b3):] c= dom the Comp of b1
proof
let c1 be Category;
let c2, c3, c4 be Object of c1;
let c5 be set ; :: according to TARSKI:def 3
assume E6: c5 in [:(Hom c3,c4),(Hom c2,c3):] ;
then E7: ( c5 `1 in Hom c3,c4 & c5 `2 in Hom c2,c3 ) by MCART_1:10;
reconsider c6 = c5 `1 , c7 = c5 `2 as Morphism of c1 by E6, MCART_1:10;
E8: c5 = [c6,c7] by E6, MCART_1:23;
dom c6 = c3 by E7, CAT_1:18
.= cod c7 by E7, CAT_1:18 ;
hence c5 in dom the Comp of c1 by E8, CAT_1:40;
end;

theorem Th12: :: ALTCAT_2:12
for b1 being Category
for b2, b3, b4 being Object of b1 holds the Comp of b1 .: [:(Hom b3,b4),(Hom b2,b3):] c= Hom b2,b4
proof
let c1 be Category;
let c2, c3, c4 be Object of c1;
let c5 be set ; :: according to TARSKI:def 3
assume c5 in the Comp of c1 .: [:(Hom c3,c4),(Hom c2,c3):] ;
then consider c6 being set such that
E7: c6 in dom the Comp of c1 and
E8: c6 in [:(Hom c3,c4),(Hom c2,c3):] and
E9: c5 = the Comp of c1 . c6 by FUNCT_1:def 12;
E10: ( c6 `1 in Hom c3,c4 & c6 `2 in Hom c2,c3 ) by E8, MCART_1:10;
reconsider c7 = c6 `1 , c8 = c6 `2 as Morphism of c1 by E8, MCART_1:10;
E11: c6 = [c7,c8] by E8, MCART_1:23;
( c7 is Morphism of c3,c4 & c8 is Morphism of c2,c3 ) by E10, CAT_1:def 7;
then c7 * c8 in Hom c2,c4 by E10, CAT_1:51;
hence c5 in Hom c2,c4 by E7, E9, E11, CAT_1:def 4;
end;

definition
let c1 be CatStr ;
func the_hom_sets_of c1 -> ManySortedSet of [:the Objects of a1,the Objects of a1:] means :Def3: :: ALTCAT_2:def 3
for b1, b2 being Object of a1 holds a2 . b1,b2 = Hom b1,b2;
existence
ex b1 being ManySortedSet of [:the Objects of c1,the Objects of c1:] st
for b2, b3 being Object of c1 holds b1 . b2,b3 = Hom b2,b3
proof
deffunc H1( Object of c1, Object of c1) -> Element of bool the Morphisms of c1 = Hom a1,a2;
thus ex b1 being ManySortedSet of [:the Objects of c1,the Objects of c1:] st
for b2, b3 being Object of c1 holds b1 . b2,b3 = H1(b2,b3) from ALTCAT_1:sch 2();
end;
uniqueness
for b1, b2 being ManySortedSet of [:the Objects of c1,the Objects of c1:] holds
( ( for b3, b4 being Object of c1 holds b1 . b3,b4 = Hom b3,b4 ) & ( for b3, b4 being Object of c1 holds b2 . b3,b4 = Hom b3,b4 ) implies b1 = b2 )
proof
let c2, c3 be ManySortedSet of [:the Objects of c1,the Objects of c1:];
assume that
E7: for b1, b2 being Object of c1 holds c2 . b1,b2 = Hom b1,b2 and
E8: for b1, b2 being Object of c1 holds c3 . b1,b2 = Hom b1,b2 ;
now
let c4, c5 be Object of c1;
thus c2 . c4,c5 = Hom c4,c5 by E7
.= c3 . c4,c5 by E8 ;
end;
hence c2 = c3 by ALTCAT_1:9;
end;
end;

:: deftheorem Def3 defines the_hom_sets_of ALTCAT_2:def 3 :
for b1 being CatStr
for b2 being ManySortedSet of [:the Objects of b1,the Objects of b1:] holds
( b2 = the_hom_sets_of b1 iff for b3, b4 being Object of b1 holds b2 . b3,b4 = Hom b3,b4 );

theorem Th13: :: ALTCAT_2:13
for b1 being Category
for b2 being Object of b1 holds id b2 in (the_hom_sets_of b1) . b2,b2
proof
let c1 be Category;
let c2 be Object of c1;
id c2 in Hom c2,c2 by CAT_1:55;
hence id c2 in (the_hom_sets_of c1) . c2,c2 by Def3;
end;

definition
let c1 be Category;
func the_comps_of c1 -> BinComp of (the_hom_sets_of a1) means :Def4: :: ALTCAT_2:def 4
for b1, b2, b3 being Object of a1 holds a2 . b1,b2,b3 = the Comp of a1 | [:((the_hom_sets_of a1) . b2,b3),((the_hom_sets_of a1) . b1,b2):];
existence
ex b1 being BinComp of (the_hom_sets_of c1) st
for b2, b3, b4 being Object of c1 holds b1 . b2,b3,b4 = the Comp of c1 | [:((the_hom_sets_of c1) . b3,b4),((the_hom_sets_of c1) . b2,b3):]
proof
set c2 = [:the Objects of c1,the Objects of c1,the Objects of c1:];
set c3 = the_hom_sets_of c1;
deffunc H1( set ) -> set = the Comp of c1 | [:((the_hom_sets_of c1) . ((a1 `1 ) `2 ),(a1 `2 )),((the_hom_sets_of c1) . ((a1 `1 ) `1 ),((a1 `1 ) `2 )):];
consider c4 being Function such that
E9: dom c4 = [:the Objects of c1,the Objects of c1,the Objects of c1:] and
E10: for b1 being set holds
( b1 in [:the Objects of c1,the Objects of c1,the Objects of c1:] implies c4 . b1 = H1(b1) ) from FUNCT_1:sch 3();
 reconsider c5 = c4 as ManySortedSet of [:the Objects of c1,the Objects of c1,the Objects of c1:] by E9, PBOOLE:def 3;
now
let c6 be set ;
assume c6 in dom c5 ;
then c5 . c6 = the Comp of c1 | [:((the_hom_sets_of c1) . ((c6 `1 ) `2 ),(c6 `2 )),((the_hom_sets_of c1) . ((c6 `1 ) `1 ),((c6 `1 ) `2 )):] by E9, E10;
hence c5 . c6 is Function ;
end;
then reconsider c6 = c5 as ManySortedFunction of [:the Objects of c1,the Objects of c1,the Objects of c1:] by FUNCOP_1:def 6;
now
let c7 be set ;
assume E11: c7 in [:the Objects of c1,the Objects of c1,the Objects of c1:] ;
reconsider c8 = c6