:: MSINST_1 semantic presentation
begin
definition
let A be non empty set ;
func MSSCat A -> non empty strict AltCatStr means :Def1: :: MSINST_1:def 1
( the carrier of it = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of it . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being object of it 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 it . (i,j) & [g1,g2] in the Arrows of it . (j,k) holds
( the Comp of it . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) );
existence
ex b1 being non empty strict AltCatStr st
( the carrier of b1 = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of b1 . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being object of b1 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 b1 . (i,j) & [g1,g2] in the Arrows of b1 . (j,k) holds
( the Comp of b1 . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) )
proof
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[ set , set , set ] 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 set st ijk in [:(MSS_set A),(MSS_set A),(MSS_set A):] holds
for x being set st x in {|M,M|} . ijk holds
ex y being set st
( y in {|M|} . ijk & S1[y,x,ijk] )
proof
let ijk be set ; ::_thesis: ( ijk in [:(MSS_set A),(MSS_set A),(MSS_set A):] implies for x being set st x in {|M,M|} . ijk holds
ex y being set 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 set st x in {|M,M|} . ijk holds
ex y being set st
( y in {|M|} . ijk & S1[y,x,ijk] )
then consider x1, x2, x3 being set 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 set ; ::_thesis: ( x in {|M,M|} . ijk implies ex y being set 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 set 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, MCART_1:7;
then A13: ( G1 = g1 & G2 = g2 ) by A8, XTUPLE_0:1;
A14: x `2 = [F1,F2] by A12, MCART_1:7;
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 set 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 set 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 set 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
end;
uniqueness
for b1, b2 being non empty strict AltCatStr st the carrier of b1 = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of b1 . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being object of b1 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 b1 . (i,j) & [g1,g2] in the Arrows of b1 . (j,k) holds
( the Comp of b1 . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) & the carrier of b2 = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of b2 . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being object of b2 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 b2 . (i,j) & [g1,g2] in the Arrows of b2 . (j,k) holds
( the Comp of b2 . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) holds
b1 = b2
proof
set c = MSS_set A;
let A1, A2 be non empty strict AltCatStr ; ::_thesis: ( the carrier of A1 = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of A1 . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being object of A1 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 A1 . (i,j) & [g1,g2] in the Arrows of A1 . (j,k) holds
( the Comp of A1 . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) & the carrier of A2 = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of A2 . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being object of A2 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 A2 . (i,j) & [g1,g2] in the Arrows of A2 . (j,k) holds
( the Comp of A2 . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) implies A1 = A2 )
assume that
A23: the carrier of A1 = MSS_set A and
A24: for i, j being Element of MSS_set A holds the Arrows of A1 . (i,j) = MSS_morph (i,j) and
A25: for i, j, k being object of A1 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 A1 . (i,j) & [g1,g2] in the Arrows of A1 . (j,k) holds
( the Comp of A1 . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] and
A26: the carrier of A2 = MSS_set A and
A27: for i, j being Element of MSS_set A holds the Arrows of A2 . (i,j) = MSS_morph (i,j) and
A28: for i, j, k being object of A2 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 A2 . (i,j) & [g1,g2] in the Arrows of A2 . (j,k) holds
( the Comp of A2 . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ; ::_thesis: A1 = A2
reconsider AA2 = the Arrows of A2 as ManySortedSet of [:(MSS_set A),(MSS_set A):] by A26;
reconsider AA1 = the Arrows of A1 as ManySortedSet of [:(MSS_set A),(MSS_set A):] by A23;
reconsider CC1 = the Comp of A1, CC2 = the Comp of A2 as ManySortedSet of [:(MSS_set A),(MSS_set A),(MSS_set A):] by A23, A26;
A29: now__::_thesis:_for_i,_j_being_Element_of_MSS_set_A_holds_AA1_._(i,j)_=_AA2_._(i,j)
let i, j be Element of MSS_set A; ::_thesis: AA1 . (i,j) = AA2 . (i,j)
thus AA1 . (i,j) = MSS_morph (i,j) by A24
.= AA2 . (i,j) by A27 ; ::_thesis: verum
end;
then A30: AA1 = AA2 by ALTCAT_1:7;
now__::_thesis:_for_i,_j,_k_being_set_st_i_in_MSS_set_A_&_j_in_MSS_set_A_&_k_in_MSS_set_A_holds_
CC1_._(i,j,k)_=_CC2_._(i,j,k)
let i, j, k be set ; ::_thesis: ( i in MSS_set A & j in MSS_set A & k in MSS_set A implies CC1 . (i,j,k) = CC2 . (i,j,k) )
set ijk = [i,j,k];
A31: CC1 . (i,j,k) = CC1 . [i,j,k] by MULTOP_1:def_1;
assume A32: ( i in MSS_set A & j in MSS_set A & k in MSS_set A ) ; ::_thesis: CC1 . (i,j,k) = CC2 . (i,j,k)
then reconsider i9 = i, j9 = j, k9 = k as Element of MSS_set A ;
reconsider I9 = i, J9 = j, K9 = k as Element of A2 by A26, A32;
reconsider I = i, J = j, K = k as Element of A1 by A23, A32;
A33: [i,j,k] in [:(MSS_set A),(MSS_set A),(MSS_set A):] by A32, MCART_1:69;
A34: CC2 . (i,j,k) = CC2 . [i,j,k] by MULTOP_1:def_1;
thus CC1 . (i,j,k) = CC2 . (i,j,k) ::_thesis: verum
proof
reconsider Cj = CC2 . [i,j,k] as Function of ({|AA2,AA2|} . [i,j,k]),({|AA2|} . [i,j,k]) by A26, A33, PBOOLE:def_15;
reconsider Ci = CC1 . [i,j,k] as Function of ({|AA1,AA1|} . [i,j,k]),({|AA1|} . [i,j,k]) by A23, A33, PBOOLE:def_15;
percases ( {|AA1|} . [i,j,k] <> {} or {|AA1|} . [i,j,k] = {} ) ;
supposeA35: {|AA1|} . [i,j,k] <> {} ; ::_thesis: CC1 . (i,j,k) = CC2 . (i,j,k)
A36: for x being set st x in {|AA1,AA1|} . [i,j,k] holds
Ci . x = Cj . x
proof
let x be set ; ::_thesis: ( x in {|AA1,AA1|} . [i,j,k] implies Ci . x = Cj . x )
assume A37: x in {|AA1,AA1|} . [i,j,k] ; ::_thesis: Ci . x = Cj . x
then x in {|AA1,AA1|} . (i,j,k) by MULTOP_1:def_1;
then A38: x in [:(AA1 . (j,k)),(AA1 . (i,j)):] by A32, ALTCAT_1:def_4;
then A39: x `1 in AA1 . (j,k) by MCART_1:10;
then x `1 in MSS_morph (j9,k9) by A24;
then consider g1, g2 being Function such that
A40: x `1 = [g1,g2] and
g1,g2 form_morphism_between j9,k9 by MSALIMIT:def_10;
x in {|AA2,AA2|} . (i,j,k) by A30, A37, MULTOP_1:def_1;
then x in [:(AA2 . (j,k)),(AA2 . (i,j)):] by A32, ALTCAT_1:def_4;
then A41: ( x `1 in AA2 . (j,k) & x `2 in AA2 . (i,j) ) by MCART_1:10;
A42: x `2 in AA1 . (i,j) by A38, MCART_1:10;
then x `2 in MSS_morph (i9,j9) by A24;
then consider f1, f2 being Function such that
A43: x `2 = [f1,f2] and
f1,f2 form_morphism_between i9,j9 by MSALIMIT:def_10;
A44: x = [[g1,g2],[f1,f2]] by A38, A40, A43, MCART_1:21;
then Ci . x = ( the Comp of A1 . (I,J,K)) . ([g1,g2],[f1,f2]) by MULTOP_1:def_1
.= [(g1 * f1),(g2 * f2)] by A23, A25, A39, A42, A40, A43
.= ( the Comp of A2 . (I9,J9,K9)) . ([g1,g2],[f1,f2]) by A26, A28, A41, A40, A43
.= Cj . x by A44, MULTOP_1:def_1 ;
hence Ci . x = Cj . x ; ::_thesis: verum
end;
{|AA2|} . [i,j,k] <> {} by A29, A35, ALTCAT_1:7;
then A45: dom Cj = {|AA2,AA2|} . [i,j,k] by FUNCT_2:def_1;
dom Ci = {|AA1,AA1|} . [i,j,k] by A35, FUNCT_2:def_1;
hence CC1 . (i,j,k) = CC2 . (i,j,k) by A30, A31, A34, A45, A36, FUNCT_1:2; ::_thesis: verum
end;
suppose {|AA1|} . [i,j,k] = {} ; ::_thesis: CC1 . (i,j,k) = CC2 . (i,j,k)
then ( Ci = {} & Cj = {} ) by A30;
hence CC1 . (i,j,k) = CC2 . (i,j,k) by A31, MULTOP_1:def_1; ::_thesis: verum
end;
end;
end;
end;
hence A1 = A2 by A23, A26, A30, ALTCAT_1:8; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines MSSCat MSINST_1:def_1_:_
for A being non empty set
for b2 being non empty strict AltCatStr holds
( b2 = MSSCat A iff ( the carrier of b2 = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of b2 . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being object of b2 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 b2 . (i,j) & [g1,g2] in the Arrows of b2 . (j,k) holds
( the Comp of b2 . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) ) );
registration
let A be non empty set ;
cluster MSSCat A -> non empty transitive strict associative with_units ;
coherence
( MSSCat A is transitive & MSSCat A is associative & MSSCat A is with_units )
proof
set M = MSSCat A;
set G = MSSCat A;
thus MSSCat A is transitive ::_thesis: ( MSSCat A is associative & MSSCat A is with_units )
proof
let o1, o2, o3 be object of (MSSCat A); :: according to ALTCAT_1:def_2 ::_thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or not <^o1,o3^> = {} )
reconsider o19 = o1, o29 = o2, o39 = o3 as Element of MSS_set A by Def1;
assume that
A1: <^o1,o2^> <> {} and
A2: <^o2,o3^> <> {} ; ::_thesis: not <^o1,o3^> = {}
set s = the Element of MSS_morph (o29,o39);
MSS_morph (o29,o39) <> {} by A2, Def1;
then consider u, w being Function such that
the Element of MSS_morph (o29,o39) = [u,w] and
A3: u,w form_morphism_between o29,o39 by MSALIMIT:def_10;
set t = the Element of MSS_morph (o19,o29);
MSS_morph (o19,o29) <> {} by A1, Def1;
then consider f, g being Function such that
the Element of MSS_morph (o19,o29) = [f,g] and
A4: f,g form_morphism_between o19,o29 by MSALIMIT:def_10;
u * f,w * g form_morphism_between o19,o39 by A4, A3, PUA2MSS1:29;
then [(u * f),(w * g)] in MSS_morph (o19,o39) by MSALIMIT:def_10;
hence not <^o1,o3^> = {} by Def1; ::_thesis: verum
end;
set G = the Arrows of (MSSCat A);
set C = the Comp of (MSSCat A);
thus the Comp of (MSSCat A) is associative :: according to ALTCAT_1:def_15 ::_thesis: MSSCat A is with_units
proof
let i, j, k, l be Element of (MSSCat A); :: according to ALTCAT_1:def_5 ::_thesis: for b1, b2, b3 being set holds
( not b1 in the Arrows of (MSSCat A) . (i,j) or not b2 in the Arrows of (MSSCat A) . (j,k) or not b3 in the Arrows of (MSSCat A) . (k,l) or ( the Comp of (MSSCat A) . (i,k,l)) . (b3,(( the Comp of (MSSCat A) . (i,j,k)) . (b2,b1))) = ( the Comp of (MSSCat A) . (i,j,l)) . ((( the Comp of (MSSCat A) . (j,k,l)) . (b3,b2)),b1) )
reconsider I = i, J = j, K = k, L = l as object of (MSSCat A) ;
let f, g, h be set ; ::_thesis: ( not f in the Arrows of (MSSCat A) . (i,j) or not g in the Arrows of (MSSCat A) . (j,k) or not h in the Arrows of (MSSCat A) . (k,l) or ( the Comp of (MSSCat A) . (i,k,l)) . (h,(( the Comp of (MSSCat A) . (i,j,k)) . (g,f))) = ( the Comp of (MSSCat A) . (i,j,l)) . ((( the Comp of (MSSCat A) . (j,k,l)) . (h,g)),f) )
reconsider i9 = i, j9 = j, k9 = k, l9 = l as Element of MSS_set A by Def1;
assume that
A5: f in the Arrows of (MSSCat A) . (i,j) and
A6: g in the Arrows of (MSSCat A) . (j,k) and
A7: h in the Arrows of (MSSCat A) . (k,l) ; ::_thesis: ( the Comp of (MSSCat A) . (i,k,l)) . (h,(( the Comp of (MSSCat A) . (i,j,k)) . (g,f))) = ( the Comp of (MSSCat A) . (i,j,l)) . ((( the Comp of (MSSCat A) . (j,k,l)) . (h,g)),f)
g in MSS_morph (j9,k9) by A6, Def1;
then consider g1, g2 being Function such that
A8: g = [g1,g2] and
A9: g1,g2 form_morphism_between j9,k9 by MSALIMIT:def_10;
f in MSS_morph (i9,j9) by A5, Def1;
then consider f1, f2 being Function such that
A10: f = [f1,f2] and
A11: f1,f2 form_morphism_between i9,j9 by MSALIMIT:def_10;
A12: ( the Comp of (MSSCat A) . (i,j,k)) . (g,f) = [(g1 * f1),(g2 * f2)] by A5, A6, A10, A11, A8, A9, Def1;
h in MSS_morph (k9,l9) by A7, Def1;
then consider h1, h2 being Function such that
A13: h = [h1,h2] and
A14: h1,h2 form_morphism_between k9,l9 by MSALIMIT:def_10;
A15: ( the Comp of (MSSCat A) . (j,k,l)) . (h,g) = [(h1 * g1),(h2 * g2)] by A6, A7, A8, A9, A13, A14, Def1;
h1 * g1,h2 * g2 form_morphism_between j9,l9 by A9, A14, PUA2MSS1:29;
then [(h1 * g1),(h2 * g2)] in MSS_morph (j9,l9) by MSALIMIT:def_10;
then A16: [(h1 * g1),(h2 * g2)] in the Arrows of (MSSCat A) . (j,l) by Def1;
A17: ( (h1 * g1) * f1 = h1 * (g1 * f1) & (h2 * g2) * f2 = h2 * (g2 * f2) ) by RELAT_1:36;
J in the carrier of (MSSCat A) ;
then A18: J in MSS_set A by Def1;
L in the carrier of (MSSCat A) ;
then A19: L in MSS_set A by Def1;
g1 * f1,g2 * f2 form_morphism_between i9,k9 by A11, A9, PUA2MSS1:29;
then [(g1 * f1),(g2 * f2)] in MSS_morph (i9,k9) by MSALIMIT:def_10;
then A20: [(g1 * f1),(g2 * f2)] in the Arrows of (MSSCat A) . (i,k) by Def1;
I in the carrier of (MSSCat A) ;
then A21: I in MSS_set A by Def1;
K in the carrier of (MSSCat A) ;
then K in MSS_set A by Def1;
then ( the Comp of (MSSCat A) . (i,k,l)) . (h,[(g1 * f1),(g2 * f2)]) = [(h1 * (g1 * f1)),(h2 * (g2 * f2))] by A21, A19, A7, A13, A20, Def1;
hence ( the Comp of (MSSCat A) . (i,k,l)) . (h,(( the Comp of (MSSCat A) . (i,j,k)) . (g,f))) = ( the Comp of (MSSCat A) . (i,j,l)) . ((( the Comp of (MSSCat A) . (j,k,l)) . (h,g)),f) by A21, A18, A19, A5, A10, A12, A15, A16, A17, Def1; ::_thesis: verum
end;
thus the Comp of (MSSCat A) is with_left_units :: according to ALTCAT_1:def_16 ::_thesis: the Comp of (MSSCat A) is with_right_units
proof
let j be Element of (MSSCat A); :: according to ALTCAT_1:def_7 ::_thesis: ex b1 being set st
( b1 in the Arrows of (MSSCat A) . (j,j) & ( for b2 being Element of the carrier of (MSSCat A)
for b3 being set holds
( not b3 in the Arrows of (MSSCat A) . (b2,j) or ( the Comp of (MSSCat A) . (b2,j,j)) . (b1,b3) = b3 ) ) )
reconsider j9 = j as Element of MSS_set A by Def1;
set e1 = id the carrier of j9;
set e2 = id the carrier' of j9;
take e = [(id the carrier of j9),(id the carrier' of j9)]; ::_thesis: ( e in the Arrows of (MSSCat A) . (j,j) & ( for b1 being Element of the carrier of (MSSCat A)
for b2 being set holds
( not b2 in the Arrows of (MSSCat A) . (b1,j) or ( the Comp of (MSSCat A) . (b1,j,j)) . (e,b2) = b2 ) ) )
( id the carrier of j9, id the carrier' of j9 form_morphism_between j9,j9 & the Arrows of (MSSCat A) . (j,j) = MSS_morph (j9,j9) ) by Def1, PUA2MSS1:28;
hence A22: e in the Arrows of (MSSCat A) . (j,j) by MSALIMIT:def_10; ::_thesis: for b1 being Element of the carrier of (MSSCat A)
for b2 being set holds
( not b2 in the Arrows of (MSSCat A) . (b1,j) or ( the Comp of (MSSCat A) . (b1,j,j)) . (e,b2) = b2 )
let i be Element of (MSSCat A); ::_thesis: for b1 being set holds
( not b1 in the Arrows of (MSSCat A) . (i,j) or ( the Comp of (MSSCat A) . (i,j,j)) . (e,b1) = b1 )
reconsider i9 = i as Element of MSS_set A by Def1;
let f be set ; ::_thesis: ( not f in the Arrows of (MSSCat A) . (i,j) or ( the Comp of (MSSCat A) . (i,j,j)) . (e,f) = f )
reconsider I = i, J = j as object of (MSSCat A) ;
assume A23: f in the Arrows of (MSSCat A) . (i,j) ; ::_thesis: ( the Comp of (MSSCat A) . (i,j,j)) . (e,f) = f
then f in MSS_morph (i9,j9) by Def1;
then consider f1, f2 being Function such that
A24: f = [f1,f2] and
A25: f1,f2 form_morphism_between i9,j9 by MSALIMIT:def_10;
A26: rng f2 c= the carrier' of j9 by A25, PUA2MSS1:def_12;
rng f1 c= the carrier of j9 by A25, PUA2MSS1:def_12;
then A27: (id the carrier of j9) * f1 = f1 by RELAT_1:53;
( the Comp of (MSSCat A) . (I,J,J)) . ([(id the carrier of j9),(id the carrier' of j9)],[f1,f2]) = [((id the carrier of j9) * f1),((id the carrier' of j9) * f2)] by A22, A23, A24, A25, Def1;
hence ( the Comp of (MSSCat A) . (i,j,j)) . (e,f) = f by A24, A26, A27, RELAT_1:53; ::_thesis: verum
end;
thus the Comp of (MSSCat A) is with_right_units ::_thesis: verum
proof
let i be Element of (MSSCat A); :: according to ALTCAT_1:def_6 ::_thesis: ex b1 being set st
( b1 in the Arrows of (MSSCat A) . (i,i) & ( for b2 being Element of the carrier of (MSSCat A)
for b3 being set holds
( not b3 in the Arrows of (MSSCat A) . (i,b2) or ( the Comp of (MSSCat A) . (i,i,b2)) . (b3,b1) = b3 ) ) )
reconsider i9 = i as Element of MSS_set A by Def1;
set e1 = id the carrier of i9;
set e2 = id the carrier' of i9;
take e = [(id the carrier of i9),(id the carrier' of i9)]; ::_thesis: ( e in the Arrows of (MSSCat A) . (i,i) & ( for b1 being Element of the carrier of (MSSCat A)
for b2 being set holds
( not b2 in the Arrows of (MSSCat A) . (i,b1) or ( the Comp of (MSSCat A) . (i,i,b1)) . (b2,e) = b2 ) ) )
( id the carrier of i9, id the carrier' of i9 form_morphism_between i9,i9 & the Arrows of (MSSCat A) . (i,i) = MSS_morph (i9,i9) ) by Def1, PUA2MSS1:28;
hence A28: e in the Arrows of (MSSCat A) . (i,i) by MSALIMIT:def_10; ::_thesis: for b1 being Element of the carrier of (MSSCat A)
for b2 being set holds
( not b2 in the Arrows of (MSSCat A) . (i,b1) or ( the Comp of (MSSCat A) . (i,i,b1)) . (b2,e) = b2 )
let j be Element of (MSSCat A); ::_thesis: for b1 being set holds
( not b1 in the Arrows of (MSSCat A) . (i,j) or ( the Comp of (MSSCat A) . (i,i,j)) . (b1,e) = b1 )
reconsider j9 = j as Element of MSS_set A by Def1;
let f be set ; ::_thesis: ( not f in the Arrows of (MSSCat A) . (i,j) or ( the Comp of (MSSCat A) . (i,i,j)) . (f,e) = f )
reconsider I = i, J = j as object of (MSSCat A) ;
assume A29: f in the Arrows of (MSSCat A) . (i,j) ; ::_thesis: ( the Comp of (MSSCat A) . (i,i,j)) . (f,e) = f
then f in MSS_morph (i9,j9) by Def1;
then consider f1, f2 being Function such that
A30: f = [f1,f2] and
A31: f1,f2 form_morphism_between i9,j9 by MSALIMIT:def_10;
A32: dom f2 = the carrier' of i9 by A31, PUA2MSS1:def_12;
dom f1 = the carrier of i9 by A31, PUA2MSS1:def_12;
then A33: f1 * (id the carrier of i9) = f1 by RELAT_1:52;
( the Comp of (MSSCat A) . (I,I,J)) . ([f1,f2],[(id the carrier of i9),(id the carrier' of i9)]) = [(f1 * (id the carrier of i9)),(f2 * (id the carrier' of i9))] by A28, A29, A30, A31, Def1;
hence ( the Comp of (MSSCat A) . (i,i,j)) . (f,e) = f by A30, A32, A33, RELAT_1:52; ::_thesis: verum
end;
end;
end;
theorem :: MSINST_1:1
for A being non empty set
for C being category st C = MSSCat A holds
for o being object of C holds o is non empty non void ManySortedSign
proof
let A be non empty set ; ::_thesis: for C being category st C = MSSCat A holds
for o being object of C holds o is non empty non void ManySortedSign
let C be category; ::_thesis: ( C = MSSCat A implies for o being object of C holds o is non empty non void ManySortedSign )
assume A1: C = MSSCat A ; ::_thesis: for o being object of C holds o is non empty non void ManySortedSign
let o be object of C; ::_thesis: o is non empty non void ManySortedSign
reconsider o = o as Element of MSS_set A by A1, Def1;
o is non empty non void ManySortedSign ;
hence o is non empty non void ManySortedSign ; ::_thesis: verum
end;
registration
let S be non empty non void ManySortedSign ;
cluster strict feasible for MSAlgebra over S;
existence
ex b1 being MSAlgebra over S st
( b1 is strict & b1 is feasible )
proof
set M = the feasible MSAlgebra over S;
take E = MSAlgebra(# the Sorts of the feasible MSAlgebra over S, the Charact of the feasible MSAlgebra over S #); ::_thesis: ( E is strict & E is feasible )
thus E is strict ; ::_thesis: E is feasible
now__::_thesis:_for_o_being_OperSymbol_of_S_st_Args_(o,E)_<>_{}_holds_
Result_(o,E)_<>_{}
let o be OperSymbol of S; ::_thesis: ( Args (o,E) <> {} implies Result (o,E) <> {} )
A1: Args (o, the feasible MSAlgebra over S) = (( the Sorts of E #) * the Arity of S) . o by MSUALG_1:def_4
.= Args (o,E) by MSUALG_1:def_4 ;
Result (o, the feasible MSAlgebra over S) = ( the Sorts of E * the ResultSort of S) . o by MSUALG_1:def_5
.= Result (o,E) by MSUALG_1:def_5 ;
hence ( Args (o,E) <> {} implies Result (o,E) <> {} ) by A1, MSUALG_6:def_1; ::_thesis: verum
end;
hence E is feasible by MSUALG_6:def_1; ::_thesis: verum
end;
end;
definition
let S be non empty non void ManySortedSign ;
let A be non empty set ;
func MSAlg_set (S,A) -> set means :Def2: :: MSINST_1:def 2
for x being set holds
( x in it iff ex M being strict feasible MSAlgebra over S st
( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ex M being strict feasible MSAlgebra over S st
( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) )
proof
defpred S1[ set , set ] means ex M being strict feasible MSAlgebra over S st
( M = $2 & $1 = [ the Sorts of M, the Charact of M] );
A1: for x, y, z being set st S1[x,y] & S1[x,z] holds
y = z
proof
let x, y, z be set ; ::_thesis: ( S1[x,y] & S1[x,z] implies y = z )
given M being strict feasible MSAlgebra over S such that A2: M = y and
A3: x = [ the Sorts of M, the Charact of M] ; ::_thesis: ( not S1[x,z] or y = z )
given N being strict feasible MSAlgebra over S such that A4: N = z and
A5: x = [ the Sorts of N, the Charact of N] ; ::_thesis: y = z
the Sorts of M = the Sorts of N by A3, A5, XTUPLE_0:1;
hence y = z by A2, A3, A4, A5, XTUPLE_0:1; ::_thesis: verum
end;
consider X being set such that
A6: for x being set holds
( x in X iff ex y being set st
( y in [:(Funcs ( the carrier of S,(bool A))),(Funcs ( the carrier' of S,(PFuncs ((PFuncs (NAT,A)),A)))):] & S1[y,x] ) ) from TARSKI:sch_1(A1);
take X ; ::_thesis: for x being set holds
( x in X iff ex M being strict feasible MSAlgebra over S st
( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) )
thus for x being set holds
( x in X iff ex M being strict feasible MSAlgebra over S st
( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) ) ::_thesis: verum
proof
let x be set ; ::_thesis: ( x in X iff ex M being strict feasible MSAlgebra over S st
( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) )
hereby ::_thesis: ( ex M being strict feasible MSAlgebra over S st
( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) implies x in X )
assume x in X ; ::_thesis: ex M being strict feasible MSAlgebra over S st
( x = M & ( for C being Component of the Sorts of M holds C c= A ) )
then consider y being set such that
A7: y in [:(Funcs ( the carrier of S,(bool A))),(Funcs ( the carrier' of S,(PFuncs ((PFuncs (NAT,A)),A)))):] and
A8: S1[y,x] by A6;
consider M being strict feasible MSAlgebra over S such that
A9: M = x and
y = [ the Sorts of M, the Charact of M] by A8;
take M = M; ::_thesis: ( x = M & ( for C being Component of the Sorts of M holds C c= A ) )
thus x = M by A9; ::_thesis: for C being Component of the Sorts of M holds C c= A
thus for C being Component of the Sorts of M holds C c= A ::_thesis: verum
proof
let C be Component of the Sorts of M; ::_thesis: C c= A
consider y1 being set such that
y1 in dom the Sorts of M and
A10: C = the Sorts of M . y1 by FUNCT_1:def_3;
the Sorts of M in Funcs ( the carrier of S,(bool A)) by A7, A8, A9, ZFMISC_1:87;
then consider f being Function such that
A11: the Sorts of M = f and
dom f = the carrier of S and
A12: rng f c= bool A by FUNCT_2:def_2;
f . y1 in rng f by A10, A11;
hence C c= A by A10, A11, A12; ::_thesis: verum
end;
end;
given M being strict feasible MSAlgebra over S such that A13: x = M and
A14: for C being Component of the Sorts of M holds C c= A ; ::_thesis: x in X
A15: dom the Sorts of M = the carrier of S by PARTFUN1:def_2;
then reconsider SM = the Sorts of M as Function of the carrier of S,(rng the Sorts of M) by FUNCT_2:1;
A16: rng the Sorts of M c= bool A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng the Sorts of M or x in bool A )
assume x in rng the Sorts of M ; ::_thesis: x in bool A
then reconsider x9 = x as Component of the Sorts of M ;
x9 c= A by A14;
hence x in bool A ; ::_thesis: verum
end;
then reconsider SM9 = SM as Function of the carrier of S,(bool A) by FUNCT_2:6;
consider y being set such that
A17: y = [ the Sorts of M, the Charact of M] ;
A18: dom the Charact of M = the carrier' of S by PARTFUN1:def_2;
rng the Charact of M c= PFuncs ((PFuncs (NAT,A)),A)
proof
reconsider SA = ( the Sorts of M #) * the Arity of S, SR = the Sorts of M * the ResultSort of S as ManySortedSet of the carrier' of S ;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng the Charact of M or x in PFuncs ((PFuncs (NAT,A)),A) )
reconsider CM = the Charact of M as ManySortedFunction of SA,SR ;
assume x in rng the Charact of M ; ::_thesis: x in PFuncs ((PFuncs (NAT,A)),A)
then consider x1 being set such that
A19: x1 in dom the Charact of M and
A20: x = the Charact of M . x1 by FUNCT_1:def_3;
reconsider Cm = CM . x1 as Function of (SA . x1),(SR . x1) by A19, PBOOLE:def_15;
A21: x1 in dom SA by A18, A19, PARTFUN1:def_2;
SA . x1 c= PFuncs (NAT,A)
proof
reconsider AX = the Arity of S . x1 as Element of the carrier of S * by A19, FUNCT_2:5;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in SA . x1 or a in PFuncs (NAT,A) )
assume a in SA . x1 ; ::_thesis: a in PFuncs (NAT,A)
then A22: a in ( the Sorts of M #) . ( the Arity of S . x1) by A21, FUNCT_1:12;
( the Sorts of M #) . AX = product ( the Sorts of M * AX) by FINSEQ_2:def_5;
then A23: ex g being Function st
( a = g & dom g = dom ( the Sorts of M * AX) & ( for x2 being set st x2 in dom ( the Sorts of M * AX) holds
g . x2 in ( the Sorts of M * AX) . x2 ) ) by A22, CARD_3:def_5;
then reconsider a9 = a as Function ;
rng AX c= dom the Sorts of M by A15;
then A24: dom a9 = dom AX by A23, RELAT_1:27;
rng a9 c= A
proof
rng the Sorts of M c= bool A
proof
let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in rng the Sorts of M or w in bool A )
assume w in rng the Sorts of M ; ::_thesis: w in bool A
then reconsider w9 = w as Component of the Sorts of M ;
w9 c= A by A14;
hence w in bool A ; ::_thesis: verum
end;
then A25: union (rng the Sorts of M) c= union (bool A) by ZFMISC_1:77;
let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in rng a9 or r in A )
assume r in rng a9 ; ::_thesis: r in A
then consider r1 being set such that
A26: r1 in dom a9 and
A27: r = a9 . r1 by FUNCT_1:def_3;
AX . r1 in rng AX by A24, A26, FUNCT_1:def_3;
then A28: the Sorts of M . (AX . r1) in rng the Sorts of M by A15, FUNCT_1:def_3;
r in ( the Sorts of M * AX) . r1 by A23, A26, A27;
then r in the Sorts of M . (AX . r1) by A24, A26, FUNCT_1:13;
then r in union (rng the Sorts of M) by A28, TARSKI:def_4;
then r in union (bool A) by A25;
hence r in A by ZFMISC_1:81; ::_thesis: verum
end;
hence a in PFuncs (NAT,A) by A23, PARTFUN1:def_3; ::_thesis: verum
end;
then A29: dom Cm c= PFuncs (NAT,A) by XBOOLE_1:1;
x1 in dom SR by A18, A19, PARTFUN1:def_2;
then A30: SR . x1 = the Sorts of M . ( the ResultSort of S . x1) by FUNCT_1:12;
the ResultSort of S . x1 in the carrier of S by A19, FUNCT_2:5;
then SR . x1 in rng the Sorts of M by A15, A30, FUNCT_1:def_3;
then rng Cm c= A by A16, XBOOLE_1:1;
hence x in PFuncs ((PFuncs (NAT,A)),A) by A20, A29, PARTFUN1:def_3; ::_thesis: verum
end;
then ( SM9 in Funcs ( the carrier of S,(bool A)) & the Charact of M in Funcs ( the carrier' of S,(PFuncs ((PFuncs (NAT,A)),A))) ) by A18, FUNCT_2:8, FUNCT_2:def_2;
then y in [:(Funcs ( the carrier of S,(bool A))),(Funcs ( the carrier' of S,(PFuncs ((PFuncs (NAT,A)),A)))):] by A17, ZFMISC_1:87;
hence x in X by A6, A13, A17; ::_thesis: verum
end;
end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ex M being strict feasible MSAlgebra over S st
( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) ) ) & ( for x being set holds
( x in b2 iff ex M being strict feasible MSAlgebra over S st
( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) ) ) holds
b1 = b2
proof
let A1, A2 be set ; ::_thesis: ( ( for x being set holds
( x in A1 iff ex M being strict feasible MSAlgebra over S st
( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) ) ) & ( for x being set holds
( x in A2 iff ex M being strict feasible MSAlgebra over S st
( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) ) ) implies A1 = A2 )
assume A31: for x being set holds
( x in A1 iff ex M being strict feasible MSAlgebra over S st
( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) ) ; ::_thesis: ( ex x being set st
( ( x in A2 implies ex M being strict feasible MSAlgebra over S st
( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) ) implies ( ex M being strict feasible MSAlgebra over S st
( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) & not x in A2 ) ) or A1 = A2 )
assume A32: for x being set holds
( x in A2 iff ex N being strict feasible MSAlgebra over S st
( x = N & ( for C being Component of the Sorts of N holds C c= A ) ) ) ; ::_thesis: A1 = A2
A33: A2 c= A1
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A2 or a in A1 )
assume a in A2 ; ::_thesis: a in A1
then ex M being strict feasible MSAlgebra over S st
( a = M & ( for C being Component of the Sorts of M holds C c= A ) ) by A32;
hence a in A1 by A31; ::_thesis: verum
end;
A1 c= A2
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A1 or a in A2 )
assume a in A1 ; ::_thesis: a in A2
then ex M being strict feasible MSAlgebra over S st
( a = M & ( for C being Component of the Sorts of M holds C c= A ) ) by A31;
hence a in A2 by A32; ::_thesis: verum
end;
hence A1 = A2 by A33, XBOOLE_0:def_10; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines MSAlg_set MSINST_1:def_2_:_
for S being non empty non void ManySortedSign
for A being non empty set
for b3 being set holds
( b3 = MSAlg_set (S,A) iff for x being set holds
( x in b3 iff ex M being strict feasible MSAlgebra over S st
( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) ) );
registration
let S be non empty non void ManySortedSign ;
let A be non empty set ;
cluster MSAlg_set (S,A) -> non empty ;
coherence
not MSAlg_set (S,A) is empty
proof
set a = the Element of A;
reconsider f = the carrier of S --> { the Element of A} as ManySortedSet of the carrier of S ;
set Ch = the ManySortedFunction of (f #) * the Arity of S,f * the ResultSort of S;
set Ex = MSAlgebra(# f, the ManySortedFunction of (f #) * the Arity of S,f * the ResultSort of S #);
reconsider Ex = MSAlgebra(# f, the ManySortedFunction of (f #) * the Arity of S,f * the ResultSort of S #) as non-empty MSAlgebra over S by MSUALG_1:def_3;
reconsider Ex = Ex as strict feasible MSAlgebra over S ;
for C being Component of the Sorts of Ex holds C c= A
proof
let C be Component of the Sorts of Ex; ::_thesis: C c= A
ex i being set st
( i in the carrier of S & C = the Sorts of Ex . i ) by PBOOLE:138;
then C = { the Element of A} by FUNCOP_1:7;
hence C c= A by ZFMISC_1:31; ::_thesis: verum
end;
hence not MSAlg_set (S,A) is empty by Def2; ::_thesis: verum
end;
end;
begin
theorem :: MSINST_1:2
for A being non empty set
for S being non empty non void ManySortedSign
for x being MSAlgebra over S st x in MSAlg_set (S,A) holds
( the Sorts of x in Funcs ( the carrier of S,(bool A)) & the Charact of x in Funcs ( the carrier' of S,(PFuncs ((PFuncs (NAT,A)),A))) )
proof
let A be non empty set ; ::_thesis: for S being non empty non void ManySortedSign
for x being MSAlgebra over S st x in MSAlg_set (S,A) holds
( the Sorts of x in Funcs ( the carrier of S,(bool A)) & the Charact of x in Funcs ( the carrier' of S,(PFuncs ((PFuncs (NAT,A)),A))) )
let S be non empty non void ManySortedSign ; ::_thesis: for x being MSAlgebra over S st x in MSAlg_set (S,A) holds
( the Sorts of x in Funcs ( the carrier of S,(bool A)) & the Charact of x in Funcs ( the carrier' of S,(PFuncs ((PFuncs (NAT,A)),A))) )
let x be MSAlgebra over S; ::_thesis: ( x in MSAlg_set (S,A) implies ( the Sorts of x in Funcs ( the carrier of S,(bool A)) & the Charact of x in Funcs ( the carrier' of S,(PFuncs ((PFuncs (NAT,A)),A))) ) )
assume x in MSAlg_set (S,A) ; ::_thesis: ( the Sorts of x in Funcs ( the carrier of S,(bool A)) & the Charact of x in Funcs ( the carrier' of S,(PFuncs ((PFuncs (NAT,A)),A))) )
then consider M being strict feasible MSAlgebra over S such that
A1: x = M and
A2: for C being Component of the Sorts of M holds C c= A by Def2;
A3: dom the Sorts of M = the carrier of S by PARTFUN1:def_2;
then reconsider SM = the Sorts of M as Function of the carrier of S,(rng the Sorts of M) by FUNCT_2:1;
A4: rng the Sorts of M c= bool A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng the Sorts of M or x in bool A )
assume x in rng the Sorts of M ; ::_thesis: x in bool A
then reconsider x9 = x as Component of the Sorts of M ;
x9 c= A by A2;
hence x in bool A ; ::_thesis: verum
end;
then reconsider SM9 = SM as Function of the carrier of S,(bool A) by FUNCT_2:6;
A5: dom the Charact of M = the carrier' of S by PARTFUN1:def_2;
A6: rng the Charact of M c= PFuncs ((PFuncs (NAT,A)),A)
proof
reconsider SA = ( the Sorts of M #) * the Arity of S, SR = the Sorts of M * the ResultSort of S as ManySortedSet of the carrier' of S ;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng the Charact of M or x in PFuncs ((PFuncs (NAT,A)),A) )
reconsider CM = the Charact of M as ManySortedFunction of SA,SR ;
assume x in rng the Charact of M ; ::_thesis: x in PFuncs ((PFuncs (NAT,A)),A)
then consider x1 being set such that
A7: x1 in dom the Charact of M and
A8: x = the Charact of M . x1 by FUNCT_1:def_3;
reconsider Cm = CM . x1 as Function of (SA . x1),(SR . x1) by A7, PBOOLE:def_15;
A9: x1 in dom SA by A5, A7, PARTFUN1:def_2;
SA . x1 c= PFuncs (NAT,A)
proof
reconsider AX = the Arity of S . x1 as Element of the carrier of S * by A7, FUNCT_2:5;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in SA . x1 or a in PFuncs (NAT,A) )
assume a in SA . x1 ; ::_thesis: a in PFuncs (NAT,A)
then A10: a in ( the Sorts of M #) . ( the Arity of S . x1) by A9, FUNCT_1:12;
( the Sorts of M #) . AX = product ( the Sorts of M * AX) by FINSEQ_2:def_5;
then A11: ex g being Function st
( a = g & dom g = dom ( the Sorts of M * AX) & ( for x2 being set st x2 in dom ( the Sorts of M * AX) holds
g . x2 in ( the Sorts of M * AX) . x2 ) ) by A10, CARD_3:def_5;
then reconsider a9 = a as Function ;
rng AX c= dom the Sorts of M by A3;
then A12: dom a9 = dom AX by A11, RELAT_1:27;
rng a9 c= A
proof
rng the Sorts of M c= bool A
proof
let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in rng the Sorts of M or w in bool A )
assume w in rng the Sorts of M ; ::_thesis: w in bool A
then reconsider w9 = w as Component of the Sorts of M ;
w9 c= A by A2;
hence w in bool A ; ::_thesis: verum
end;
then A13: union (rng the Sorts of M) c= union (bool A) by ZFMISC_1:77;
let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in rng a9 or r in A )
assume r in rng a9 ; ::_thesis: r in A
then consider r1 being set such that
A14: r1 in dom a9 and
A15: r = a9 . r1 by FUNCT_1:def_3;
AX . r1 in rng AX by A12, A14, FUNCT_1:def_3;
then A16: the Sorts of M . (AX . r1) in rng the Sorts of M by A3, FUNCT_1:def_3;
r in ( the Sorts of M * AX) . r1 by A11, A14, A15;
then r in the Sorts of M . (AX . r1) by A12, A14, FUNCT_1:13;
then r in union (rng the Sorts of M) by A16, TARSKI:def_4;
then r in union (bool A) by A13;
hence r in A by ZFMISC_1:81; ::_thesis: verum
end;
hence a in PFuncs (NAT,A) by A11, PARTFUN1:def_3; ::_thesis: verum
end;
then A17: dom Cm c= PFuncs (NAT,A) by XBOOLE_1:1;
x1 in dom SR by A5, A7, PARTFUN1:def_2;
then A18: SR . x1 = the Sorts of M . ( the ResultSort of S . x1) by FUNCT_1:12;
the ResultSort of S . x1 in the carrier of S by A7, FUNCT_2:5;
then SR . x1 in rng the Sorts of M by A3, A18, FUNCT_1:def_3;
then rng Cm c= A by A4, XBOOLE_1:1;
hence x in PFuncs ((PFuncs (NAT,A)),A) by A8, A17, PARTFUN1:def_3; ::_thesis: verum
end;
SM9 in Funcs ( the carrier of S,(bool A)) by FUNCT_2:8;
hence ( the Sorts of x in Funcs ( the carrier of S,(bool A)) & the Charact of x in Funcs ( the carrier' of S,(PFuncs ((PFuncs (NAT,A)),A))) ) by A1, A5, A6, FUNCT_2:def_2; ::_thesis: verum
end;
theorem Th3: :: MSINST_1:3
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U1, U2 being MSAlgebra over S st the Sorts of U1 is_transformable_to the Sorts of U2 & Args (o,U1) <> {} holds
Args (o,U2) <> {}
proof
let S be non empty non void ManySortedSign ; ::_thesis: for o being OperSymbol of S
for U1, U2 being MSAlgebra over S st the Sorts of U1 is_transformable_to the Sorts of U2 & Args (o,U1) <> {} holds
Args (o,U2) <> {}
let o be OperSymbol of S; ::_thesis: for U1, U2 being MSAlgebra over S st the Sorts of U1 is_transformable_to the Sorts of U2 & Args (o,U1) <> {} holds
Args (o,U2) <> {}
let U1, U2 be MSAlgebra over S; ::_thesis: ( the Sorts of U1 is_transformable_to the Sorts of U2 & Args (o,U1) <> {} implies Args (o,U2) <> {} )
assume that
A1: the Sorts of U1 is_transformable_to the Sorts of U2 and
A2: Args (o,U1) <> {} ; ::_thesis: Args (o,U2) <> {}
A3: (( the Sorts of U1 #) * the Arity of S) . o <> {} by A2, MSUALG_1:def_4;
dom the Sorts of U1 = the carrier of S by PARTFUN1:def_2;
then rng (the_arity_of o) c= dom the Sorts of U1 ;
then A4: dom ( the Sorts of U1 * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27;
A5: dom ( the Sorts of U2 * (the_arity_of o)) c= dom (the_arity_of o) by RELAT_1:25;
A6: dom the Arity of S = the carrier' of S by FUNCT_2:def_1;
then (( the Sorts of U1 #) * the Arity of S) . o = ( the Sorts of U1 #) . ( the Arity of S . o) by FUNCT_1:13
.= ( the Sorts of U1 #) . (the_arity_of o) by MSUALG_1:def_1 ;
then product ( the Sorts of U1 * (the_arity_of o)) <> {} by A3, FINSEQ_2:def_5;
then A7: not {} in rng ( the Sorts of U1 * (the_arity_of o)) by CARD_3:26;
now__::_thesis:_for_x_being_set_st_x_in_dom_(_the_Sorts_of_U2_*_(the_arity_of_o))_holds_
(_the_Sorts_of_U2_*_(the_arity_of_o))_._x_<>_{}
let x be set ; ::_thesis: ( x in dom ( the Sorts of U2 * (the_arity_of o)) implies ( the Sorts of U2 * (the_arity_of o)) . x <> {} )
assume A8: x in dom ( the Sorts of U2 * (the_arity_of o)) ; ::_thesis: ( the Sorts of U2 * (the_arity_of o)) . x <> {}
then (the_arity_of o) . x in rng (the_arity_of o) by A5, FUNCT_1:def_3;
then A9: ( the Sorts of U1 . ((the_arity_of o) . x) <> {} implies the Sorts of U2 . ((the_arity_of o) . x) <> {} ) by A1, PZFMISC1:def_3;
( the Sorts of U1 * (the_arity_of o)) . x = the Sorts of U1 . ((the_arity_of o) . x) by A5, A8, FUNCT_1:13;
hence ( the Sorts of U2 * (the_arity_of o)) . x <> {} by A7, A4, A5, A8, A9, FUNCT_1:13, FUNCT_1:def_3; ::_thesis: verum
end;
then not {} in rng ( the Sorts of U2 * (the_arity_of o)) by FUNCT_1:def_3;
then product ( the Sorts of U2 * (the_arity_of o)) <> {} by CARD_3:26;
then ( the Sorts of U2 #) . (the_arity_of o) <> {} by FINSEQ_2:def_5;
then ( the Sorts of U2 #) . ( the Arity of S . o) <> {} by MSUALG_1:def_1;
then (( the Sorts of U2 #) * the Arity of S) . o <> {} by A6, FUNCT_1:13;
hence Args (o,U2) <> {} by MSUALG_1:def_4; ::_thesis: verum
end;
theorem Th4: :: MSINST_1:4
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U1, U2, U3 being feasible MSAlgebra over S
for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U2,U3
for x being Element of Args (o,U1) st Args (o,U1) <> {} & the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 holds
ex GF being ManySortedFunction of U1,U3 st
( GF = G ** F & GF # x = G # (F # x) )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for o being OperSymbol of S
for U1, U2, U3 being feasible MSAlgebra over S
for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U2,U3
for x being Element of Args (o,U1) st Args (o,U1) <> {} & the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 holds
ex GF being ManySortedFunction of U1,U3 st
( GF = G ** F & GF # x = G # (F # x) )
let o be OperSymbol of S; ::_thesis: for U1, U2, U3 being feasible MSAlgebra over S
for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U2,U3
for x being Element of Args (o,U1) st Args (o,U1) <> {} & the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 holds
ex GF being ManySortedFunction of U1,U3 st
( GF = G ** F & GF # x = G # (F # x) )
let U1, U2, U3 be feasible MSAlgebra over S; ::_thesis: for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U2,U3
for x being Element of Args (o,U1) st Args (o,U1) <> {} & the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 holds
ex GF being ManySortedFunction of U1,U3 st
( GF = G ** F & GF # x = G # (F # x) )
let F be ManySortedFunction of U1,U2; ::_thesis: for G being ManySortedFunction of U2,U3
for x being Element of Args (o,U1) st Args (o,U1) <> {} & the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 holds
ex GF being ManySortedFunction of U1,U3 st
( GF = G ** F & GF # x = G # (F # x) )
let G be ManySortedFunction of U2,U3; ::_thesis: for x being Element of Args (o,U1) st Args (o,U1) <> {} & the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 holds
ex GF being ManySortedFunction of U1,U3 st
( GF = G ** F & GF # x = G # (F # x) )
let x be Element of Args (o,U1); ::_thesis: ( Args (o,U1) <> {} & the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 implies ex GF being ManySortedFunction of U1,U3 st
( GF = G ** F & GF # x = G # (F # x) ) )
assume that
A1: Args (o,U1) <> {} and
A2: the Sorts of U1 is_transformable_to the Sorts of U2 and
A3: the Sorts of U2 is_transformable_to the Sorts of U3 ; ::_thesis: ex GF being ManySortedFunction of U1,U3 st
( GF = G ** F & GF # x = G # (F # x) )
x in Args (o,U1) by A1;
then x in product ( the Sorts of U1 * (the_arity_of o)) by PRALG_2:3;
then A4: ex g being Function st
( x = g & dom g = dom ( the Sorts of U1 * (the_arity_of o)) & ( for x being set st x in dom ( the Sorts of U1 * (the_arity_of o)) holds
g . x in ( the Sorts of U1 * (the_arity_of o)) . x ) ) by CARD_3:def_5;
then reconsider x9 = x as Function ;
reconsider Fr = (Frege (F * (the_arity_of o))) . x9 as Function ;
dom F = the carrier of S by PARTFUN1:def_2;
then A5: rng (the_arity_of o) c= dom F ;
then A6: dom (F * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27;
A7: dom (doms (F * (the_arity_of o))) = dom (F * (the_arity_of o)) by FUNCT_6:59;
then A8: dom x9 = dom (doms (F * (the_arity_of o))) by A1, A6, MSUALG_3:6;
then reconsider x99 = x9 as ManySortedSet of dom (the_arity_of o) by A6, A7, PARTFUN1:def_2, RELAT_1:def_18;
dom G = the carrier of S by PARTFUN1:def_2;
then rng (the_arity_of o) c= dom G ;
then A9: dom (G * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27;
then reconsider Ga = G * (the_arity_of o), Fa = F * (the_arity_of o) as ManySortedFunction of dom (the_arity_of o) by A6, PARTFUN1:def_2, RELAT_1:def_18;
A10: Args (o,U2) <> {} by A1, A2, Th3;
dom the Sorts of U1 = the carrier of S by PARTFUN1:def_2;
then A11: rng (the_arity_of o) c= dom the Sorts of U1 ;
now__::_thesis:_for_x_being_set_st_x_in_dom_(doms_(F_*_(the_arity_of_o)))_holds_
x9_._x_in_(doms_(F_*_(the_arity_of_o)))_._x
let x be set ; ::_thesis: ( x in dom (doms (F * (the_arity_of o))) implies x9 . x in (doms (F * (the_arity_of o))) . x )
set ds = (the_arity_of o) . x;
assume x in dom (doms (F * (the_arity_of o))) ; ::_thesis: x9 . x in (doms (F * (the_arity_of o))) . x
then A12: x in dom (F * (the_arity_of o)) by FUNCT_6:59;
then A13: (doms (F * (the_arity_of o))) . x = dom ((F * (the_arity_of o)) . x) by FUNCT_6:22;
A14: x in dom (the_arity_of o) by A5, A12, RELAT_1:27;
then A15: (the_arity_of o) . x in rng (the_arity_of o) by FUNCT_1:def_3;
then reconsider Ff = F . ((the_arity_of o) . x) as Function of ( the Sorts of U1 . ((the_arity_of o) . x)),( the Sorts of U2 . ((the_arity_of o) . x)) by PBOOLE:def_15;
x in dom ( the Sorts of U1 * (the_arity_of o)) by A11, A14, RELAT_1:27;
then A16: x9 . x in ( the Sorts of U1 * (the_arity_of o)) . x by A1, MSUALG_3:6;
A17: the Sorts of U1 . ((the_arity_of o) . x) = dom Ff
proof
percases ( the Sorts of U2 . ((the_arity_of o) . x) <> {} or the Sorts of U2 . ((the_arity_of o) . x) = {} ) ;
suppose the Sorts of U2 . ((the_arity_of o) . x) <> {} ; ::_thesis: the Sorts of U1 . ((the_arity_of o) . x) = dom Ff
hence the Sorts of U1 . ((the_arity_of o) . x) = dom Ff by FUNCT_2:def_1; ::_thesis: verum
end;
suppose the Sorts of U2 . ((the_arity_of o) . x) = {} ; ::_thesis: the Sorts of U1 . ((the_arity_of o) . x) = dom Ff
then the Sorts of U1 . ((the_arity_of o) . x) = {} by A2, A15, PZFMISC1:def_3;
hence the Sorts of U1 . ((the_arity_of o) . x) = dom Ff ; ::_thesis: verum
end;
end;
end;
(F * (the_arity_of o)) . x = F . ((the_arity_of o) . x) by A14, FUNCT_1:13;
hence x9 . x in (doms (F * (the_arity_of o))) . x by A13, A14, A16, A17, FUNCT_1:13; ::_thesis: verum
end;
then A18: x9 in product (doms (F * (the_arity_of o))) by A8, CARD_3:9;
then A19: Fr = (F * (the_arity_of o)) .. x9 by PRALG_2:def_2;
A20: now__::_thesis:_for_x_being_set_st_x_in_dom_(doms_(G_*_(the_arity_of_o)))_holds_
Fr_._x_in_(doms_(G_*_(the_arity_of_o)))_._x
let x be set ; ::_thesis: ( x in dom (doms (G * (the_arity_of o))) implies Fr . x in (doms (G * (the_arity_of o))) . x )
set ds = (the_arity_of o) . x;
assume A21: x in dom (doms (G * (the_arity_of o))) ; ::_thesis: Fr . x in (doms (G * (the_arity_of o))) . x
then A22: x in dom (G * (the_arity_of o)) by FUNCT_6:59;
x in dom (F * (the_arity_of o)) by A9, A6, A21, FUNCT_6:59;
then A23: Fr . x = ((F * (the_arity_of o)) . x) . (x9 . x) by A19, PRALG_1:def_17;
A24: dom ( the Sorts of U1 * (the_arity_of o)) = dom (the_arity_of o) by A11, RELAT_1:27;
A25: x in dom (the_arity_of o) by A9, A21, FUNCT_6:59;
then A26: (the_arity_of o) . x in rng (the_arity_of o) by FUNCT_1:def_3;
then reconsider Ff = F . ((the_arity_of o) . x) as Function of ( the Sorts of U1 . ((the_arity_of o) . x)),( the Sorts of U2 . ((the_arity_of o) . x)) by PBOOLE:def_15;
A27: (F * (the_arity_of o)) . x = Ff by A6, A25, FUNCT_1:12;
reconsider Gds = G . ((the_arity_of o) . x) as Function of ( the Sorts of U2 . ((the_arity_of o) . x)),( the Sorts of U3 . ((the_arity_of o) . x)) by A26, PBOOLE:def_15;
A28: dom Gds = the Sorts of U2 . ((the_arity_of o) . x)
proof
percases ( the Sorts of U3 . ((the_arity_of o) . x) <> {} or the Sorts of U3 . ((the_arity_of o) . x) = {} ) ;
suppose the Sorts of U3 . ((the_arity_of o) . x) <> {} ; ::_thesis: dom Gds = the Sorts of U2 . ((the_arity_of o) . x)
hence dom Gds = the Sorts of U2 . ((the_arity_of o) . x) by FUNCT_2:def_1; ::_thesis: verum
end;
suppose the Sorts of U3 . ((the_arity_of o) . x) = {} ; ::_thesis: dom Gds = the Sorts of U2 . ((the_arity_of o) . x)
then the Sorts of U2 . ((the_arity_of o) . x) = {} by A3, A26, PZFMISC1:def_3;
hence dom Gds = the Sorts of U2 . ((the_arity_of o) . x) ; ::_thesis: verum
end;
end;
end;
A29: the Sorts of U1 . ((the_arity_of o) . x) = dom Ff
proof
percases ( the Sorts of U2 . ((the_arity_of o) . x) <> {} or the Sorts of U2 . ((the_arity_of o) . x) = {} ) ;
suppose the Sorts of U2 . ((the_arity_of o) . x) <> {} ; ::_thesis: the Sorts of U1 . ((the_arity_of o) . x) = dom Ff
hence the Sorts of U1 . ((the_arity_of o) . x) = dom Ff by FUNCT_2:def_1; ::_thesis: verum
end;
suppose the Sorts of U2 . ((the_arity_of o) . x) = {} ; ::_thesis: the Sorts of U1 . ((the_arity_of o) . x) = dom Ff
then the Sorts of U1 . ((the_arity_of o) . x) = {} by A2, A26, PZFMISC1:def_3;
hence the Sorts of U1 . ((the_arity_of o) . x) = dom Ff ; ::_thesis: verum
end;
end;
end;
( the Sorts of U1 * (the_arity_of o)) . x = the Sorts of U1 . ((the_arity_of o) . x) by A25, FUNCT_1:13;
then x9 . x in dom Ff by A1, A25, A24, A29, MSUALG_3:6;
then A30: ((F * (the_arity_of o)) . x) . (x9 . x) in rng Ff by A27, FUNCT_1:def_3;
(G * (the_arity_of o)) . x = G . ((the_arity_of o) . x) by A25, FUNCT_1:13;
then Fr . x in dom ((G * (the_arity_of o)) . x) by A28, A30, A23;
hence Fr . x in (doms (G * (the_arity_of o))) . x by A22, FUNCT_6:22; ::_thesis: verum
end;
reconsider GF = G ** F as ManySortedFunction of U1,U3 by A2, ALTCAT_2:4;
dom GF = the carrier of S by PARTFUN1:def_2;
then rng (the_arity_of o) c= dom GF ;
then A31: dom (GF * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27;
A32: x99 in doms Fa
proof
let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in dom (the_arity_of o) or x99 . i in (doms Fa) . i )
set ai = (the_arity_of o) . i;
assume A33: i in dom (the_arity_of o) ; ::_thesis: x99 . i in (doms Fa) . i
then A34: (the_arity_of o) . i in rng (the_arity_of o) by FUNCT_1:def_3;
Fa . i = F . ((the_arity_of o) . i) by A33, FUNCT_1:13;
then reconsider Ew = Fa . i as Function of ( the Sorts of U1 . ((the_arity_of o) . i)),( the Sorts of U2 . ((the_arity_of o) . i)) by A34, PBOOLE:def_15;
A35: dom Ew = the Sorts of U1 . ((the_arity_of o) . i)
proof
percases ( the Sorts of U2 . ((the_arity_of o) . i) = {} or the Sorts of U2 . ((the_arity_of o) . i) <> {} ) ;
suppose the Sorts of U2 . ((the_arity_of o) . i) = {} ; ::_thesis: dom Ew = the Sorts of U1 . ((the_arity_of o) . i)
then the Sorts of U1 . ((the_arity_of o) . i) = {} by A2, A34, PZFMISC1:def_3;
hence dom Ew = the Sorts of U1 . ((the_arity_of o) . i) ; ::_thesis: verum
end;
suppose the Sorts of U2 . ((the_arity_of o) . i) <> {} ; ::_thesis: dom Ew = the Sorts of U1 . ((the_arity_of o) . i)
hence dom Ew = the Sorts of U1 . ((the_arity_of o) . i) by FUNCT_2:def_1; ::_thesis: verum
end;
end;
end;
i in dom ( the Sorts of U1 * (the_arity_of o)) by A33, PRALG_2:3;
then x99 . i in ( the Sorts of U1 * (the_arity_of o)) . i by A4;
then x99 . i in dom (Fa . i) by A33, A35, FUNCT_1:13;
hence x99 . i in (doms Fa) . i by A33, MSSUBFAM:14; ::_thesis: verum
end;
take GF ; ::_thesis: ( GF = G ** F & GF # x = G # (F # x) )
thus GF = G ** F ; ::_thesis: GF # x = G # (F # x)
A36: (G * (the_arity_of o)) ** (F * (the_arity_of o)) = GF * (the_arity_of o) by FUNCTOR0:12;
A37: the Sorts of U1 is_transformable_to the Sorts of U3 by A2, A3, AUTALG_1:10;
A38: now__::_thesis:_for_x_being_set_st_x_in_dom_(doms_(GF_*_(the_arity_of_o)))_holds_
x9_._x_in_(doms_(GF_*_(the_arity_of_o)))_._x
let x be set ; ::_thesis: ( x in dom (doms (GF * (the_arity_of o))) implies x9 . x in (doms (GF * (the_arity_of o))) . x )
set ds = (the_arity_of o) . x;
assume A39: x in dom (doms (GF * (the_arity_of o))) ; ::_thesis: x9 . x in (doms (GF * (the_arity_of o))) . x
then A40: x in dom (the_arity_of o) by A31, FUNCT_6:59;
then A41: (the_arity_of o) . x in rng (the_arity_of o) by FUNCT_1:def_3;
then reconsider Gf = GF . ((the_arity_of o) . x) as Function of ( the Sorts of U1 . ((the_arity_of o) . x)),( the Sorts of U3 . ((the_arity_of o) . x)) by PBOOLE:def_15;
x in dom (GF * (the_arity_of o)) by A39, FUNCT_6:59;
then A42: (doms (GF * (the_arity_of o))) . x = dom ((GF * (the_arity_of o)) . x) by FUNCT_6:22;
A43: the Sorts of U1 . ((the_arity_of o) . x) = dom Gf
proof
percases ( the Sorts of U3 . ((the_arity_of o) . x) <> {} or the Sorts of U3 . ((the_arity_of o) . x) = {} ) ;
suppose the Sorts of U3 . ((the_arity_of o) . x) <> {} ; ::_thesis: the Sorts of U1 . ((the_arity_of o) . x) = dom Gf
hence the Sorts of U1 . ((the_arity_of o) . x) = dom Gf by FUNCT_2:def_1; ::_thesis: verum
end;
suppose the Sorts of U3 . ((the_arity_of o) . x) = {} ; ::_thesis: the Sorts of U1 . ((the_arity_of o) . x) = dom Gf
then the Sorts of U1 . ((the_arity_of o) . x) = {} by A37, A41, PZFMISC1:def_3;
hence the Sorts of U1 . ((the_arity_of o) . x) = dom Gf ; ::_thesis: verum
end;
end;
end;
x in dom ( the Sorts of U1 * (the_arity_of o)) by A11, A40, RELAT_1:27;
then x9 . x in ( the Sorts of U1 * (the_arity_of o)) . x by A1, MSUALG_3:6;
then x9 . x in dom (GF . ((the_arity_of o) . x)) by A40, A43, FUNCT_1:13;
hence x9 . x in (doms (GF * (the_arity_of o))) . x by A42, A40, FUNCT_1:13; ::_thesis: verum
end;
dom (doms (GF * (the_arity_of o))) = dom (GF * (the_arity_of o)) by FUNCT_6:59;
then dom x9 = dom (doms (GF * (the_arity_of o))) by A1, A31, MSUALG_3:6;
then A44: x9 in product (doms (GF * (the_arity_of o))) by A38, CARD_3:9;
dom Fr = dom (G * (the_arity_of o)) by A9, A6, A19, PRALG_1:def_17;
then dom Fr = dom (doms (G * (the_arity_of o))) by FUNCT_6:59;
then Fr in product (doms (G * (the_arity_of o))) by A20, CARD_3:9;
then A45: (Frege (G * (the_arity_of o))) . ((Frege (F * (the_arity_of o))) . x) = (G * (the_arity_of o)) .. ((Frege (F * (the_arity_of o))) . x) by PRALG_2:def_2
.= Ga .. (Fa .. x99) by A18, PRALG_2:def_2
.= (Ga ** Fa) .. x99 by A32, CLOSURE1:4 ;
A46: Args (o,U3) <> {} by A1, A2, A3, Th3, AUTALG_1:10;
then GF # x = (Frege (GF * (the_arity_of o))) . x by A1, MSUALG_3:def_5
.= (Frege (G * (the_arity_of o))) . ((Frege (F * (the_arity_of o))) . x) by A44, A45, A36, PRALG_2:def_2
.= (Frege (G * (the_arity_of o))) . (F # x) by A1, A10, MSUALG_3:def_5 ;
hence GF # x = G # (F # x) by A10, A46, MSUALG_3:def_5; ::_thesis: verum
end;
theorem Th5: :: MSINST_1:5
for S being non empty non void ManySortedSign
for U1, U2, U3 being feasible MSAlgebra over S
for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U2,U3 st the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 & F is_homomorphism U1,U2 & G is_homomorphism U2,U3 holds
ex GF being ManySortedFunction of U1,U3 st
( GF = G ** F & GF is_homomorphism U1,U3 )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2, U3 being feasible MSAlgebra over S
for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U2,U3 st the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 & F is_homomorphism U1,U2 & G is_homomorphism U2,U3 holds
ex GF being ManySortedFunction of U1,U3 st
( GF = G ** F & GF is_homomorphism U1,U3 )
let U1, U2, U3 be feasible MSAlgebra over S; ::_thesis: for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U2,U3 st the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 & F is_homomorphism U1,U2 & G is_homomorphism U2,U3 holds
ex GF being ManySortedFunction of U1,U3 st
( GF = G ** F & GF is_homomorphism U1,U3 )
let F be ManySortedFunction of U1,U2; ::_thesis: for G being ManySortedFunction of U2,U3 st the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 & F is_homomorphism U1,U2 & G is_homomorphism U2,U3 holds
ex GF being ManySortedFunction of U1,U3 st
( GF = G ** F & GF is_homomorphism U1,U3 )
let G be ManySortedFunction of U2,U3; ::_thesis: ( the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 & F is_homomorphism U1,U2 & G is_homomorphism U2,U3 implies ex GF being ManySortedFunction of U1,U3 st
( GF = G ** F & GF is_homomorphism U1,U3 ) )
assume that
A1: the Sorts of U1 is_transformable_to the Sorts of U2 and
A2: the Sorts of U2 is_transformable_to the Sorts of U3 and
A3: F is_homomorphism U1,U2 and
A4: G is_homomorphism U2,U3 ; ::_thesis: ex GF being ManySortedFunction of U1,U3 st
( GF = G ** F & GF is_homomorphism U1,U3 )
reconsider GF = G ** F as ManySortedFunction of U1,U3 by A1, ALTCAT_2:4;
take GF ; ::_thesis: ( GF = G ** F & GF is_homomorphism U1,U3 )
thus GF = G ** F ; ::_thesis: GF is_homomorphism U1,U3
thus GF is_homomorphism U1,U3 ::_thesis: verum
proof
let o be OperSymbol of S; :: according to MSUALG_3:def_7 ::_thesis: ( Args (o,U1) = {} or for b1 being Element of Args (o,U1) holds (GF . (the_result_sort_of o)) . ((Den (o,U1)) . b1) = (Den (o,U3)) . (GF # b1) )
assume A5: Args (o,U1) <> {} ; ::_thesis: for b1 being Element of Args (o,U1) holds (GF . (the_result_sort_of o)) . ((Den (o,U1)) . b1) = (Den (o,U3)) . (GF # b1)
let x be Element of Args (o,U1); ::_thesis: (GF . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U3)) . (GF # x)
A6: ex gf being ManySortedFunction of U1,U3 st
( gf = G ** F & gf # x = G # (F # x) ) by A1, A2, A5, Th4;
set r = the_result_sort_of o;
( (F . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U2)) . (F # x) & Args (o,U2) <> {} ) by A1, A3, A5, Th3, MSUALG_3:def_7;
then A7: (G . (the_result_sort_of o)) . ((F . (the_result_sort_of o)) . ((Den (o,U1)) . x)) = (Den (o,U3)) . (G # (F # x)) by A4, MSUALG_3:def_7;
A8: the Sorts of U1 is_transformable_to the Sorts of U3 by A1, A2, AUTALG_1:10;
A9: dom (GF . (the_result_sort_of o)) = the Sorts of U1 . (the_result_sort_of o)
proof
percases ( the Sorts of U1 . (the_result_sort_of o) <> {} or the Sorts of U1 . (the_result_sort_of o) = {} ) ;
suppose the Sorts of U1 . (the_result_sort_of o) <> {} ; ::_thesis: dom (GF . (the_result_sort_of o)) = the Sorts of U1 . (the_result_sort_of o)
then the Sorts of U3 . (the_result_sort_of o) <> {} by A8, PZFMISC1:def_3;
hence dom (GF . (the_result_sort_of o)) = the Sorts of U1 . (the_result_sort_of o) by FUNCT_2:def_1; ::_thesis: verum
end;
suppose the Sorts of U1 . (the_result_sort_of o) = {} ; ::_thesis: dom (GF . (the_result_sort_of o)) = the Sorts of U1 . (the_result_sort_of o)
hence dom (GF . (the_result_sort_of o)) = the Sorts of U1 . (the_result_sort_of o) ; ::_thesis: verum
end;
end;
end;
o in the carrier' of S ;
then A10: o in dom the ResultSort of S by FUNCT_2:def_1;
rng the ResultSort of S c= the carrier of S ;
then rng the ResultSort of S c= dom the Sorts of U1 by PARTFUN1:def_2;
then ( Result (o,U1) = ( the Sorts of U1 * the ResultSort of S) . o & dom ( the Sorts of U1 * the ResultSort of S) = dom the ResultSort of S ) by MSUALG_1:def_5, RELAT_1:27;
then A11: Result (o,U1) = the Sorts of U1 . ( the ResultSort of S . o) by A10, FUNCT_1:12
.= the Sorts of U1 . (the_result_sort_of o) by MSUALG_1:def_2 ;
then ( GF . (the_result_sort_of o) = (G . (the_result_sort_of o)) * (F . (the_result_sort_of o)) & the Sorts of U1 . (the_result_sort_of o) <> {} ) by A5, MSUALG_3:2, MSUALG_6:def_1;
hence (GF . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U3)) . (GF # x) by A5, A7, A9, A11, A6, FUNCT_1:12, FUNCT_2:5; ::_thesis: verum
end;
end;
definition
let S be non empty non void ManySortedSign ;
let A be non empty set ;
let i, j be set ;
assume that
A1: i in MSAlg_set (S,A) and
A2: j in MSAlg_set (S,A) ;
func MSAlg_morph (S,A,i,j) -> set means :Def3: :: MSINST_1:def 3
for x being set holds
( x in it iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st
( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st
( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) )
proof
consider M being strict feasible MSAlgebra over S such that
A3: i = M and
A4: for C being Component of the Sorts of M holds C c= A by A1, Def2;
consider N being strict feasible MSAlgebra over S such that
A5: j = N and
A6: for C being Component of the Sorts of N holds C c= A by A2, Def2;
defpred S1[ set ] means ( the Sorts of M is_transformable_to the Sorts of N & ex f being ManySortedFunction of M,N st
( $1 = f & f is_homomorphism M,N ) );
consider X being set such that
A7: for x being set holds
( x in X iff ( x in Funcs ( the carrier of S,(PFuncs ((union (bool A)),(union (bool A))))) & S1[x] ) ) from XBOOLE_0:sch_1();
take X ; ::_thesis: for x being set holds
( x in X iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st
( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) )
let x be set ; ::_thesis: ( x in X iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st
( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) )
hereby ::_thesis: ( ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st
( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) implies x in X )
assume A8: x in X ; ::_thesis: ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st
( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N )
then consider f being ManySortedFunction of M,N such that
A9: x = f and
A10: f is_homomorphism M,N by A7;
take M = M; ::_thesis: ex N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st
( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N )
take N = N; ::_thesis: ex f being ManySortedFunction of M,N st
( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N )
reconsider f = f as ManySortedFunction of M,N ;
take f = f; ::_thesis: ( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N )
thus ( M = i & N = j & f = x ) by A3, A5, A9; ::_thesis: ( the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N )
thus the Sorts of M is_transformable_to the Sorts of N by A8, A7; ::_thesis: f is_homomorphism M,N
thus f is_homomorphism M,N by A10; ::_thesis: verum
end;
given M1, N1 being strict feasible MSAlgebra over S, f being ManySortedFunction of M1,N1 such that A11: ( M1 = i & N1 = j & f = x & the Sorts of M1 is_transformable_to the Sorts of N1 & f is_homomorphism M1,N1 ) ; ::_thesis: x in X
reconsider F = f as ManySortedFunction of M,N by A11, A3, A5;
A12: dom F = the carrier of S by PARTFUN1:def_2;
rng F c= PFuncs ((union (bool A)),(union (bool A)))
proof
A13: rng the Sorts of M c= bool A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng the Sorts of M or x in bool A )
assume x in rng the Sorts of M ; ::_thesis: x in bool A
then reconsider x9 = x as Component of the Sorts of M ;
x9 c= A by A4;
hence x in bool A ; ::_thesis: verum
end;
let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in rng F or w in PFuncs ((union (bool A)),(union (bool A))) )
assume w in rng F ; ::_thesis: w in PFuncs ((union (bool A)),(union (bool A)))
then consider w1 being set such that
A14: w1 in dom F and
A15: w = F . w1 by FUNCT_1:def_3;
reconsider w9 = w as Function of ( the Sorts of M . w1),( the Sorts of N . w1) by A14, A15, PBOOLE:def_15;
A16: dom the Sorts of M = the carrier of S by PARTFUN1:def_2;
A17: dom w9 c= union (bool A)
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in dom w9 or s in union (bool A) )
assume A18: s in dom w9 ; ::_thesis: s in union (bool A)
the Sorts of M . w1 in rng the Sorts of M by A14, A16, FUNCT_1:def_3;
hence s in union (bool A) by A13, A18, TARSKI:def_4; ::_thesis: verum
end;
A19: rng the Sorts of N c= bool A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng the Sorts of N or x in bool A )
assume x in rng the Sorts of N ; ::_thesis: x in bool A
then reconsider x9 = x as Component of the Sorts of N ;
x9 c= A by A6;
hence x in bool A ; ::_thesis: verum
end;
A20: dom the Sorts of N = the carrier of S by PARTFUN1:def_2;
rng w9 c= union (bool A)
proof
let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in rng w9 or r in union (bool A) )
assume A21: r in rng w9 ; ::_thesis: r in union (bool A)
the Sorts of N . w1 in rng the Sorts of N by A14, A20, FUNCT_1:def_3;
hence r in union (bool A) by A19, A21, TARSKI:def_4; ::_thesis: verum
end;
hence w in PFuncs ((union (bool A)),(union (bool A))) by A17, PARTFUN1:def_3; ::_thesis: verum
end;
then F in Funcs ( the carrier of S,(PFuncs ((union (bool A)),(union (bool A))))) by A12, FUNCT_2:def_2;
hence x in X by A7, A11, A3, A5; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st
( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) ) ) & ( for x being set holds
( x in b2 iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st
( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) ) ) holds
b1 = b2
proof
let A1, A2 be set ; ::_thesis: ( ( for x being set holds
( x in A1 iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st
( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) ) ) & ( for x being set holds
( x in A2 iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st
( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) ) ) implies A1 = A2 )
assume A22: for x being set holds
( x in A1 iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st
( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) ) ; ::_thesis: ( ex x being set st
( ( x in A2 implies ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st
( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) ) implies ( ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st
( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) & not x in A2 ) ) or A1 = A2 )
assume A23: for x being set holds
( x in A2 iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st
( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) ) ; ::_thesis: A1 = A2
A24: A2 c= A1
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A2 or a in A1 )
assume a in A2 ; ::_thesis: a in A1
then ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st
( M = i & N = j & f = a & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) by A23;
hence a in A1 by A22; ::_thesis: verum
end;
A1 c= A2
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A1 or a in A2 )
assume a in A1 ; ::_thesis: a in A2
then ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st
( M = i & N = j & f = a & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) by A22;
hence a in A2 by A23; ::_thesis: verum
end;
hence A1 = A2 by A24, XBOOLE_0:def_10; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines MSAlg_morph MSINST_1:def_3_:_
for S being non empty non void ManySortedSign
for A being non empty set
for i, j being set st i in MSAlg_set (S,A) & j in MSAlg_set (S,A) holds
for b5 being set holds
( b5 = MSAlg_morph (S,A,i,j) iff for x being set holds
( x in b5 iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st
( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) ) );
definition
let S be non empty non void ManySortedSign ;
let A be non empty set ;
func MSAlgCat (S,A) -> non empty strict AltCatStr means :Def4: :: MSINST_1:def 4
( the carrier of it = MSAlg_set (S,A) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of it . (i,j) = MSAlg_morph (S,A,i,j) ) & ( for i, j, k being object of it
for f, g being Function-yielding Function st f in the Arrows of it . (i,j) & g in the Arrows of it . (j,k) holds
( the Comp of it . (i,j,k)) . (g,f) = g ** f ) );
existence
ex b1 being non empty strict AltCatStr st
( the carrier of b1 = MSAlg_set (S,A) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of b1 . (i,j) = MSAlg_morph (S,A,i,j) ) & ( for i, j, k being object of b1
for f, g being Function-yielding Function st f in the Arrows of b1 . (i,j) & g in the Arrows of b1 . (j,k) holds
( the Comp of b1 . (i,j,k)) . (g,f) = g ** f ) )
proof
set c = MSAlg_set (S,A);
deffunc H1( Element of MSAlg_set (S,A), Element of MSAlg_set (S,A)) -> set = MSAlg_morph (S,A,$1,$2);
consider M being ManySortedSet of [:(MSAlg_set (S,A)),(MSAlg_set (S,A)):] such that
A1: for i, j being Element of MSAlg_set (S,A) holds M . (i,j) = H1(i,j) from ALTCAT_1:sch_2();
defpred S1[ set , set , set ] means ex i, j, k being Element of MSAlg_set (S,A) st
( $3 = [i,j,k] & ( for f, g being Function-yielding Function st f in M . (i,j) & g in M . (j,k) & $2 = [g,f] holds
$1 = g ** f ) );
A2: for ijk being set st ijk in [:(MSAlg_set (S,A)),(MSAlg_set (S,A)),(MSAlg_set (S,A)):] holds
for x being set st x in {|M,M|} . ijk holds
ex y being set st
( y in {|M|} . ijk & S1[y,x,ijk] )
proof
let ijk be set ; ::_thesis: ( ijk in [:(MSAlg_set (S,A)),(MSAlg_set (S,A)),(MSAlg_set (S,A)):] implies for x being set st x in {|M,M|} . ijk holds
ex y being set st
( y in {|M|} . ijk & S1[y,x,ijk] ) )
assume ijk in [:(MSAlg_set (S,A)),(MSAlg_set (S,A)),(MSAlg_set (S,A)):] ; ::_thesis: for x being set st x in {|M,M|} . ijk holds
ex y being set st
( y in {|M|} . ijk & S1[y,x,ijk] )
then consider x1, x2, x3 being set such that
A3: ( x1 in MSAlg_set (S,A) & x2 in MSAlg_set (S,A) & x3 in MSAlg_set (S,A) ) and
A4: ijk = [x1,x2,x3] by MCART_1:68;
reconsider x1 = x1, x2 = x2, x3 = x3 as Element of MSAlg_set (S,A) by A3;
let x be set ; ::_thesis: ( x in {|M,M|} . ijk implies ex y being set 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 set 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 MSAlg_morph (S,A,x2,x3) by A1;
then consider M2, N2 being strict feasible MSAlgebra over S, g being ManySortedFunction of M2,N2 such that
A8: M2 = x2 and
A9: N2 = x3 and
A10: g = x `1 and
A11: ( the Sorts of M2 is_transformable_to the Sorts of N2 & g is_homomorphism M2,N2 ) by Def3;
x `2 in M . (x1,x2) by A4, A7, A5, MCART_1:10;
then x `2 in MSAlg_morph (S,A,x1,x2) by A1;
then consider M1, N1 being strict feasible MSAlgebra over S, f being ManySortedFunction of M1,N1 such that
A12: M1 = x1 and
A13: N1 = x2 and
A14: f = x `2 and
A15: ( the Sorts of M1 is_transformable_to the Sorts of N1 & f is_homomorphism M1,N1 ) by Def3;
take y = g ** f; ::_thesis: ( y in {|M|} . ijk & S1[y,x,ijk] )
reconsider f = f as ManySortedFunction of M1,M2 by A8, A13;
( the Sorts of M1 is_transformable_to the Sorts of N2 & ex fg being ManySortedFunction of M1,N2 st
( fg = g ** f & fg is_homomorphism M1,N2 ) ) by A8, A11, A13, A15, Th5, AUTALG_1:10;
then ( {|M|} . (x1,x2,x3) = M . (x1,x3) & y in MSAlg_morph (S,A,x1,x3) ) by A9, A12, Def3, ALTCAT_1:def_3;
hence y in {|M|} . ijk by A1, A6; ::_thesis: S1[y,x,ijk]
take x1 ; ::_thesis: ex j, k being Element of MSAlg_set (S,A) st
( ijk = [x1,j,k] & ( for f, g being Function-yielding Function st f in M . (x1,j) & g in M . (j,k) & x = [g,f] holds
y = g ** f ) )
take x2 ; ::_thesis: ex k being Element of MSAlg_set (S,A) st
( ijk = [x1,x2,k] & ( for f, g being Function-yielding Function st f in M . (x1,x2) & g in M . (x2,k) & x = [g,f] holds
y = g ** f ) )
take x3 ; ::_thesis: ( ijk = [x1,x2,x3] & ( for f, g being Function-yielding Function st f in M . (x1,x2) & g in M . (x2,x3) & x = [g,f] holds
y = g ** f ) )
thus ijk = [x1,x2,x3] by A4; ::_thesis: for f, g being Function-yielding Function st f in M . (x1,x2) & g in M . (x2,x3) & x = [g,f] holds
y = g ** f
let F, G be Function-yielding Function; ::_thesis: ( F in M . (x1,x2) & G in M . (x2,x3) & x = [G,F] implies y = G ** F )
assume that
F in M . (x1,x2) and
G in M . (x2,x3) and
A16: x = [G,F] ; ::_thesis: y = G ** F
x `1 = G by A16, MCART_1:7;
hence y = G ** F by A10, A14, A16, MCART_1:7; ::_thesis: verum
end;
consider F being ManySortedFunction of {|M,M|},{|M|} such that
A17: for ijk being set st ijk in [:(MSAlg_set (S,A)),(MSAlg_set (S,A)),(MSAlg_set (S,A)):] holds
ex f being Function of ({|M,M|} . ijk),({|M|} . ijk) st
( f = F . ijk & ( for x being set st x in {|M,M|} . ijk holds
S1[f . x,x,ijk] ) ) from MSSUBFAM:sch_1(A2);
take EX = AltCatStr(# (MSAlg_set (S,A)),M,F #); ::_thesis: ( the carrier of EX = MSAlg_set (S,A) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of EX . (i,j) = MSAlg_morph (S,A,i,j) ) & ( for i, j, k being object of EX
for f, g being Function-yielding Function st f in the Arrows of EX . (i,j) & g in the Arrows of EX . (j,k) holds
( the Comp of EX . (i,j,k)) . (g,f) = g ** f ) )
reconsider EX = EX as non empty AltCatStr ;
for i, j, k being object of EX
for f, g being Function-yielding Function st f in the Arrows of EX . (i,j) & g in the Arrows of EX . (j,k) holds
( the Comp of EX . (i,j,k)) . (g,f) = g ** f
proof
let i, j, k be object of EX; ::_thesis: for f, g being Function-yielding Function st f in the Arrows of EX . (i,j) & g in the Arrows of EX . (j,k) holds
( the Comp of EX . (i,j,k)) . (g,f) = g ** f
let f, g be Function-yielding Function; ::_thesis: ( f in the Arrows of EX . (i,j) & g in the Arrows of EX . (j,k) implies ( the Comp of EX . (i,j,k)) . (g,f) = g ** f )
assume A18: ( f in the Arrows of EX . (i,j) & g in the Arrows of EX . (j,k) ) ; ::_thesis: ( the Comp of EX . (i,j,k)) . (g,f) = g ** f
set x = [g,f];
set ijk = [i,j,k];
[i,j,k] in [:(MSAlg_set (S,A)),(MSAlg_set (S,A)),(MSAlg_set (S,A)):] by MCART_1:69;
then consider ff being Function of ({|M,M|} . [i,j,k]),({|M|} . [i,j,k]) such that
A19: ff = F . [i,j,k] and
A20: for x being set st x in {|M,M|} . [i,j,k] holds
S1[ff . x,x,[i,j,k]] by A17;
A21: ff = the Comp of EX . (i,j,k) by A19, 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 [g,f] in {|M,M|} . [i,j,k] by A18, ZFMISC_1:87;
then consider I, J, K being Element of MSAlg_set (S,A) such that
A22: [i,j,k] = [I,J,K] and
A23: for f, g being Function-yielding Function st f in M . (I,J) & g in M . (J,K) & [g,f] = [g,f] holds
ff . [g,f] = g ** f by A20;
A24: K = k by A22, XTUPLE_0:3;
( I = i & J = j ) by A22, XTUPLE_0:3;
hence ( the Comp of EX . (i,j,k)) . (g,f) = g ** f by A18, A23, A24, A21; ::_thesis: verum
end;
hence ( the carrier of EX = MSAlg_set (S,A) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of EX . (i,j) = MSAlg_morph (S,A,i,j) ) & ( for i, j, k being object of EX
for f, g being Function-yielding Function st f in the Arrows of EX . (i,j) & g in the Arrows of EX . (j,k) holds
( the Comp of EX . (i,j,k)) . (g,f) = g ** f ) ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being non empty strict AltCatStr st the carrier of b1 = MSAlg_set (S,A) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of b1 . (i,j) = MSAlg_morph (S,A,i,j) ) & ( for i, j, k being object of b1
for f, g being Function-yielding Function st f in the Arrows of b1 . (i,j) & g in the Arrows of b1 . (j,k) holds
( the Comp of b1 . (i,j,k)) . (g,f) = g ** f ) & the carrier of b2 = MSAlg_set (S,A) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of b2 . (i,j) = MSAlg_morph (S,A,i,j) ) & ( for i, j, k being object of b2
for f, g being Function-yielding Function st f in the Arrows of b2 . (i,j) & g in the Arrows of b2 . (j,k) holds
( the Comp of b2 . (i,j,k)) . (g,f) = g ** f ) holds
b1 = b2
proof
reconsider c = MSAlg_set (S,A) as non empty set ;
let A1, A2 be non empty strict AltCatStr ; ::_thesis: ( the carrier of A1 = MSAlg_set (S,A) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of A1 . (i,j) = MSAlg_morph (S,A,i,j) ) & ( for i, j, k being object of A1
for f, g being Function-yielding Function st f in the Arrows of A1 . (i,j) & g in the Arrows of A1 . (j,k) holds
( the Comp of A1 . (i,j,k)) . (g,f) = g ** f ) & the carrier of A2 = MSAlg_set (S,A) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of A2 . (i,j) = MSAlg_morph (S,A,i,j) ) & ( for i, j, k being object of A2
for f, g being Function-yielding Function st f in the Arrows of A2 . (i,j) & g in the Arrows of A2 . (j,k) holds
( the Comp of A2 . (i,j,k)) . (g,f) = g ** f ) implies A1 = A2 )
assume that
A25: the carrier of A1 = MSAlg_set (S,A) and
A26: for i, j being Element of MSAlg_set (S,A) holds the Arrows of A1 . (i,j) = MSAlg_morph (S,A,i,j) and
A27: for i, j, k being object of A1
for f, g being Function-yielding Function st f in the Arrows of A1 . (i,j) & g in the Arrows of A1 . (j,k) holds
( the Comp of A1 . (i,j,k)) . (g,f) = g ** f and
A28: the carrier of A2 = MSAlg_set (S,A) and
A29: for i, j being Element of MSAlg_set (S,A) holds the Arrows of A2 . (i,j) = MSAlg_morph (S,A,i,j) and
A30: for i, j, k being object of A2
for f, g being Function-yielding Function st f in the Arrows of A2 . (i,j) & g in the Arrows of A2 . (j,k) holds
( the Comp of A2 . (i,j,k)) . (g,f) = g ** f ; ::_thesis: A1 = A2
reconsider CC1 = the Comp of A1, CC2 = the Comp of A2 as ManySortedSet of [:c,c,c:] by A25, A28;
reconsider AA1 = the Arrows of A1, AA2 = the Arrows of A2 as ManySortedSet of [:c,c:] by A25, A28;
A31: now__::_thesis:_for_i,_j_being_Element_of_c_holds_AA1_._(i,j)_=_AA2_._(i,j)
let i, j be Element of c; ::_thesis: AA1 . (i,j) = AA2 . (i,j)
thus AA1 . (i,j) = MSAlg_morph (S,A,i,j) by A26
.= AA2 . (i,j) by A29 ; ::_thesis: verum
end;
then A32: AA1 = AA2 by ALTCAT_1:7;
now__::_thesis:_for_i,_j,_k_being_set_st_i_in_c_&_j_in_c_&_k_in_c_holds_
CC1_._(i,j,k)_=_CC2_._(i,j,k)
let i, j, k be set ; ::_thesis: ( i in c & j in c & k in c implies CC1 . (i,j,k) = CC2 . (i,j,k) )
set ijk = [i,j,k];
A33: CC1 . (i,j,k) = CC1 . [i,j,k] by MULTOP_1:def_1;
assume A34: ( i in c & j in c & k in c ) ; ::_thesis: CC1 . (i,j,k) = CC2 . (i,j,k)
then reconsider i9 = i, j9 = j, k9 = k as Element of c ;
reconsider I9 = i, J9 = j, K9 = k as object of A2 by A28, A34;
reconsider I = i, J = j, K = k as object of A1 by A25, A34;
A35: [i,j,k] in [:c,c,c:] by A34, MCART_1:69;
A36: CC2 . (i,j,k) = CC2 . [i,j,k] by MULTOP_1:def_1;
thus CC1 . (i,j,k) = CC2 . (i,j,k) ::_thesis: verum
proof
reconsider Cj = CC2 . [i,j,k] as Function of ({|AA2,AA2|} . [i,j,k]),({|AA2|} . [i,j,k]) by A28, A35, PBOOLE:def_15;
reconsider Ci = CC1 . [i,j,k] as Function of ({|AA1,AA1|} . [i,j,k]),({|AA1|} . [i,j,k]) by A25, A35, PBOOLE:def_15;
percases ( {|AA1|} . [i,j,k] <> {} or {|AA1|} . [i,j,k] = {} ) ;
supposeA37: {|AA1|} . [i,j,k] <> {} ; ::_thesis: CC1 . (i,j,k) = CC2 . (i,j,k)
A38: for x being set st x in {|AA1,AA1|} . [i,j,k] holds
Ci . x = Cj . x
proof
let x be set ; ::_thesis: ( x in {|AA1,AA1|} . [i,j,k] implies Ci . x = Cj . x )
assume A39: x in {|AA1,AA1|} . [i,j,k] ; ::_thesis: Ci . x = Cj . x
then x in {|AA1,AA1|} . (i,j,k) by MULTOP_1:def_1;
then A40: x in [:(AA1 . (j,k)),(AA1 . (i,j)):] by A34, ALTCAT_1:def_4;
then A41: x `1 in AA1 . (j,k) by MCART_1:10;
then x `1 in MSAlg_morph (S,A,j9,k9) by A26;
then consider M2, N2 being strict feasible MSAlgebra over S, g being ManySortedFunction of M2,N2 such that
M2 = j9 and
N2 = k9 and
A42: g = x `1 and
the Sorts of M2 is_transformable_to the Sorts of N2 and
g is_homomorphism M2,N2 by Def3;
x in {|AA2,AA2|} . (i,j,k) by A32, A39, MULTOP_1:def_1;
then x in [:(AA2 . (j,k)),(AA2 . (i,j)):] by A34, ALTCAT_1:def_4;
then A43: ( x `1 in AA2 . (j,k) & x `2 in AA2 . (i,j) ) by MCART_1:10;
A44: x `2 in AA1 . (i,j) by A40, MCART_1:10;
then x `2 in MSAlg_morph (S,A,i9,j9) by A26;
then consider M1, N1 being strict feasible MSAlgebra over S, f being ManySortedFunction of M1,N1 such that
M1 = i9 and
N1 = j9 and
A45: f = x `2 and
the Sorts of M1 is_transformable_to the Sorts of N1 and
f is_homomorphism M1,N1 by Def3;
A46: x = [g,f] by A40, A45, A42, MCART_1:21;
then Ci . x = ( the Comp of A1 . (I,J,K)) . (g,f) by MULTOP_1:def_1
.= g ** f by A27, A41, A44, A45, A42
.= ( the Comp of A2 . (I9,J9,K9)) . (g,f) by A30, A43, A45, A42
.= Cj . x by A46, MULTOP_1:def_1 ;
hence Ci . x = Cj . x ; ::_thesis: verum
end;
{|AA2|} . [i,j,k] <> {} by A31, A37, ALTCAT_1:7;
then A47: dom Cj = {|AA2,AA2|} . [i,j,k] by FUNCT_2:def_1;
dom Ci = {|AA1,AA1|} . [i,j,k] by A37, FUNCT_2:def_1;
hence CC1 . (i,j,k) = CC2 . (i,j,k) by A32, A33, A36, A47, A38, FUNCT_1:2; ::_thesis: verum
end;
suppose {|AA1|} . [i,j,k] = {} ; ::_thesis: CC1 . (i,j,k) = CC2 . (i,j,k)
then ( Ci = {} & Cj = {} ) by A32;
hence CC1 . (i,j,k) = CC2 . (i,j,k) by A33, MULTOP_1:def_1; ::_thesis: verum
end;
end;
end;
end;
hence A1 = A2 by A25, A28, A32, ALTCAT_1:8; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines MSAlgCat MSINST_1:def_4_:_
for S being non empty non void ManySortedSign
for A being non empty set
for b3 being non empty strict AltCatStr holds
( b3 = MSAlgCat (S,A) iff ( the carrier of b3 = MSAlg_set (S,A) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of b3 . (i,j) = MSAlg_morph (S,A,i,j) ) & ( for i, j, k being object of b3
for f, g being Function-yielding Function st f in the Arrows of b3 . (i,j) & g in the Arrows of b3 . (j,k) holds
( the Comp of b3 . (i,j,k)) . (g,f) = g ** f ) ) );
registration
let S be non empty non void ManySortedSign ;
let A be non empty set ;
cluster MSAlgCat (S,A) -> non empty transitive strict associative with_units ;
coherence
( MSAlgCat (S,A) is transitive & MSAlgCat (S,A) is associative & MSAlgCat (S,A) is with_units )
proof
set M = MSAlgCat (S,A);
set G = MSAlgCat (S,A);
set GM = the Arrows of (MSAlgCat (S,A));
set C = the Comp of (MSAlgCat (S,A));
thus MSAlgCat (S,A) is transitive ::_thesis: ( MSAlgCat (S,A) is associative & MSAlgCat (S,A) is with_units )
proof
let o1, o2, o3 be object of (MSAlgCat (S,A)); :: according to ALTCAT_1:def_2 ::_thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or not <^o1,o3^> = {} )
reconsider o19 = o1, o29 = o2, o39 = o3 as Element of MSAlg_set (S,A) by Def4;
assume that
A1: <^o1,o2^> <> {} and
A2: <^o2,o3^> <> {} ; ::_thesis: not <^o1,o3^> = {}
set t = the Element of MSAlg_morph (S,A,o19,o29);
MSAlg_morph (S,A,o19,o29) <> {} by A1, Def4;
then consider M, N being strict feasible MSAlgebra over S, f being ManySortedFunction of M,N such that
A3: M = o19 and
A4: N = o29 and
f = the Element of MSAlg_morph (S,A,o19,o29) and
A5: the Sorts of M is_transformable_to the Sorts of N and
A6: f is_homomorphism M,N by Def3;
set s = the Element of MSAlg_morph (S,A,o29,o39);
MSAlg_morph (S,A,o29,o39) <> {} by A2, Def4;
then consider M1, N1 being strict feasible MSAlgebra over S, g being ManySortedFunction of M1,N1 such that
A7: M1 = o29 and
A8: N1 = o39 and
g = the Element of MSAlg_morph (S,A,o29,o39) and
A9: the Sorts of M1 is_transformable_to the Sorts of N1 and
A10: g is_homomorphism M1,N1 by Def3;
reconsider g9 = g as ManySortedFunction of N,N1 by A4, A7;
consider GF being ManySortedFunction of M,N1 such that
GF = g9 ** f and
A11: GF is_homomorphism M,N1 by A4, A5, A6, A7, A9, A10, Th5;
the Sorts of M is_transformable_to the Sorts of N1 by A4, A5, A7, A9, AUTALG_1:10;
then GF in MSAlg_morph (S,A,o19,o39) by A3, A8, A11, Def3;
hence not <^o1,o3^> = {} by Def4; ::_thesis: verum
end;
thus the Comp of (MSAlgCat (S,A)) is associative :: according to ALTCAT_1:def_15 ::_thesis: MSAlgCat (S,A) is with_units
proof
let i, j, k, l be Element of (MSAlgCat (S,A)); :: according to ALTCAT_1:def_5 ::_thesis: for b1, b2, b3 being set holds
( not b1 in the Arrows of (MSAlgCat (S,A)) . (i,j) or not b2 in the Arrows of (MSAlgCat (S,A)) . (j,k) or not b3 in the Arrows of (MSAlgCat (S,A)) . (k,l) or ( the Comp of (MSAlgCat (S,A)) . (i,k,l)) . (b3,(( the Comp of (MSAlgCat (S,A)) . (i,j,k)) . (b2,b1))) = ( the Comp of (MSAlgCat (S,A)) . (i,j,l)) . ((( the Comp of (MSAlgCat (S,A)) . (j,k,l)) . (b3,b2)),b1) )
let f, g, h be set ; ::_thesis: ( not f in the Arrows of (MSAlgCat (S,A)) . (i,j) or not g in the Arrows of (MSAlgCat (S,A)) . (j,k) or not h in the Arrows of (MSAlgCat (S,A)) . (k,l) or ( the Comp of (MSAlgCat (S,A)) . (i,k,l)) . (h,(( the Comp of (MSAlgCat (S,A)) . (i,j,k)) . (g,f))) = ( the Comp of (MSAlgCat (S,A)) . (i,j,l)) . ((( the Comp of (MSAlgCat (S,A)) . (j,k,l)) . (h,g)),f) )
reconsider i9 = i, j9 = j, k9 = k, l9 = l as Element of MSAlg_set (S,A) by Def4;
assume that
A12: f in the Arrows of (MSAlgCat (S,A)) . (i,j) and
A13: g in the Arrows of (MSAlgCat (S,A)) . (j,k) and
A14: h in the Arrows of (MSAlgCat (S,A)) . (k,l) ; ::_thesis: ( the Comp of (MSAlgCat (S,A)) . (i,k,l)) . (h,(( the Comp of (MSAlgCat (S,A)) . (i,j,k)) . (g,f))) = ( the Comp of (MSAlgCat (S,A)) . (i,j,l)) . ((( the Comp of (MSAlgCat (S,A)) . (j,k,l)) . (h,g)),f)
g in MSAlg_morph (S,A,j9,k9) by A13, Def4;
then consider M2, N2 being strict feasible MSAlgebra over S, G being ManySortedFunction of M2,N2 such that
A15: M2 = j9 and
A16: N2 = k9 and
A17: g = G and
A18: the Sorts of M2 is_transformable_to the Sorts of N2 and
A19: G is_homomorphism M2,N2 by Def3;
h in MSAlg_morph (S,A,k9,l9) by A14, Def4;
then consider M3, N3 being strict feasible MSAlgebra over S, H being ManySortedFunction of M3,N3 such that
A20: M3 = k9 and
A21: N3 = l9 and
A22: h = H and
A23: the Sorts of M3 is_transformable_to the Sorts of N3 and
A24: H is_homomorphism M3,N3 by Def3;
reconsider G9 = G as ManySortedFunction of M2,M3 by A16, A20;
consider HG being ManySortedFunction of M2,N3 such that
A25: HG = H ** G9 and
A26: HG is_homomorphism M2,N3 by A16, A18, A19, A20, A23, A24, Th5;
A27: ( the Comp of (MSAlgCat (S,A)) . (j,k,l)) . (H,G) = H ** G9 by A13, A14, A17, A22, Def4;
f in MSAlg_morph (S,A,i9,j9) by A12, Def4;
then consider M1, N1 being strict feasible MSAlgebra over S, F being ManySortedFunction of M1,N1 such that
A28: M1 = i9 and
A29: N1 = j9 and
A30: f = F and
A31: the Sorts of M1 is_transformable_to the Sorts of N1 and
A32: F is_homomorphism M1,N1 by Def3;
A33: ( the Comp of (MSAlgCat (S,A)) . (i,j,k)) . (g,f) = G ** F by A12, A13, A30, A17, Def4;
consider GF being ManySortedFunction of M1,M3 such that
A34: GF = G9 ** F and
A35: GF is_homomorphism M1,M3 by A29, A31, A32, A15, A16, A18, A19, A20, Th5;
the Sorts of M1 is_transformable_to the Sorts of M3 by A29, A31, A15, A16, A18, A20, AUTALG_1:10;
then G9 ** F in MSAlg_morph (S,A,i9,k9) by A28, A20, A34, A35, Def3;
then GF in the Arrows of (MSAlgCat (S,A)) . (i,k) by A34, Def4;
then A36: ( the Comp of (MSAlgCat (S,A)) . (i,k,l)) . (H,GF) = H ** GF by A14, A22, Def4;
the Sorts of M2 is_transformable_to the Sorts of N3 by A16, A18, A20, A23, AUTALG_1:10;
then HG in MSAlg_morph (S,A,j9,l9) by A15, A21, A26, Def3;
then A37: H ** G9 in the Arrows of (MSAlgCat (S,A)) . (j,l) by A25, Def4;
(H ** G9) ** F = H ** (G9 ** F) by PBOOLE:140;
hence ( the Comp of (MSAlgCat (S,A)) . (i,k,l)) . (h,(( the Comp of (MSAlgCat (S,A)) . (i,j,k)) . (g,f))) = ( the Comp of (MSAlgCat (S,A)) . (i,j,l)) . ((( the Comp of (MSAlgCat (S,A)) . (j,k,l)) . (h,g)),f) by A12, A30, A17, A22, A33, A34, A36, A27, A37, Def4; ::_thesis: verum
end;
thus the Comp of (MSAlgCat (S,A)) is with_left_units :: according to ALTCAT_1:def_16 ::_thesis: the Comp of (MSAlgCat (S,A)) is with_right_units
proof
let j be Element of (MSAlgCat (S,A)); :: according to ALTCAT_1:def_7 ::_thesis: ex b1 being set st
( b1 in the Arrows of (MSAlgCat (S,A)) . (j,j) & ( for b2 being Element of the carrier of (MSAlgCat (S,A))
for b3 being set holds
( not b3 in the Arrows of (MSAlgCat (S,A)) . (b2,j) or ( the Comp of (MSAlgCat (S,A)) . (b2,j,j)) . (b1,b3) = b3 ) ) )
reconsider j9 = j as Element of MSAlg_set (S,A) by Def4;
consider MS being strict feasible MSAlgebra over S such that
A38: MS = j9 and
for C being Component of the Sorts of MS holds C c= A by Def2;
reconsider e = id the Sorts of MS as ManySortedFunction of MS,MS ;
take e ; ::_thesis: ( e in the Arrows of (MSAlgCat (S,A)) . (j,j) & ( for b1 being Element of the carrier of (MSAlgCat (S,A))
for b2 being set holds
( not b2 in the Arrows of (MSAlgCat (S,A)) . (b1,j) or ( the Comp of (MSAlgCat (S,A)) . (b1,j,j)) . (e,b2) = b2 ) ) )
( e is_homomorphism MS,MS & the Arrows of (MSAlgCat (S,A)) . (j,j) = MSAlg_morph (S,A,j9,j9) ) by Def4, MSUALG_3:9;
hence A39: e in the Arrows of (MSAlgCat (S,A)) . (j,j) by A38, Def3; ::_thesis: for b1 being Element of the carrier of (MSAlgCat (S,A))
for b2 being set holds
( not b2 in the Arrows of (MSAlgCat (S,A)) . (b1,j) or ( the Comp of (MSAlgCat (S,A)) . (b1,j,j)) . (e,b2) = b2 )
let i be Element of (MSAlgCat (S,A)); ::_thesis: for b1 being set holds
( not b1 in the Arrows of (MSAlgCat (S,A)) . (i,j) or ( the Comp of (MSAlgCat (S,A)) . (i,j,j)) . (e,b1) = b1 )
reconsider i9 = i as Element of MSAlg_set (S,A) by Def4;
let f be set ; ::_thesis: ( not f in the Arrows of (MSAlgCat (S,A)) . (i,j) or ( the Comp of (MSAlgCat (S,A)) . (i,j,j)) . (e,f) = f )
reconsider I = i, J = j as object of (MSAlgCat (S,A)) ;
assume A40: f in the Arrows of (MSAlgCat (S,A)) . (i,j) ; ::_thesis: ( the Comp of (MSAlgCat (S,A)) . (i,j,j)) . (e,f) = f
then f in MSAlg_morph (S,A,i9,j9) by Def4;
then consider M1, N1 being strict feasible MSAlgebra over S, F being ManySortedFunction of M1,N1 such that
M1 = i9 and
A41: N1 = j9 and
A42: F = f and
the Sorts of M1 is_transformable_to the Sorts of N1 and
F is_homomorphism M1,N1 by Def3;
reconsider F = F as ManySortedFunction of M1,MS by A38, A41;
( the Comp of (MSAlgCat (S,A)) . (I,J,J)) . (e,f) = e ** F by A39, A40, A42, Def4;
hence ( the Comp of (MSAlgCat (S,A)) . (i,j,j)) . (e,f) = f by A42, MSUALG_3:4; ::_thesis: verum
end;
thus the Comp of (MSAlgCat (S,A)) is with_right_units ::_thesis: verum
proof
let i be Element of (MSAlgCat (S,A)); :: according to ALTCAT_1:def_6 ::_thesis: ex b1 being set st
( b1 in the Arrows of (MSAlgCat (S,A)) . (i,i) & ( for b2 being Element of the carrier of (MSAlgCat (S,A))
for b3 being set holds
( not b3 in the Arrows of (MSAlgCat (S,A)) . (i,b2) or ( the Comp of (MSAlgCat (S,A)) . (i,i,b2)) . (b3,b1) = b3 ) ) )
reconsider i9 = i as Element of MSAlg_set (S,A) by Def4;
consider MS being strict feasible MSAlgebra over S such that
A43: MS = i9 and
for C being Component of the Sorts of MS holds C c= A by Def2;
reconsider e = id the Sorts of MS as ManySortedFunction of MS,MS ;
take e ; ::_thesis: ( e in the Arrows of (MSAlgCat (S,A)) . (i,i) & ( for b1 being Element of the carrier of (MSAlgCat (S,A))
for b2 being set holds
( not b2 in the Arrows of (MSAlgCat (S,A)) . (i,b1) or ( the Comp of (MSAlgCat (S,A)) . (i,i,b1)) . (b2,e) = b2 ) ) )
( e is_homomorphism MS,MS & the Arrows of (MSAlgCat (S,A)) . (i,i) = MSAlg_morph (S,A,i9,i9) ) by Def4, MSUALG_3:9;
hence A44: e in the Arrows of (MSAlgCat (S,A)) . (i,i) by A43, Def3; ::_thesis: for b1 being Element of the carrier of (MSAlgCat (S,A))
for b2 being set holds
( not b2 in the Arrows of (MSAlgCat (S,A)) . (i,b1) or ( the Comp of (MSAlgCat (S,A)) . (i,i,b1)) . (b2,e) = b2 )
let j be Element of (MSAlgCat (S,A)); ::_thesis: for b1 being set holds
( not b1 in the Arrows of (MSAlgCat (S,A)) . (i,j) or ( the Comp of (MSAlgCat (S,A)) . (i,i,j)) . (b1,e) = b1 )
reconsider j9 = j as Element of MSAlg_set (S,A) by Def4;
let f be set ; ::_thesis: ( not f in the Arrows of (MSAlgCat (S,A)) . (i,j) or ( the Comp of (MSAlgCat (S,A)) . (i,i,j)) . (f,e) = f )
reconsider I = i, J = j as object of (MSAlgCat (S,A)) ;
assume A45: f in the Arrows of (MSAlgCat (S,A)) . (i,j) ; ::_thesis: ( the Comp of (MSAlgCat (S,A)) . (i,i,j)) . (f,e) = f
then f in MSAlg_morph (S,A,i9,j9) by Def4;
then consider M1, N1 being strict feasible MSAlgebra over S, F being ManySortedFunction of M1,N1 such that
A46: M1 = i9 and
N1 = j9 and
A47: F = f and
the Sorts of M1 is_transformable_to the Sorts of N1 and
F is_homomorphism M1,N1 by Def3;
reconsider F = F as ManySortedFunction of MS,N1 by A43, A46;
( the Comp of (MSAlgCat (S,A)) . (I,I,J)) . (f,e) = F ** e by A44, A45, A47, Def4;
hence ( the Comp of (MSAlgCat (S,A)) . (i,i,j)) . (f,e) = f by A47, MSUALG_3:3; ::_thesis: verum
end;
end;
end;
theorem :: MSINST_1:6
for A being non empty set
for S being non empty non void ManySortedSign
for C being category st C = MSAlgCat (S,A) holds
for o being object of C holds o is strict feasible MSAlgebra over S
proof
let A be non empty set ; ::_thesis: for S being non empty non void ManySortedSign
for C being category st C = MSAlgCat (S,A) holds
for o being object of C holds o is strict feasible MSAlgebra over S
let S be non empty non void ManySortedSign ; ::_thesis: for C being category st C = MSAlgCat (S,A) holds
for o being object of C holds o is strict feasible MSAlgebra over S
let C be category; ::_thesis: ( C = MSAlgCat (S,A) implies for o being object of C holds o is strict feasible MSAlgebra over S )
assume A1: C = MSAlgCat (S,A) ; ::_thesis: for o being object of C holds o is strict feasible MSAlgebra over S
let o be object of C; ::_thesis: o is strict feasible MSAlgebra over S
o in the carrier of C ;
then o in MSAlg_set (S,A) by A1, Def4;
then ex M being strict feasible MSAlgebra over S st
( o = M & ( for C1 being Component of the Sorts of M holds C1 c= A ) ) by Def2;
hence o is strict feasible MSAlgebra over S ; ::_thesis: verum
end;