set c = MSS_set A;
deffunc H1( Element of MSS_set A, Element of MSS_set A) -> set = MSS_morph ($1,$2);
consider M being ManySortedSet of [:(MSS_set A),(MSS_set A):] such that
A1: for i, j being Element of MSS_set A holds M . (i,j) = H1(i,j) from ALTCAT_1:sch 2();
 defpred S1[ object , object , object ] means ex i, j, k being Element of MSS_set A st
( $3 = [i,j,k] & ( for f1, f2, g1, g2 being Function st [f1,f2] in M . (i,j) & [g1,g2] in M . (j,k) & $2 = [[g1,g2],[f1,f2]] holds
$1 = [(g1 * f1),(g2 * f2)] ) );
A2: for ijk being object st ijk in [:(MSS_set A),(MSS_set A),(MSS_set A):] holds
for x being object st x in {|M,M|} . ijk holds
ex y being object st
( y in {|M|} . ijk & S1[y,x,ijk] )
proof
let ijk be object ; :: thesis: ( ijk in [:(MSS_set A),(MSS_set A),(MSS_set A):] implies for x being object st x in {|M,M|} . ijk holds
ex y being object st
( y in {|M|} . ijk & S1[y,x,ijk] ) )
assume ijk in [:(MSS_set A),(MSS_set A),(MSS_set A):] ; :: thesis: for x being object st x in {|M,M|} . ijk holds
ex y being object st
( y in {|M|} . ijk & S1[y,x,ijk] )
then consider x1, x2, x3 being object such that
A3: ( x1 in MSS_set A & x2 in MSS_set A & x3 in MSS_set A ) and
A4: ijk = [x1,x2,x3] by MCART_1:68;
reconsider x1 = x1, x2 = x2, x3 = x3 as Element of MSS_set A by A3;
let x be object ; :: thesis: ( x in {|M,M|} . ijk implies ex y being object st
( y in {|M|} . ijk & S1[y,x,ijk] ) )
A5: ( {|M,M|} . (x1,x2,x3) = {|M,M|} . [x1,x2,x3] & {|M,M|} . (x1,x2,x3) = [:(M . (x2,x3)),(M . (x1,x2)):] ) by ALTCAT_1:def 4, MULTOP_1:def 1;
A6: {|M|} . ijk = {|M|} . (x1,x2,x3) by A4, MULTOP_1:def 1;
assume A7: x in {|M,M|} . ijk ; :: thesis: ex y being object st
( y in {|M|} . ijk & S1[y,x,ijk] )
then x `1 in M . (x2,x3) by A4, A5, MCART_1:10;
then x `1 in MSS_morph (x2,x3) by A1;
then consider g1, g2 being Function such that
A8: x `1 = [g1,g2] and
A9: g1,g2 form_morphism_between x2,x3 by MSALIMIT:def 10;
x `2 in M . (x1,x2) by A4, A7, A5, MCART_1:10;
then x `2 in MSS_morph (x1,x2) by A1;
then consider f1, f2 being Function such that
A10: x `2 = [f1,f2] and
A11: f1,f2 form_morphism_between x1,x2 by MSALIMIT:def 10;
take y = [(g1 * f1),(g2 * f2)]; :: thesis: ( y in {|M|} . ijk & S1[y,x,ijk] )
g1 * f1,g2 * f2 form_morphism_between x1,x3 by A11, A9, PUA2MSS1:29;
then ( {|M|} . (x1,x2,x3) = M . (x1,x3) & y in MSS_morph (x1,x3) ) by ALTCAT_1:def 3, MSALIMIT:def 10;
hence y in {|M|} . ijk by A1, A6; :: thesis: S1[y,x,ijk]
take x1 ; :: thesis: ex j, k being Element of MSS_set A st
( ijk = [x1,j,k] & ( for f1, f2, g1, g2 being Function st [f1,f2] in M . (x1,j) & [g1,g2] in M . (j,k) & x = [[g1,g2],[f1,f2]] holds
y = [(g1 * f1),(g2 * f2)] ) )
take x2 ; :: thesis: ex k being Element of MSS_set A st
( ijk = [x1,x2,k] & ( for f1, f2, g1, g2 being Function st [f1,f2] in M . (x1,x2) & [g1,g2] in M . (x2,k) & x = [[g1,g2],[f1,f2]] holds
y = [(g1 * f1),(g2 * f2)] ) )
take x3 ; :: thesis: ( ijk = [x1,x2,x3] & ( for f1, f2, g1, g2 being Function st [f1,f2] in M . (x1,x2) & [g1,g2] in M . (x2,x3) & x = [[g1,g2],[f1,f2]] holds
y = [(g1 * f1),(g2 * f2)] ) )
thus ijk = [x1,x2,x3] by A4; :: thesis: for f1, f2, g1, g2 being Function st [f1,f2] in M . (x1,x2) & [g1,g2] in M . (x2,x3) & x = [[g1,g2],[f1,f2]] holds
y = [(g1 * f1),(g2 * f2)]
let F1, F2, G1, G2 be Function; :: thesis: ( [F1,F2] in M . (x1,x2) & [G1,G2] in M . (x2,x3) & x = [[G1,G2],[F1,F2]] implies y = [(G1 * F1),(G2 * F2)] )
assume that
[F1,F2] in M . (x1,x2) and
[G1,G2] in M . (x2,x3) and
A12: x = [[G1,G2],[F1,F2]] ; :: thesis: y = [(G1 * F1),(G2 * F2)]
x `1 = [G1,G2] by A12;
then A13: ( G1 = g1 & G2 = g2 ) by A8, XTUPLE_0:1;
A14: x `2 = [F1,F2] by A12;
then F1 = f1 by A10, XTUPLE_0:1;
hence y = [(G1 * F1),(G2 * F2)] by A10, A14, A13, XTUPLE_0:1; :: thesis: verum
end;
consider F being ManySortedFunction of {|M,M|},{|M|} such that
A15: for ijk being object st ijk in [:(MSS_set A),(MSS_set A),(MSS_set A):] holds
ex f being Function of ({|M,M|} . ijk),({|M|} . ijk) st
( f = F . ijk & ( for x being object st x in {|M,M|} . ijk holds
S1[f . x,x,ijk] ) ) from MSSUBFAM:sch 1(A2);
 take EX = AltCatStr(# (MSS_set A),M,F #); :: thesis: ( the carrier of EX = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of EX . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being Object of EX st i in MSS_set A & j in MSS_set A & k in MSS_set A holds
for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of EX . (i,j) & [g1,g2] in the Arrows of EX . (j,k) holds
( the Comp of EX . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) )
reconsider EX = EX as non empty AltCatStr ;
for i, j, k being Object of EX st i in MSS_set A & j in MSS_set A & k in MSS_set A holds
for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of EX . (i,j) & [g1,g2] in the Arrows of EX . (j,k) holds
( the Comp of EX . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)]
proof
let i, j, k be Object of EX; :: thesis: ( i in MSS_set A & j in MSS_set A & k in MSS_set A implies for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of EX . (i,j) & [g1,g2] in the Arrows of EX . (j,k) holds
( the Comp of EX . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] )
assume that
i in MSS_set A and
j in MSS_set A and
k in MSS_set A ; :: thesis: for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of EX . (i,j) & [g1,g2] in the Arrows of EX . (j,k) holds
( the Comp of EX . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)]
let f1, f2, g1, g2 be Function; :: thesis: ( [f1,f2] in the Arrows of EX . (i,j) & [g1,g2] in the Arrows of EX . (j,k) implies ( the Comp of EX . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] )
assume A16: ( [f1,f2] in the Arrows of EX . (i,j) & [g1,g2] in the Arrows of EX . (j,k) ) ; :: thesis: ( the Comp of EX . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)]
set x = [[g1,g2],[f1,f2]];
set ijk = [i,j,k];
[i,j,k] in [:(MSS_set A),(MSS_set A),(MSS_set A):] by MCART_1:69;
then consider f being Function of ({|M,M|} . [i,j,k]),({|M|} . [i,j,k]) such that
A17: f = F . [i,j,k] and
A18: for x being object st x in {|M,M|} . [i,j,k] holds
S1[f . x,x,[i,j,k]] by A15;
A19: f = the Comp of EX . (i,j,k) by A17, MULTOP_1:def 1;
( {|M,M|} . (i,j,k) = {|M,M|} . [i,j,k] & {|M,M|} . (i,j,k) = [:(M . (j,k)),(M . (i,j)):] ) by ALTCAT_1:def 4, MULTOP_1:def 1;
then [[g1,g2],[f1,f2]] in {|M,M|} . [i,j,k] by A16, ZFMISC_1:87;
then consider I, J, K being Element of MSS_set A such that
A20: [i,j,k] = [I,J,K] and
A21: for f1, f2, g1, g2 being Function st [f1,f2] in M . (I,J) & [g1,g2] in M . (J,K) & [[g1,g2],[f1,f2]] = [[g1,g2],[f1,f2]] holds
f . [[g1,g2],[f1,f2]] = [(g1 * f1),(g2 * f2)] by A18;
A22: K = k by A20, XTUPLE_0:3;
( I = i & J = j ) by A20, XTUPLE_0:3;
hence ( the Comp of EX . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] by A16, A21, A22, A19; :: thesis: verum
end;
hence ( the carrier of EX = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of EX . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being Object of EX st i in MSS_set A & j in MSS_set A & k in MSS_set A holds
for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of EX . (i,j) & [g1,g2] in the Arrows of EX . (j,k) holds
( the Comp of EX . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) ) by A1; :: thesis: verum