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 [:(),():] such that
A1: for i, j being Element of MSS_set A holds M . (i,j) = H1(i,j) from 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 [:(),(),():] 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 [:(),(),():] 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 [:(),(),():] ; :: 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 ;
A6: {|M|} . ijk = {|M|} . (x1,x2,x3) by ;
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 ;
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 ;
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 ;
then ( {|M|} . (x1,x2,x3) = M . (x1,x3) & y in MSS_morph (x1,x3) ) by ;
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 ;
A14: x `2 = [F1,F2] by A12;
then F1 = f1 by ;
hence y = [(G1 * F1),(G2 * F2)] by ; :: thesis: verum
end;
consider F being ManySortedFunction of {|M,M|},{|M|} such that
A15: for ijk being object st ijk in [:(),(),():] 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 take EX = AltCatStr(# (),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 [:(),(),():] 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 ;
( {|M,M|} . (i,j,k) = {|M,M|} . [i,j,k] & {|M,M|} . (i,j,k) = [:(M . (j,k)),(M . (i,j)):] ) by ;
then [[g1,g2],[f1,f2]] in {|M,M|} . [i,j,k] by ;
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 ;
( I = i & J = j ) by ;
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