:: Extensions of Mappings on Generator Set :: by Artur Korni{\l}owicz :: :: Received March 23, 1995 :: Copyright (c) 1995-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies STRUCT_0, XBOOLE_0, MSUALG_1, RELAT_1, PBOOLE, MEMBER_1, TARSKI, REALSET1, FUNCT_1, PZFMISC1, MSUALG_3, FUNCT_6, MSAFREE, LANG1, MCART_1, TREES_4, SUBSET_1, FUNCOP_1, PRELAMB, MSUALG_2, UNIALG_2, MARGREL1, CARD_3, NAT_1, PARTFUN1; notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, RELSET_1, FUNCT_1, XTUPLE_0, MCART_1, PARTFUN1, FUNCOP_1, FUNCT_6, PZFMISC1, FINSEQ_2, STRUCT_0, LANG1, FUNCT_2, CARD_3, ORDINAL1, TREES_4, DTCONSTR, PBOOLE, MSUALG_1, MSUALG_2, MSUALG_3, MSAFREE; constructors PZFMISC1, MSUALG_3, MSAFREE, RELSET_1, XTUPLE_0; registrations FUNCT_1, RELSET_1, FUNCOP_1, PBOOLE, STRUCT_0, MSUALG_1, MSUALG_3, MSAFREE, MSSUBFAM, FINSEQ_1, XTUPLE_0; requirements SUBSET, BOOLE; begin :: Preliminaries reserve S for non void non empty ManySortedSign, U1, U2, U3 for non-empty MSAlgebra over S, I for set, A for ManySortedSet of I, B, C for non-empty ManySortedSet of I; begin :: Facts about Many Sorted Functions theorem :: EXTENS_1:1 for F be ManySortedFunction of A, B for X be ManySortedSubset of A st A c= X holds F || X = F; theorem :: EXTENS_1:2 for A, B be ManySortedSet of I for M be ManySortedSubset of A for F be ManySortedFunction of A, B holds F.:.:M c= F.:.:A; theorem :: EXTENS_1:3 for F be ManySortedFunction of A, B for M1, M2 be ManySortedSubset of A st M1 c= M2 holds (F||M2).:.:M1 = F.:.:M1; theorem :: EXTENS_1:4 for F be ManySortedFunction of A, B for G be ManySortedFunction of B, C for X be ManySortedSubset of A holds (G ** F) || X = G ** (F || X); theorem :: EXTENS_1:5 for A, B be ManySortedSet of I st A is_transformable_to B for F be ManySortedFunction of A, B for C be ManySortedSet of I st B is ManySortedSubset of C holds F is ManySortedFunction of A, C; theorem :: EXTENS_1:6 for F be ManySortedFunction of A, B for X be ManySortedSubset of A holds F is "1-1" implies F || X is "1-1"; begin :: doms & rngs of Many Sorted Function theorem :: EXTENS_1:7 for F be ManySortedFunction of A, B for X be ManySortedSubset of A holds doms (F || X) c= doms F; theorem :: EXTENS_1:8 for F be ManySortedFunction of A, B for X be ManySortedSubset of A holds rngs (F || X) c= rngs F; theorem :: EXTENS_1:9 for A, B be ManySortedSet of I for F be ManySortedFunction of A, B holds F is "onto" iff rngs F = B; theorem :: EXTENS_1:10 for X be non-empty ManySortedSet of the carrier of S holds rngs Reverse X = X ; theorem :: EXTENS_1:11 for F be ManySortedFunction of A, B for G be ManySortedFunction of B, C for X be non-empty ManySortedSubset of B st rngs F c= X holds (G || X) ** F = G ** F; begin :: Other properties of "onto" & "1-1" theorem :: EXTENS_1:12 for F be ManySortedFunction of A, B holds F is "onto" iff for C for G, H be ManySortedFunction of B, C st G**F = H**F holds G = H; theorem :: EXTENS_1:13 for F be ManySortedFunction of A, B st A is non-empty holds F is "1-1" iff for C be ManySortedSet of I for G, H be ManySortedFunction of C, A st F**G = F**H holds G = H; begin :: Extensions of Mappings on Generator Set theorem :: EXTENS_1:14 for X be non-empty ManySortedSet of the carrier of S for h1, h2 be ManySortedFunction of FreeMSA X, U1 st h1 is_homomorphism FreeMSA X, U1 & h2 is_homomorphism FreeMSA X, U1 & h1 || FreeGen (X) = h2 || FreeGen (X) holds h1 = h2; theorem :: EXTENS_1:15 for F be ManySortedFunction of U1, U2 st F is_epimorphism U1, U2 for U3 be non-empty MSAlgebra over S for h1, h2 be ManySortedFunction of U2, U3 st h1**F = h2**F holds h1 = h2; theorem :: EXTENS_1:16 for F be ManySortedFunction of U2, U3 st F is_homomorphism U2, U3 holds F is_monomorphism U2, U3 iff for U1 be non-empty MSAlgebra over S for h1, h2 be ManySortedFunction of U1, U2 st h1 is_homomorphism U1, U2 & h2 is_homomorphism U1, U2 holds (F**h1 = F**h2 implies h1 = h2); registration let S, U1; cluster non-empty for GeneratorSet of U1; end; theorem :: EXTENS_1:17 for U1 being MSAlgebra over S for A, B being MSSubset of U1 st A is ManySortedSubset of B holds GenMSAlg A is MSSubAlgebra of GenMSAlg B; theorem :: EXTENS_1:18 for U1 being MSAlgebra over S, U2 being MSSubAlgebra of U1 for B1 being MSSubset of U1, B2 being MSSubset of U2 st B1 = B2 holds GenMSAlg B1 = GenMSAlg B2; theorem :: EXTENS_1:19 for U1 being non-empty MSAlgebra over S for U2 being non-empty MSAlgebra over S for Gen being GeneratorSet of U1 for h1, h2 being ManySortedFunction of U1, U2 st h1 is_homomorphism U1, U2 & h2 is_homomorphism U1, U2 & h1 || Gen = h2 || Gen holds h1 = h2;