:: by Artur Korni\l owicz

::

:: Received June 11, 1996

:: Copyright (c) 1996-2018 Association of Mizar Users

registration

let I be set ;

let M be ManySortedSet of I;

existence

not for b_{1} being Element of Bool M holds b_{1} is V35()

end;
let M be ManySortedSet of I;

existence

not for b

proof end;

registration

let I be set ;

let M be V2() ManySortedSet of I;

existence

ex b_{1} being ManySortedSubset of M st

( b_{1} is V2() & b_{1} is V35() )

end;
let M be V2() ManySortedSet of I;

existence

ex b

( b

proof end;

registration

let S be non empty non void ManySortedSign ;

let A be non-empty MSAlgebra over S;

let o be OperSymbol of S;

coherence

for b_{1} being Element of Args (o,A) holds b_{1} is FinSequence-like

end;
let A be non-empty MSAlgebra over S;

let o be OperSymbol of S;

coherence

for b

proof end;

registration

let S be non empty non void ManySortedSign ;

let I be set ;

let s be SortSymbol of S;

let F be MSAlgebra-Family of I,S;

coherence

for b_{1} being Element of (SORTS F) . s holds

( b_{1} is Function-like & b_{1} is Relation-like )

end;
let I be set ;

let s be SortSymbol of S;

let F be MSAlgebra-Family of I,S;

coherence

for b

( b

proof end;

registration

let S be non empty non void ManySortedSign ;

let X be V2() ManySortedSet of the carrier of S;

coherence

( FreeGen X is free & FreeGen X is non-empty ) by MSAFREE:14, MSAFREE:16;

end;
let X be V2() ManySortedSet of the carrier of S;

coherence

( FreeGen X is free & FreeGen X is non-empty ) by MSAFREE:14, MSAFREE:16;

registration

let S be non empty non void ManySortedSign ;

let X be V2() ManySortedSet of the carrier of S;

coherence

FreeMSA X is free by MSAFREE:17;

end;
let X be V2() ManySortedSet of the carrier of S;

coherence

FreeMSA X is free by MSAFREE:17;

registration

let S be non empty non void ManySortedSign ;

let A, B be non-empty MSAlgebra over S;

coherence

[:A,B:] is non-empty

end;
let A, B be non-empty MSAlgebra over S;

coherence

[:A,B:] is non-empty

proof end;

theorem :: MSUALG_9:1

for a, X, Y being set

for f being Function st a in dom f & f . a in [:X,Y:] holds

f . a = [((pr1 f) . a),((pr2 f) . a)]

for f being Function st a in dom f & f . a in [:X,Y:] holds

f . a = [((pr1 f) . a),((pr2 f) . a)]

proof end;

theorem :: MSUALG_9:7

for I being set

for M being V2() ManySortedSet of I

for B being V35() ManySortedSubset of M ex C being V2() V35() ManySortedSubset of M st B c= C

for M being V2() ManySortedSet of I

for B being V35() ManySortedSubset of M ex C being V2() V35() ManySortedSubset of M st B c= C

proof end;

theorem :: MSUALG_9:8

for I being set

for A, B being ManySortedSet of I

for F, G being ManySortedFunction of A,{B} holds F = G

for A, B being ManySortedSet of I

for F, G being ManySortedFunction of A,{B} holds F = G

proof end;

theorem Th9: :: MSUALG_9:9

for I being set

for A being V2() ManySortedSet of I

for B being ManySortedSet of I

for F being ManySortedFunction of A,{B} holds F is "onto"

for A being V2() ManySortedSet of I

for B being ManySortedSet of I

for F being ManySortedFunction of A,{B} holds F is "onto"

proof end;

theorem Th10: :: MSUALG_9:10

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 "1-1"

for A being ManySortedSet of I

for B being V2() ManySortedSet of I

for F being ManySortedFunction of {A},B holds F is "1-1"

proof end;

theorem :: MSUALG_9:11

for S being non empty non void ManySortedSign

for X being V2() ManySortedSet of the carrier of S holds Reverse X is "1-1"

for X being V2() ManySortedSet of the carrier of S holds Reverse X is "1-1"

proof end;

theorem :: MSUALG_9:12

for I being set

for A being V2() V35() ManySortedSet of I ex F being ManySortedFunction of I --> NAT,A st F is "onto"

for A being V2() V35() ManySortedSet of I ex F being ManySortedFunction of I --> NAT,A st F is "onto"

proof end;

theorem :: MSUALG_9:13

for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

for f, g being Element of product the Sorts of A st ( for i being object holds (proj ( the Sorts of A,i)) . f = (proj ( the Sorts of A,i)) . g ) holds

f = g

for A being non-empty MSAlgebra over S

for f, g being Element of product the Sorts of A st ( for i being object holds (proj ( the Sorts of A,i)) . f = (proj ( the Sorts of A,i)) . g ) holds

f = g

proof end;

theorem :: MSUALG_9:14

for S being non empty non void ManySortedSign

for I being non empty set

for s being Element of S

for A being MSAlgebra-Family of I,S

for f, g being Element of product (Carrier (A,s)) st ( for a being Element of I holds (proj ((Carrier (A,s)),a)) . f = (proj ((Carrier (A,s)),a)) . g ) holds

f = g

for I being non empty set

for s being Element of S

for A being MSAlgebra-Family of I,S

for f, g being Element of product (Carrier (A,s)) st ( for a being Element of I holds (proj ((Carrier (A,s)),a)) . f = (proj ((Carrier (A,s)),a)) . g ) holds

f = g

proof end;

theorem :: MSUALG_9:15

for S being non empty non void ManySortedSign

for A, B being non-empty MSAlgebra over S

for C being non-empty MSSubAlgebra of A

for h1 being ManySortedFunction of B,C st h1 is_homomorphism B,C holds

for h2 being ManySortedFunction of B,A st h1 = h2 holds

h2 is_homomorphism B,A

for A, B being non-empty MSAlgebra over S

for C being non-empty MSSubAlgebra of A

for h1 being ManySortedFunction of B,C st h1 is_homomorphism B,C holds

for h2 being ManySortedFunction of B,A st h1 = h2 holds

h2 is_homomorphism B,A

proof end;

theorem :: MSUALG_9:16

for S being non empty non void ManySortedSign

for A, B being non-empty MSAlgebra over S

for F being ManySortedFunction of A,B st F is_monomorphism A,B holds

A, Image F are_isomorphic

for A, B being non-empty MSAlgebra over S

for F being ManySortedFunction of A,B st F is_monomorphism A,B holds

A, Image F are_isomorphic

proof end;

theorem Th17: :: MSUALG_9:17

for S being non empty non void ManySortedSign

for A, B being non-empty MSAlgebra over S

for F being ManySortedFunction of A,B st F is "onto" holds

for o being OperSymbol of S

for x being Element of Args (o,B) ex y being Element of Args (o,A) st F # y = x

for A, B being non-empty MSAlgebra over S

for F being ManySortedFunction of A,B st F is "onto" holds

for o being OperSymbol of S

for x being Element of Args (o,B) ex y being Element of Args (o,A) st F # y = x

proof end;

theorem Th18: :: MSUALG_9:18

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for o being OperSymbol of S

for x being Element of Args (o,A) holds (Den (o,A)) . x in the Sorts of A . (the_result_sort_of o)

for A being non-empty MSAlgebra over S

for o being OperSymbol of S

for x being Element of Args (o,A) holds (Den (o,A)) . x in the Sorts of A . (the_result_sort_of o)

proof end;

theorem Th19: :: MSUALG_9:19

for S being non empty non void ManySortedSign

for A, B, C being non-empty MSAlgebra over S

for F1 being ManySortedFunction of A,B

for F2 being ManySortedFunction of A,C st F1 is_epimorphism A,B & F2 is_homomorphism A,C holds

for G being ManySortedFunction of B,C st G ** F1 = F2 holds

G is_homomorphism B,C

for A, B, C being non-empty MSAlgebra over S

for F1 being ManySortedFunction of A,B

for F2 being ManySortedFunction of A,C st F1 is_epimorphism A,B & F2 is_homomorphism A,C holds

for G being ManySortedFunction of B,C st G ** F1 = F2 holds

G is_homomorphism B,C

proof end;

definition

let I be set ;

let A be ManySortedSet of I;

let B, C be V2() ManySortedSet of I;

let F be ManySortedFunction of A,[|B,C|];

ex b_{1} being ManySortedFunction of A,B st

for i being set st i in I holds

b_{1} . i = pr1 (F . i)

for b_{1}, b_{2} being ManySortedFunction of A,B st ( for i being set st i in I holds

b_{1} . i = pr1 (F . i) ) & ( for i being set st i in I holds

b_{2} . i = pr1 (F . i) ) holds

b_{1} = b_{2}

ex b_{1} being ManySortedFunction of A,C st

for i being set st i in I holds

b_{1} . i = pr2 (F . i)

for b_{1}, b_{2} being ManySortedFunction of A,C st ( for i being set st i in I holds

b_{1} . i = pr2 (F . i) ) & ( for i being set st i in I holds

b_{2} . i = pr2 (F . i) ) holds

b_{1} = b_{2}

end;
let A be ManySortedSet of I;

let B, C be V2() ManySortedSet of I;

let F be ManySortedFunction of A,[|B,C|];

func Mpr1 F -> ManySortedFunction of A,B means :Def1: :: MSUALG_9:def 1

for i being set st i in I holds

it . i = pr1 (F . i);

existence for i being set st i in I holds

it . i = pr1 (F . i);

ex b

for i being set st i in I holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func Mpr2 F -> ManySortedFunction of A,C means :Def2: :: MSUALG_9:def 2

for i being set st i in I holds

it . i = pr2 (F . i);

existence for i being set st i in I holds

it . i = pr2 (F . i);

ex b

for i being set st i in I holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def1 defines Mpr1 MSUALG_9:def 1 :

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,C|]

for b_{6} being ManySortedFunction of A,B holds

( b_{6} = Mpr1 F iff for i being set st i in I holds

b_{6} . i = pr1 (F . i) );

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,C|]

