:: Extensions of Mappings on Generator Set
:: by Artur Korni{\l}owicz
::
:: Received March 23, 1995
:: Copyright (c) 1995-2012 Association of Mizar Users


begin

Lm1:  for I being set
for A, B, C being ManySortedSet of I
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C holds G ** F is ManySortedSet of I
proofend;

begin

theorem :: EXTENS_1:1
for I being set
for A being ManySortedSet of I
for B being V2() ManySortedSet of I
for F being ManySortedFunction of A,B
for X being ManySortedSubset of A st A c= X holds
F || X = F
proofend;

theorem :: EXTENS_1:2
for I being set
for A, B being ManySortedSet of I
for M being ManySortedSubset of A
for F being ManySortedFunction of A,B holds F .:.: M c= F .:.: A
proofend;

theorem :: EXTENS_1:3
for I being set
for A being ManySortedSet of I
for B being V2() ManySortedSet of I
for F being ManySortedFunction of A,B
for M1, M2 being ManySortedSubset of A st M1 c= M2 holds
(F || M2) .:.: M1 = F .:.: M1
proofend;

theorem Th4: :: EXTENS_1:4
for I being set
for A being ManySortedSet of I
for B, C being V2() ManySortedSet of I
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C
for X being ManySortedSubset of A holds (G ** F) || X = G ** (F || X)
proofend;

theorem :: EXTENS_1:5
for I being set
for A, B being ManySortedSet of I st A is_transformable_to B holds
for F being ManySortedFunction of A,B
for C being ManySortedSet of I st B is ManySortedSubset of C holds
F is ManySortedFunction of A,C
proofend;

theorem :: EXTENS_1:6
for I being set
for A being ManySortedSet of I
for B being V2() ManySortedSet of I
for F being ManySortedFunction of A,B
for X being ManySortedSubset of A st F is "1-1" holds
F || X is "1-1"
proofend;

begin

theorem :: EXTENS_1:7
for I being set
for A being ManySortedSet of I
for B being V2() ManySortedSet of I
for F being ManySortedFunction of A,B
for X being ManySortedSubset of A holds doms (F || X) c= doms F
proofend;

theorem :: EXTENS_1:8
for I being set
for A being ManySortedSet of I
for B being V2() ManySortedSet of I
for F being ManySortedFunction of A,B
for X being ManySortedSubset of A holds rngs (F || X) c= rngs F
proofend;

theorem :: EXTENS_1:9
for I being set
for A, B being ManySortedSet of I
for F being ManySortedFunction of A,B holds
( F is "onto" iff rngs F = B )
proofend;

theorem :: EXTENS_1:10
for S being non empty non void ManySortedSign
for X being V2() ManySortedSet of the carrier of S holds rngs (Reverse X) = X
proofend;

theorem :: EXTENS_1:11
for I being set
for A being ManySortedSet of I
for B, C being V2() ManySortedSet of I
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C
for X being V2() ManySortedSubset of B st rngs F c= X holds
(G || X) ** F = G ** F
proofend;

begin

theorem Th12: :: EXTENS_1:12
for I being set
for A being ManySortedSet of I
for B being V2() ManySortedSet of I
for F being ManySortedFunction of A,B holds
( F is "onto" iff for C being V2() ManySortedSet of I
for G, H being ManySortedFunction of B,C st G ** F = H ** F holds
G = H )
proofend;

theorem Th13: :: EXTENS_1:13
for I being set
for A being ManySortedSet of I
for B being V2() ManySortedSet of I
for F being ManySortedFunction of A,B st A is V2() holds
( F is "1-1" iff for C being ManySortedSet of I
for G, H being ManySortedFunction of C,A st F ** G = F ** H holds
G = H )
proofend;

begin

theorem Th14: :: EXTENS_1:14
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for X being V2() ManySortedSet of the carrier of S
for h1, h2 being 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
proofend;

theorem :: EXTENS_1:15
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 holds
for U3 being non-empty MSAlgebra over S
for h1, h2 being ManySortedFunction of U2,U3 st h1 ** F = h2 ** F holds
h1 = h2
proofend;

theorem :: EXTENS_1:16
for S being non empty non void ManySortedSign
for U2, U3 being non-empty MSAlgebra over S
for F being ManySortedFunction of U2,U3 st F is_homomorphism U2,U3 holds
( F is_monomorphism U2,U3 iff for U1 being non-empty MSAlgebra over S
for h1, h2 being ManySortedFunction of U1,U2 st h1 is_homomorphism U1,U2 & h2 is_homomorphism U1,U2 & F ** h1 = F ** h2 holds
h1 = h2 )
proofend;

registration
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra over S;
cluster Relation-like V2() the carrier of S -defined Function-like non empty total for GeneratorSet of U1;
existence
 not for b1 being GeneratorSet of U1 holds b1 is V2()
proofend;
end;

theorem :: EXTENS_1:17
for S being non empty non void ManySortedSign
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
proofend;

theorem :: EXTENS_1:18
for S being non empty non void ManySortedSign
for U1 being MSAlgebra over S
for U2 being MSSubAlgebra of U1
for B1 being MSSubset of U1
for B2 being MSSubset of U2 st B1 = B2 holds
GenMSAlg B1 = GenMSAlg B2
proofend;

theorem :: EXTENS_1:19
for S being non empty non void ManySortedSign
for U1, 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
proofend;