environ
vocabularies HIDDEN, FUNCT_1, RELAT_1, XBOOLE_0, TARSKI, FUNCT_4, PARTFUN1, SUBSET_1, PBOOLE, STRUCT_0, MSUALG_1, MARGREL1, CATALG_1, PUA2MSS1, TREES_1, FINSEQ_1, INSTALG1, FUNCSDOM, MSUALG_6, PROB_2, CARD_3, ALGSPEC1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, MSAFREE1, FINSEQ_1, PBOOLE, RELSET_1, PARTFUN1, FINSEQ_2, FUNCT_4, LANG1, FUNCT_2, STRUCT_0, CARD_3, MSUALG_1, PROB_2, PUA2MSS1, CIRCCOMB, MSUALG_6, INSTALG1, CATALG_1;
definitions TARSKI, FUNCT_1, PARTFUN1, STRUCT_0, CIRCCOMB, PUA2MSS1, INSTALG1, XBOOLE_0, FUNCT_2;
theorems RELAT_1, FUNCT_1, FUNCT_2, FUNCT_3, FUNCT_4, PARTFUN1, GRFUNC_1, FINSEQ_1, PBOOLE, LANG1, PUA2MSS1, FRECHET, INSTALG1, FUNCT_7, CIRCCOMB, RELSET_1, PROB_2, MSAFREE1, XBOOLE_0, XBOOLE_1, FINSEQ_2;
schemes FUNCT_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FUNCT_2, PBOOLE, STRUCT_0, MSUALG_1, MSUALG_2, CIRCCOMB, MSUALG_6, INSTALG1, CATALG_1, RELSET_1, FINSEQ_1, FUNCT_4;
constructors HIDDEN, MSAFREE1, CIRCCOMB, PUA2MSS1, MSUALG_6, CATALG_1, RELSET_1;
requirements HIDDEN, SUBSET, BOOLE;
equalities MSUALG_1;
expansions TARSKI, FUNCT_1, CIRCCOMB, PUA2MSS1, XBOOLE_0, FUNCT_2;
theorem Th49:
for
S1,
S2,
S being non
empty ManySortedSign for
f1,
g1,
f2,
g2 being
Function st
f1 tolerates f2 &
f1,
g1 form_morphism_between S1,
S &
f2,
g2 form_morphism_between S2,
S holds
f1 +* f2,
g1 +* g2 form_morphism_between S1 +* S2,
S