:: by Artur Korni{\l}owicz

::

:: Received March 23, 1995

:: Copyright (c) 1995-2019 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

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

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

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)

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

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"

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

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

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 )

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

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

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 )

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 )

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

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;

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 )

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;

not for b_{1} being GeneratorSet of U1 holds b_{1} is V2()

end;
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

proof 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

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

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

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;