:: ALTCAT_2 semantic presentation

theorem :: 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 ; :: uses FUNCOP_1:def 6
assume c2 in dom ([0] c1) ;
thus ([0] c1) . c2 is Function by PBOOLE:5;
end;
end;

theorem :: ALTCAT_2:2
for b1, b2 being Function holds ~ (b1 * b2) = (~ b1) * b2
proof
let c1, c2 be Function;
E1: now
let c3 be set ;
hereby
assume E2: c3 in dom ((~ c1) * c2) ;
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 (c1 * c2) by E4, FUNCT_1:21;
end;given c4, c5 being set such that E2: c3 = [c5,c4]
and E3: [c4,c5] in dom (c1 * c2) ;
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 ((~ c1) * c2) by E5, FUNCT_1:21;
end;
now
let c3, c4 be set ;
assume E2: [c3,c4] in dom (c1 * c2) ;
then [c3,c4] in dom c1 by FUNCT_1:21;
then E3: [c4,c3] in dom (~ c1) by FUNCT_4:43;
hence ((~ c1) * c2) . [c4,c3] = c2 . ((~ c1) . [c4,c3]) by FUNCT_1:23
.= c2 . (c1 . [c3,c4]) by E3, FUNCT_4:44
.= (c1 * c2) . [c3,c4] by E2, FUNCT_1:22 ;

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

theorem :: ALTCAT_2:3
for b1, b2, b3 being Function holds ~ ([:b2,b3:] * b1) = [:b3,b2:] * (~ b1)
proof
let c1, c2, c3 be Function;
E1: now
let c4 be set ;
hereby
assume E2: c4 in dom ([:c3,c2:] * (~ c1)) ;
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 ([:c2,c3:] * c1) by E6, FUNCT_1:21;
end;given c5, c6 being set such that E2: c4 = [c6,c5]
and E3: [c5,c6] in dom ([:c2,c3:] * c1) ;
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 ([:c3,c2:] * (~ c1)) by E6, FUNCT_1:21;
end;
now
let c4, c5 be set ;
assume E2: [c4,c5] in dom ([:c2,c3:] * c1) ;
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 ([:c3,c2:] * (~ c1)) . [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
.= ([:c2,c3:] * c1) . [c4,c5] by E2, FUNCT_1:22 ;

end;
hence ~ ([:c2,c3:] * c1) = [:c3,c2:] * (~ c1) 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 ; :: uses 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 :: 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 ; :: uses 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 = c10 * c9 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 ~ a2 -> ManySortedSet of [:a1,a1:];
coherence
~ c2 is ManySortedSet of [:c1,c1:]
proof
thus dom (~ c2) = [:c1,c1:] by PBOOLE:def 3; :: uses PBOOLE:def 3
end;
end;

theorem :: 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 ; :: uses 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 ~ a4 -> 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 ; :: uses 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 :: 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) . [c5,c4] by BINOP_1:def 1
.= c3 . [c4,c5] by E1, FUNCT_4:def 2
.= c3 . c4,c5 by BINOP_1:def 1 ;
end;

definition
let c1 be set ;
let c2, c3 be ManySortedFunction of c1;
redefine func ** as a3 ** a2 -> 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 a1 cc= a2 means :E1: :: 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 E1 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 a3 cc= a4 means :E2: :: 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 E1;
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; :: uses 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 E2 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 :: ALTCAT_2:7
canceled;

theorem E3: :: 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, E2;
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, E2;
hence c3 . c6 = c5 . c6 by XBOOLE_0:def 10;
end;
hence c3 = c4 by PBOOLE:3;
end;

theorem E4: :: 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, E2;
c2 c= c3 by E6, E2;
hence c1 c= c3 by E7, XBOOLE_1:1; :: uses 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, E2;
hence c4 . c7 c= c6 . c7 by XBOOLE_1:1;
end;