for b

( b

b

:: deftheorem Def2 defines Mpr2 MSUALG_9:def 2 :

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,C|]

for b_{6} being ManySortedFunction of A,C holds

( b_{6} = Mpr2 F iff for i being set st i in I holds

b_{6} . i = pr2 (F . i) );

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,C|]

for b

( b

b

theorem :: MSUALG_9:20

for a, I being set

for A being ManySortedSet of I

for F being ManySortedFunction of A,[|(I --> {a}),(I --> {a})|] holds Mpr1 F = Mpr2 F

for A being ManySortedSet of I

for F being ManySortedFunction of A,[|(I --> {a}),(I --> {a})|] holds Mpr1 F = Mpr2 F

proof end;

theorem :: MSUALG_9:21

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,C|] st F is "onto" holds

Mpr1 F is "onto"

for A being ManySortedSet of I

for B, C being V2() ManySortedSet of I

for F being ManySortedFunction of A,[|B,C|] st F is "onto" holds

Mpr1 F is "onto"

proof end;

theorem :: MSUALG_9:22

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,C|] st F is "onto" holds

Mpr2 F is "onto"

for A being ManySortedSet of I

for B, C being V2() ManySortedSet of I

for F being ManySortedFunction of A,[|B,C|] st F is "onto" holds

