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

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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)

proof end;

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

proof end;

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"

proof end;

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

proof end;

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

proof end;

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 )

proof end;

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

proof end;

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

proof end;

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 )

proof end;

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 )

proof end;

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

proof end;

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 by Th12;

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 )

proof end;

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 b₁ being GeneratorSet of U1 holds b₁ is V2()

proof end;

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

proof end;

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

proof end;

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

proof end;