set c = MSS_set A;

deffunc H_{1}( 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) = H_{1}(i,j)
from ALTCAT_1:sch 2();

defpred S_{1}[ 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 & S_{1}[y,x,ijk] )

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

S_{1}[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)]

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

deffunc H

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) = H

defpred S

( $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 & S

proof

consider F being ManySortedFunction of {|M,M|},{|M|} such that
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 & S_{1}[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 & S_{1}[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 & S_{1}[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 & S_{1}[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 & S_{1}[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: S_{1}[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;ex y being object st

( y in {|M|} . ijk & S

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 & S

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 & S

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 & S

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 & S

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: S

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

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

S

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

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
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

S_{1}[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;( 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

S

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

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