Mpr2 F is "onto"

proof end;

theorem :: MSUALG_9:23

for I being set

for A, M being ManySortedSet of I

for B, C being V2() ManySortedSet of I

for F being ManySortedFunction of A,[|B,C|] st M in doms F holds

for i being set st i in I holds

(F .. M) . i = [(((Mpr1 F) .. M) . i),(((Mpr2 F) .. M) . i)]

for A, M being ManySortedSet of I

for B, C being V2() ManySortedSet of I

for F being ManySortedFunction of A,[|B,C|] st M in doms F holds

for i being set st i in I holds

(F .. M) . i = [(((Mpr1 F) .. M) . i),(((Mpr2 F) .. M) . i)]

proof end;

registration

let S be non empty ManySortedSign ;

coherence

( the Sorts of (Trivial_Algebra S) is finite-yielding & the Sorts of (Trivial_Algebra S) is non-empty )

end;
coherence

( the Sorts of (Trivial_Algebra S) is finite-yielding & the Sorts of (Trivial_Algebra S) is non-empty )

proof end;

registration

let S be non empty ManySortedSign ;

coherence

( Trivial_Algebra S is finite-yielding & Trivial_Algebra S is non-empty ) ;

end;
coherence

( Trivial_Algebra S is finite-yielding & Trivial_Algebra S is non-empty ) ;

theorem Th24: :: MSUALG_9:24

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for F being ManySortedFunction of A,(Trivial_Algebra S)

for o being OperSymbol of S