theorem :: 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 ; :: uses PBOOLE:def 5
thus not ( c4 in c1 & not c2 . c4 c= c3 . c4 ) by E5, E2;
end;
assume E5: c2 c= c3 ;
thus c1 c= c1 ; :: uses 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
provided
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 ; :: uses 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 ; :: uses 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 E5: :: 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 ; :: uses 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 E6: :: 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 ; :: uses 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 a1 -> ManySortedSet of [:the Objects of a1,the Objects of a1:] means :E7: :: 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 E7 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 E8: :: 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 E7;
end;

definition
let c1 be Category;
func the_comps_of a1 -> BinComp of (the_hom_sets_of a1) means :E9: :: 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 . c7 as Function ;
consider c9, c10, c11 being Object of c1 such that
E12: c7 = [c9,c10,c11] by E11, DOMAIN_1:15;
reconsider c12 = c7 as Element of [:the Objects of c1,the Objects of c1,the Objects of c1:] by E11;
E13: ([c9,c10,c11] `1 ) `1 = c12 `1 by E12, MCART_1:50
.= c9 by E12, MCART_1:47 ;
E14: ([c9,c10,c11] `1 ) `2 = c12 `2 by E12, MCART_1:50
.= c10 by E12, MCART_1:47 ;
E15: [c9,c10,c11] `2 = c12 `3 by E12, MCART_1:50
.= c11 by E12, MCART_1:47 ;
E16: ( (the_hom_sets_of c1) . c9,c10 = Hom c9,c10 & (the_hom_sets_of c1) . c10,c11 = Hom c10,c11 ) by E7;
E17: c8 = the Comp of c1 | [:((the_hom_sets_of c1) . c10,c11),((the_hom_sets_of c1) . c9,c10):] by E10, E11, E12, E13, E14, E15;
E18: {|(the_hom_sets_of c1)|} . c7 = {|(the_hom_sets_of c1)|} . c9,c10,c11 by E12, MULTOP_1:def 1
.= (the_hom_sets_of c1) . c9,c11 by ALTCAT_1:def 5
.= Hom c9,c11 by E7 ;
E19: {|(the_hom_sets_of c1),(the_hom_sets_of c1)|} . c7 = {|(the_hom_sets_of c1),(the_hom_sets_of c1)|} . c9,c10,c11 by E12, MULTOP_1:def 1
.= [:(Hom c10,c11),(Hom c9,c10):] by E16, ALTCAT_1:def 6 ;
E20: now
assume {|(the_hom_sets_of c1)|} . c7 = {} ;
then ( Hom c9,c10 = {} or Hom c10,c11 = {} ) by E18, CAT_1:52;
hence {|(the_hom_sets_of c1),(the_hom_sets_of c1)|} . c7 = {} by E19, ZFMISC_1:113;
end;
[:(Hom c10,c11),(Hom c9,c10):] c= dom the Comp of c1 by E5;
then E21: dom c8 = {|(the_hom_sets_of c1),(the_hom_sets_of c1)|} . c7 by E16, E17, E19, RELAT_1:91;
the Comp of c1 .: [:(Hom c10,c11),(Hom c9,c10):] c= Hom c9,c11 by E6;
then rng c8 c= {|(the_hom_sets_of c1)|} . c7 by E16, E17, E18, RELAT_1:148;
hence c6 . c7 is Function of {|(the_hom_sets_of c1),(the_hom_sets_of c1)|} . c7,{|(the_hom_sets_of c1)|} . c7 by E20, E21, FUNCT_2:def 1, RELSET_1:11;
end;
then reconsider c7 = c6 as BinComp of (the_hom_sets_of c1) by PBOOLE:def 18;
take c7 ;
let c8, c9, c10 be Object of c1;
E11: [c8,c9,c10] in [:the Objects of c1,the Objects of c1,the Objects of c1:] by DOMAIN_1:15;
reconsider c11 = [c8,c9,c10] as Element of [:the Objects of c1,the Objects of c1,the Objects of c1:] by DOMAIN_1:15;
E12: ([c8,c9,c10] `1 ) `1 = c11 `1 by