for x being Element of Args (o,A) holds

( (F . (the_result_sort_of o)) . ((Den (o,A)) . x) = 0 & (Den (o,(Trivial_Algebra S))) . (F # x) = 0 )

for A being non-empty MSAlgebra over S

for F being ManySortedFunction of A,(Trivial_Algebra S)

for o being OperSymbol of S

for x being Element of Args (o,A) holds

( (F . (the_result_sort_of o)) . ((Den (o,A)) . x) = 0 & (Den (o,(Trivial_Algebra S))) . (F # x) = 0 )

proof end;

theorem Th25: :: MSUALG_9:25

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for F being ManySortedFunction of A,(Trivial_Algebra S) holds F is_epimorphism A, Trivial_Algebra S

for A being non-empty MSAlgebra over S

for F being ManySortedFunction of A,(Trivial_Algebra S) holds F is_epimorphism A, Trivial_Algebra S

proof end;

theorem :: MSUALG_9:26

for S being non empty non void ManySortedSign

for A being MSAlgebra over S st ex X being ManySortedSet of the carrier of S st the Sorts of A = {X} holds

A, Trivial_Algebra S are_isomorphic

for A being MSAlgebra over S st ex X being ManySortedSet of the carrier of S st the Sorts of A = {X} holds

A, Trivial_Algebra S are_isomorphic

proof end;

theorem :: MSUALG_9:27

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for C being MSCongruence of A holds C is ManySortedSubset of [| the Sorts of A, the Sorts of A|]

for A being non-empty MSAlgebra over S

for C being MSCongruence of A holds C is ManySortedSubset of [| the Sorts of A, the Sorts of A|]

proof end;

theorem :: MSUALG_9:28

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for R being Subset of (CongrLatt A)

for F being SubsetFamily of [| the Sorts of A, the Sorts of A|] st R = F holds

meet |:F:| is MSCongruence of A

for A being non-empty MSAlgebra over S

for R being Subset of (CongrLatt A)

for F being SubsetFamily of [| the Sorts of A, the Sorts of A|] st R = F holds

meet |:F:| is MSCongruence of A

proof end;

theorem :: MSUALG_9:29

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for C being MSCongruence of A st C = [| the Sorts of A, the Sorts of A|] holds

the Sorts of (QuotMSAlg (A,C)) = { the Sorts of A}

for A being non-empty MSAlgebra over S

for C being MSCongruence of A st C = [| the Sorts of A, the Sorts of A|] holds

the Sorts of (QuotMSAlg (A,C)) = { the Sorts of A}

proof end;

theorem Th30: :: MSUALG_9:30

for S being non empty non void ManySortedSign

for A, B being non-empty MSAlgebra over S

for F being ManySortedFunction of A,B st F is_homomorphism A,B holds

(MSHomQuot F) ** (MSNat_Hom (A,(MSCng F))) = F

for A, B being non-empty MSAlgebra over S

for F being ManySortedFunction of A,B st F is_homomorphism A,B holds

(MSHomQuot F) ** (MSNat_Hom (A,(MSCng F))) = F

proof end;

theorem Th31: :: MSUALG_9:31

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for C being MSCongruence of A

for s being SortSymbol of S

for a being Element of the Sorts of (QuotMSAlg (A,C)) . s ex x being Element of the Sorts of A . s st a = Class (C,x)

for A being non-empty MSAlgebra over S

for C being MSCongruence of A

for s being SortSymbol of S

for a being Element of the Sorts of (QuotMSAlg (A,C)) . s ex x being Element of the Sorts of A . s st a = Class (C,x)

proof end;

theorem :: MSUALG_9:32

for S being non empty non void ManySortedSign

for A being MSAlgebra over S

for C1, C2 being MSEquivalence-like ManySortedRelation of A st C1 c= C2 holds

for i being Element of S

for x, y being Element of the Sorts of A . i st [x,y] in C1 . i holds

( Class (C1,x) c= Class (C2,y) & ( A is non-empty implies Class (C1,y) c= Class (C2,x) ) )

for A being MSAlgebra over S

for C1, C2 being MSEquivalence-like ManySortedRelation of A st C1 c= C2 holds

for i being Element of S

for x, y being Element of the Sorts of A . i st [x,y] in C1 . i holds

( Class (C1,x) c= Class (C2,y) & ( A is non-empty implies Class (C1,y) c= Class (C2,x) ) )

proof end;

theorem :: MSUALG_9:33

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for C being MSCongruence of A

for s being SortSymbol of S

for x, y being Element of the Sorts of A . s holds

( ((MSNat_Hom (A,C)) . s) . x = ((MSNat_Hom (A,C)) . s) . y iff [x,y] in C . s )

for A being non-empty MSAlgebra over S

for C being MSCongruence of A

for s being SortSymbol of S

for x, y being Element of the Sorts of A . s holds

( ((MSNat_Hom (A,C)) . s) . x = ((MSNat_Hom (A,C)) . s) . y iff [x,y] in C . s )

proof end;

Lm1: now :: thesis: for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for C1, C2 being MSCongruence of A

for G being ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)) st ( for i being Element of S

for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i

for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds

(G . i) . x = Class (C2,xx) ) holds

G is "onto"

for A being non-empty MSAlgebra over S

for C1, C2 being MSCongruence of A

for G being ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)) st ( for i being Element of S

for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i

for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds

(G . i) . x = Class (C2,xx) ) holds

G is "onto"

let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S

for C1, C2 being MSCongruence of A

for G being ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)) st ( for i being Element of S

for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i

for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds

(G . i) . x = Class (C2,xx) ) holds

G is "onto"

let A be non-empty MSAlgebra over S; :: thesis: for C1, C2 being MSCongruence of A

for G being ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)) st ( for i being Element of S

for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i

for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds

(G . i) . x = Class (C2,xx) ) holds

G is "onto"

let C1, C2 be MSCongruence of A; :: thesis: for G being ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)) st ( for i being Element of S

for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i

for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds

(G . i) . x = Class (C2,xx) ) holds

G is "onto"

let G be ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)); :: thesis: ( ( for i being Element of S

for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i

for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds

(G . i) . x = Class (C2,xx) ) implies G is "onto" )

assume A1: for i being Element of S

for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i

for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds

(G . i) . x = Class (C2,xx) ; :: thesis: G is "onto"

thus G is "onto" :: thesis: verum

end;
for C1, C2 being MSCongruence of A

for G being ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)) st ( for i being Element of S

for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i

for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds

(G . i) . x = Class (C2,xx) ) holds

G is "onto"

let A be non-empty MSAlgebra over S; :: thesis: for C1, C2 being MSCongruence of A

for G being ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)) st ( for i being Element of S

for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i

for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds

(G . i) . x = Class (C2,xx) ) holds

G is "onto"

let C1, C2 be MSCongruence of A; :: thesis: for G being ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)) st ( for i being Element of S

for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i

for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds

(G . i) . x = Class (C2,xx) ) holds

G is "onto"

let G be ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)); :: thesis: ( ( for i being Element of S

for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i

for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds

(G . i) . x = Class (C2,xx) ) implies G is "onto" )

assume A1: for i being Element of S

for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i

for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds

(G . i) . x = Class (C2,xx) ; :: thesis: G is "onto"

thus G is "onto" :: thesis: verum

proof

let i be set ; :: according to MSUALG_3:def 3 :: thesis: ( not i in the carrier of S or rng (G . i) = the Sorts of (QuotMSAlg (A,C2)) . i )

set sL = the Sorts of (QuotMSAlg (A,C1));

set sP = the Sorts of (QuotMSAlg (A,C2));

assume i in the carrier of S ; :: thesis: rng (G . i) = the Sorts of (QuotMSAlg (A,C2)) . i

then reconsider s = i as SortSymbol of S ;

A2: dom (G . s) = the Sorts of (QuotMSAlg (A,C1)) . s by FUNCT_2:def 1;

rng (G . s) c= the Sorts of (QuotMSAlg (A,C2)) . s ;

hence rng (G . i) c= the Sorts of (QuotMSAlg (A,C2)) . i ; :: according to XBOOLE_0:def 10 :: thesis: the Sorts of (QuotMSAlg (A,C2)) . i c= rng (G . i)

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in the Sorts of (QuotMSAlg (A,C2)) . i or q in rng (G . i) )

assume q in the Sorts of (QuotMSAlg (A,C2)) . i ; :: thesis: q in rng (G . i)

then q in Class (C2 . s) by MSUALG_4:def 6;

then consider a being object such that

A3: a in the Sorts of A . s and

A4: q = Class ((C2 . s),a) by EQREL_1:def 3;

reconsider a = a as Element of the Sorts of A . s by A3;

Class ((C1 . s),a) in Class (C1 . s) by EQREL_1:def 3;

then reconsider x = Class (C1,a) as Element of the Sorts of (QuotMSAlg (A,C1)) . s by MSUALG_4:def 6;

(G . s) . x = Class (C2,a) by A1

.= Class ((C2 . s),a) ;

hence q in rng (G . i) by A4, A2, FUNCT_1:def 3; :: thesis: verum

end;
set sL = the Sorts of (QuotMSAlg (A,C1));

set sP = the Sorts of (QuotMSAlg (A,C2));

assume i in the carrier of S ; :: thesis: rng (G . i) = the Sorts of (QuotMSAlg (A,C2)) . i

then reconsider s = i as SortSymbol of S ;

A2: dom (G . s) = the Sorts of (QuotMSAlg (A,C1)) . s by FUNCT_2:def 1;

rng (G . s) c= the Sorts of (QuotMSAlg (A,C2)) . s ;

hence rng (G . i) c= the Sorts of (QuotMSAlg (A,C2)) . i ; :: according to XBOOLE_0:def 10 :: thesis: the Sorts of (QuotMSAlg (A,C2)) . i c= rng (G . i)

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in the Sorts of (QuotMSAlg (A,C2)) . i or q in rng (G . i) )

assume q in the Sorts of (QuotMSAlg (A,C2)) . i ; :: thesis: q in rng (G . i)

then q in Class (C2 . s) by MSUALG_4:def 6;

then consider a being object such that

A3: a in the Sorts of A . s and

A4: q = Class ((C2 . s),a) by EQREL_1:def 3;

reconsider a = a as Element of the Sorts of A . s by A3;

Class ((C1 . s),a) in Class (C1 . s) by EQREL_1:def 3;

then reconsider x = Class (C1,a) as Element of the Sorts of (QuotMSAlg (A,C1)) . s by MSUALG_4:def 6;

(G . s) . x = Class (C2,a) by A1

.= Class ((C2 . s),a) ;

hence q in rng (G . i) by A4, A2, FUNCT_1:def 3; :: thesis: verum

theorem Th34: :: MSUALG_9:34

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for C1, C2 being MSCongruence of A

for G being ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)) st ( for i being Element of S

for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i

for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds

(G . i) . x = Class (C2,xx) ) holds

G ** (MSNat_Hom (A,C1)) = MSNat_Hom (A,C2)

for A being non-empty MSAlgebra over S

for C1, C2 being MSCongruence of A

for G being ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)) st ( for i being Element of S

for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i

for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds

(G . i) . x = Class (C2,xx) ) holds

G ** (MSNat_Hom (A,C1)) = MSNat_Hom (A,C2)

proof end;

theorem Th35: :: MSUALG_9:35

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for C1, C2 being MSCongruence of A

for G being ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)) st ( for i being Element of S

for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i

for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds

(G . i) . x = Class (C2,xx) ) holds

G is_epimorphism QuotMSAlg (A,C1), QuotMSAlg (A,C2)

for A being non-empty MSAlgebra over S

for C1, C2 being MSCongruence of A

for G being ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)) st ( for i being Element of S

for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i

for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds

(G . i) . x = Class (C2,xx) ) holds

G is_epimorphism QuotMSAlg (A,C1), QuotMSAlg (A,C2)

proof end;

theorem :: MSUALG_9:36

for S being non empty non void ManySortedSign

for A, B being non-empty MSAlgebra over S

for F being ManySortedFunction of A,B st F is_homomorphism A,B holds

for C1 being MSCongruence of A st C1 c= MSCng F holds

ex H being ManySortedFunction of (QuotMSAlg (A,C1)),B st

( H is_homomorphism QuotMSAlg (A,C1),B & F = H ** (MSNat_Hom (A,C1)) )

for A, B being non-empty MSAlgebra over S

for F being ManySortedFunction of A,B st F is_homomorphism A,B holds

for C1 being MSCongruence of A st C1 c= MSCng F holds

ex H being ManySortedFunction of (QuotMSAlg (A,C1)),B st

( H is_homomorphism QuotMSAlg (A,C1),B & F = H ** (MSNat_Hom (A,C1)) )

proof end;