:: by Artur Korni{\l}owicz

::

:: Received May 30, 1997

:: Copyright (c) 1997-2012 Association of Mizar Users

begin

theorem Th1: :: EQUATION:1

for A being set

for B, C being non empty set

for f being Function of A,B

for g being Function of B,C st rng (g * f) = C holds

rng g = C

for B, C being non empty set

for f being Function of A,B

for g being Function of B,C st rng (g * f) = C holds

rng g = C

proof end;

theorem :: EQUATION: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

for g being ManySortedFunction of B,C st g ** f is "onto" holds

g is "onto"

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 st g ** f is "onto" holds

g is "onto"

proof end;

theorem Th3: :: EQUATION:3

for A, B being non empty set

for C, y being set

for f being Function st f in Funcs (A,(Funcs (B,C))) & y in B holds

( dom ((commute f) . y) = A & rng ((commute f) . y) c= C )

for C, y being set

for f being Function st f in Funcs (A,(Funcs (B,C))) & y in B holds

( dom ((commute f) . y) = A & rng ((commute f) . y) c= C )

proof end;

theorem :: EQUATION:4

for I being set

for A, B being ManySortedSet of I st A is_transformable_to B holds

for f being ManySortedFunction of I st doms f = A & rngs f c= B holds

f is ManySortedFunction of A,B

for A, B being ManySortedSet of I st A is_transformable_to B holds

for f being ManySortedFunction of I st doms f = A & rngs f c= B holds

f is ManySortedFunction of A,B

proof end;

theorem Th5: :: EQUATION:5

for I being set

for A, B being ManySortedSet of I

for F being ManySortedFunction of A,B

for C, E being ManySortedSubset of A

for D being ManySortedSubset of C st E = D holds

(F || C) || D = F || E

for A, B being ManySortedSet of I

for F being ManySortedFunction of A,B

for C, E being ManySortedSubset of A

for D being ManySortedSubset of C st E = D holds

(F || C) || D = F || E

proof end;

theorem Th6: :: EQUATION:6

for I being set

for B being V2() ManySortedSet of I

for C being ManySortedSet of I

for A being ManySortedSubset of C

for F being ManySortedFunction of A,B ex G being ManySortedFunction of C,B st G || A = F

for B being V2() ManySortedSet of I

for C being ManySortedSet of I

for A being ManySortedSubset of C

for F being ManySortedFunction of A,B ex G being ManySortedFunction of C,B st G || A = F

proof end;

definition

let I be set ;

let A be ManySortedSet of I;

let F be ManySortedFunction of I;

ex b_{1} being ManySortedSet of I st

for i being set st i in I holds

b_{1} . i = (F . i) " (A . i)

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

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

b_{2} . i = (F . i) " (A . i) ) holds

b_{1} = b_{2}

end;
let A be ManySortedSet of I;

let F be ManySortedFunction of I;

func F "" A -> ManySortedSet of I means :Def1: :: EQUATION:def 1

for i being set st i in I holds

it . i = (F . i) " (A . i);

existence for i being set st i in I holds

it . i = (F . i) " (A . 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 "" EQUATION:def 1 :

for I being set

for A being ManySortedSet of I

for F being ManySortedFunction of I

for b_{4} being ManySortedSet of I holds

( b_{4} = F "" A iff for i being set st i in I holds

b_{4} . i = (F . i) " (A . i) );

for I being set

for A being ManySortedSet of I

for F being ManySortedFunction of I

for b

( b

b

theorem :: EQUATION:7

for I being set

for A, B, C being ManySortedSet of I

for F being ManySortedFunction of A,B holds F .:.: C is ManySortedSubset of B

for A, B, C being ManySortedSet of I

for F being ManySortedFunction of A,B holds F .:.: C is ManySortedSubset of B

proof end;

theorem :: EQUATION:8

for I being set

for A, B, C being ManySortedSet of I

for F being ManySortedFunction of A,B holds F "" C is ManySortedSubset of A

for A, B, C being ManySortedSet of I

for F being ManySortedFunction of A,B holds F "" C is ManySortedSubset of A

proof end;

theorem :: EQUATION:9

for I being set

for A, B being ManySortedSet of I

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

F .:.: A = B

for A, B being ManySortedSet of I

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

F .:.: A = B

proof end;

theorem :: EQUATION:10

for I being set

for A, B being ManySortedSet of I

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

F "" B = A

for A, B being ManySortedSet of I

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

F "" B = A

proof end;

theorem :: EQUATION:11

for I being set

for A being ManySortedSet of I

for F being ManySortedFunction of I st A c= rngs F holds

F .:.: (F "" A) = A

for A being ManySortedSet of I

for F being ManySortedFunction of I st A c= rngs F holds

F .:.: (F "" A) = A

proof end;

theorem :: EQUATION:12

for I being set

for f being ManySortedFunction of I

for X being ManySortedSet of I holds f .:.: X c= rngs f

for f being ManySortedFunction of I

for X being ManySortedSet of I holds f .:.: X c= rngs f

proof end;

begin

theorem Th17: :: EQUATION:17

for S being non empty non void ManySortedSign

for A being MSAlgebra over S holds A is MSSubAlgebra of MSAlgebra(# the Sorts of A, the Charact of A #)

for A being MSAlgebra over S holds A is MSSubAlgebra of MSAlgebra(# the Sorts of A, the Charact of A #)

proof end;

theorem Th18: :: EQUATION:18

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for A being MSSubAlgebra of U0

for o being OperSymbol of S

for x being set st x in Args (o,A) holds

x in Args (o,U0)

for U0 being MSAlgebra over S

for A being MSSubAlgebra of U0

for o being OperSymbol of S

for x being set st x in Args (o,A) holds

x in Args (o,U0)

proof end;

theorem Th19: :: EQUATION:19

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for A being MSSubAlgebra of U0

for o being OperSymbol of S

for x being set st x in Args (o,A) holds

(Den (o,A)) . x = (Den (o,U0)) . x

for U0 being MSAlgebra over S

for A being MSSubAlgebra of U0

for o being OperSymbol of S

for x being set st x in Args (o,A) holds

(Den (o,A)) . x = (Den (o,U0)) . x

proof end;

theorem Th20: :: EQUATION:20

for I being set

for S being non empty non void ManySortedSign

for F being MSAlgebra-Family of I,S

for B being MSSubAlgebra of product F

for o being OperSymbol of S

for x being set st x in Args (o,B) holds

( (Den (o,B)) . x is Function & (Den (o,(product F))) . x is Function )

for S being non empty non void ManySortedSign

for F being MSAlgebra-Family of I,S

for B being MSSubAlgebra of product F

for o being OperSymbol of S

for x being set st x in Args (o,B) holds

( (Den (o,B)) . x is Function & (Den (o,(product F))) . x is Function )

proof end;

definition

let S be non empty non void ManySortedSign ;

let A be MSAlgebra over S;

let B be MSSubAlgebra of A;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ex C being strict MSSubAlgebra of A st

( x = C & B is MSSubAlgebra of C ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ex C being strict MSSubAlgebra of A st

( x = C & B is MSSubAlgebra of C ) ) ) & ( for x being set holds

( x in b_{2} iff ex C being strict MSSubAlgebra of A st

( x = C & B is MSSubAlgebra of C ) ) ) holds

b_{1} = b_{2}

end;
let A be MSAlgebra over S;

let B be MSSubAlgebra of A;

func SuperAlgebraSet B -> set means :Def2: :: EQUATION:def 2

for x being set holds

( x in it iff ex C being strict MSSubAlgebra of A st

( x = C & B is MSSubAlgebra of C ) );

existence for x being set holds

( x in it iff ex C being strict MSSubAlgebra of A st

( x = C & B is MSSubAlgebra of C ) );

ex b

for x being set holds

( x in b

( x = C & B is MSSubAlgebra of C ) )

proof end;

uniqueness for b

( x in b

( x = C & B is MSSubAlgebra of C ) ) ) & ( for x being set holds

( x in b

( x = C & B is MSSubAlgebra of C ) ) ) holds

b

proof end;

:: deftheorem Def2 defines SuperAlgebraSet EQUATION:def 2 :

for S being non empty non void ManySortedSign

for A being MSAlgebra over S

for B being MSSubAlgebra of A

for b_{4} being set holds

( b_{4} = SuperAlgebraSet B iff for x being set holds

( x in b_{4} iff ex C being strict MSSubAlgebra of A st

( x = C & B is MSSubAlgebra of C ) ) );

for S being non empty non void ManySortedSign

for A being MSAlgebra over S

for B being MSSubAlgebra of A

for b

( b

( x in b

( x = C & B is MSSubAlgebra of C ) ) );

registration

let S be non empty non void ManySortedSign ;

let A be MSAlgebra over S;

let B be MSSubAlgebra of A;

coherence

not SuperAlgebraSet B is empty

end;
let A be MSAlgebra over S;

let B be MSSubAlgebra of A;

coherence

not SuperAlgebraSet B is empty

proof end;

registration

let S be non empty non void ManySortedSign ;

existence

ex b_{1} being MSAlgebra over S st

( b_{1} is strict & b_{1} is non-empty & b_{1} is free )

end;
existence

ex b

( b

proof end;

registration

let S be non empty non void ManySortedSign ;

let A be non-empty MSAlgebra over S;

let X be V2() V29() MSSubset of A;

coherence

GenMSAlg X is finitely-generated

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

let X be V2() V29() MSSubset of A;

coherence

GenMSAlg X is finitely-generated

proof end;

registration

let S be non empty non void ManySortedSign ;

let A be non-empty MSAlgebra over S;

existence

ex b_{1} being MSSubAlgebra of A st

( b_{1} is strict & b_{1} is non-empty & b_{1} is finitely-generated )

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

existence

ex b

( b

proof end;

registration

let S be non empty non void ManySortedSign ;

let A be feasible MSAlgebra over S;

existence

ex b_{1} being MSSubAlgebra of A st b_{1} is feasible

end;
let A be feasible MSAlgebra over S;

existence

ex b

proof end;

theorem Th21: :: EQUATION:21

for S being non empty non void ManySortedSign

for U0 being non-empty MSAlgebra over S

for A being MSAlgebra over S

for C being MSSubAlgebra of A

for D being ManySortedSubset of the Sorts of A st D = the Sorts of C holds

for h being ManySortedFunction of A,U0

for g being ManySortedFunction of C,U0 st g = h || D holds

for o being OperSymbol of S

for x being Element of Args (o,A)

for y being Element of Args (o,C) st Args (o,C) <> {} & x = y holds

h # x = g # y

for U0 being non-empty MSAlgebra over S

for A being MSAlgebra over S

for C being MSSubAlgebra of A

for D being ManySortedSubset of the Sorts of A st D = the Sorts of C holds

for h being ManySortedFunction of A,U0

for g being ManySortedFunction of C,U0 st g = h || D holds

for o being OperSymbol of S

for x being Element of Args (o,A)

for y being Element of Args (o,C) st Args (o,C) <> {} & x = y holds

h # x = g # y

proof end;

theorem Th22: :: EQUATION:22

for S being non empty non void ManySortedSign

for U0 being non-empty MSAlgebra over S

for A being feasible MSAlgebra over S

for C being feasible MSSubAlgebra of A

for D being ManySortedSubset of the Sorts of A st D = the Sorts of C holds

for h being ManySortedFunction of A,U0 st h is_homomorphism A,U0 holds

for g being ManySortedFunction of C,U0 st g = h || D holds

g is_homomorphism C,U0

for U0 being non-empty MSAlgebra over S

for A being feasible MSAlgebra over S

for C being feasible MSSubAlgebra of A

for D being ManySortedSubset of the Sorts of A st D = the Sorts of C holds

for h being ManySortedFunction of A,U0 st h is_homomorphism A,U0 holds

for g being ManySortedFunction of C,U0 st g = h || D holds

g is_homomorphism C,U0

proof end;

theorem :: EQUATION:23

for S being non empty non void ManySortedSign

for U0 being non-empty MSAlgebra over S

for B being strict non-empty MSAlgebra over S

for G being GeneratorSet of U0

for H being V2() GeneratorSet of B

for f being ManySortedFunction of U0,B st H c= f .:.: G & f is_homomorphism U0,B holds

f is_epimorphism U0,B

for U0 being non-empty MSAlgebra over S

for B being strict non-empty MSAlgebra over S

for G being GeneratorSet of U0

for H being V2() GeneratorSet of B

for f being ManySortedFunction of U0,B st H c= f .:.: G & f is_homomorphism U0,B holds

f is_epimorphism U0,B

proof end;

theorem Th24: :: EQUATION:24

for S being non empty non void ManySortedSign

for U0, U1 being non-empty MSAlgebra over S

for W being strict non-empty free MSAlgebra over S

for F being ManySortedFunction of U0,U1 st F is_epimorphism U0,U1 holds

for G being ManySortedFunction of W,U1 st G is_homomorphism W,U1 holds

ex H being ManySortedFunction of W,U0 st

( H is_homomorphism W,U0 & G = F ** H )

for U0, U1 being non-empty MSAlgebra over S

for W being strict non-empty free MSAlgebra over S

for F being ManySortedFunction of U0,U1 st F is_epimorphism U0,U1 holds

for G being ManySortedFunction of W,U1 st G is_homomorphism W,U1 holds

ex H being ManySortedFunction of W,U0 st

( H is_homomorphism W,U0 & G = F ** H )

proof end;

theorem Th25: :: EQUATION:25

for S being non empty non void ManySortedSign

for I being non empty finite set

for A being non-empty MSAlgebra over S

for F being MSAlgebra-Family of I,S st ( for i being Element of I ex C being strict non-empty finitely-generated MSSubAlgebra of A st C = F . i ) holds

ex B being strict non-empty finitely-generated MSSubAlgebra of A st

for i being Element of I holds F . i is MSSubAlgebra of B

for I being non empty finite set

for A being non-empty MSAlgebra over S

for F being MSAlgebra-Family of I,S st ( for i being Element of I ex C being strict non-empty finitely-generated MSSubAlgebra of A st C = F . i ) holds

ex B being strict non-empty finitely-generated MSSubAlgebra of A st

for i being Element of I holds F . i is MSSubAlgebra of B

proof end;

theorem Th26: :: EQUATION:26

for S being non empty non void ManySortedSign

for U0 being non-empty MSAlgebra over S

for A, B being strict non-empty finitely-generated MSSubAlgebra of U0 ex M being strict non-empty finitely-generated MSSubAlgebra of U0 st

( A is MSSubAlgebra of M & B is MSSubAlgebra of M )

for U0 being non-empty MSAlgebra over S

for A, B being strict non-empty finitely-generated MSSubAlgebra of U0 ex M being strict non-empty finitely-generated MSSubAlgebra of U0 st

( A is MSSubAlgebra of M & B is MSSubAlgebra of M )

proof end;

theorem :: EQUATION:27

for SG being non empty non void ManySortedSign

for AG being non-empty MSAlgebra over SG

for C being set st C = { A where A is Element of MSSub AG : ex R being strict non-empty finitely-generated MSSubAlgebra of AG st R = A } holds

for F being MSAlgebra-Family of C,SG st ( for c being set st c in C holds

c = F . c ) holds

ex PS being strict non-empty MSSubAlgebra of product F ex BA being ManySortedFunction of PS,AG st BA is_epimorphism PS,AG

for AG being non-empty MSAlgebra over SG

for C being set st C = { A where A is Element of MSSub AG : ex R being strict non-empty finitely-generated MSSubAlgebra of AG st R = A } holds

for F being MSAlgebra-Family of C,SG st ( for c being set st c in C holds

c = F . c ) holds

ex PS being strict non-empty MSSubAlgebra of product F ex BA being ManySortedFunction of PS,AG st BA is_epimorphism PS,AG

proof end;

theorem :: EQUATION:28

for S being non empty non void ManySortedSign

for U0 being free feasible MSAlgebra over S

for A being free GeneratorSet of U0

for Z being MSSubset of U0 st Z c= A & GenMSAlg Z is feasible holds

GenMSAlg Z is free

for U0 being free feasible MSAlgebra over S

for A being free GeneratorSet of U0

for Z being MSSubset of U0 st Z c= A & GenMSAlg Z is feasible holds

GenMSAlg Z is free

proof end;

begin

definition

let S be non empty non void ManySortedSign ;

correctness

coherence

FreeMSA ( the carrier of S --> NAT) is MSAlgebra over S;

;

end;
correctness

coherence

FreeMSA ( the carrier of S --> NAT) is MSAlgebra over S;

;

:: deftheorem defines TermAlg EQUATION:def 3 :

for S being non empty non void ManySortedSign holds TermAlg S = FreeMSA ( the carrier of S --> NAT);

for S being non empty non void ManySortedSign holds TermAlg S = FreeMSA ( the carrier of S --> NAT);

registration

let S be non empty non void ManySortedSign ;

coherence

( TermAlg S is strict & TermAlg S is non-empty & TermAlg S is free ) ;

end;
coherence

( TermAlg S is strict & TermAlg S is non-empty & TermAlg S is free ) ;

definition

let S be non empty non void ManySortedSign ;

coherence

[| the Sorts of (TermAlg S), the Sorts of (TermAlg S)|] is ManySortedSet of the carrier of S;

;

end;
func Equations S -> ManySortedSet of the carrier of S equals :: EQUATION:def 4

[| the Sorts of (TermAlg S), the Sorts of (TermAlg S)|];

correctness [| the Sorts of (TermAlg S), the Sorts of (TermAlg S)|];

coherence

[| the Sorts of (TermAlg S), the Sorts of (TermAlg S)|] is ManySortedSet of the carrier of S;

;

:: deftheorem defines Equations EQUATION:def 4 :

for S being non empty non void ManySortedSign holds Equations S = [| the Sorts of (TermAlg S), the Sorts of (TermAlg S)|];

for S being non empty non void ManySortedSign holds Equations S = [| the Sorts of (TermAlg S), the Sorts of (TermAlg S)|];

definition
end;

notation

let S be non empty non void ManySortedSign ;

let s be SortSymbol of S;

let x, y be Element of the Sorts of (TermAlg S) . s;

synonym x '=' y for [S,s];

end;
let s be SortSymbol of S;

let x, y be Element of the Sorts of (TermAlg S) . s;

synonym x '=' y for [S,s];

definition

let S be non empty non void ManySortedSign ;

let s be SortSymbol of S;

let x, y be Element of the Sorts of (TermAlg S) . s;

:: original: '='

redefine func x '=' y -> Element of (Equations S) . s;

coherence

'=' is Element of (Equations S) . s

end;
let s be SortSymbol of S;

let x, y be Element of the Sorts of (TermAlg S) . s;

:: original: '='

redefine func x '=' y -> Element of (Equations S) . s;

coherence

'=' is Element of (Equations S) . s

proof end;

theorem Th29: :: EQUATION:29

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for e being Element of (Equations S) . s holds e `1 in the Sorts of (TermAlg S) . s

for s being SortSymbol of S

for e being Element of (Equations S) . s holds e `1 in the Sorts of (TermAlg S) . s

proof end;

theorem Th30: :: EQUATION:30

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for e being Element of (Equations S) . s holds e `2 in the Sorts of (TermAlg S) . s

for s being SortSymbol of S

for e being Element of (Equations S) . s holds e `2 in the Sorts of (TermAlg S) . s

proof end;

definition

let S be non empty non void ManySortedSign ;

let A be MSAlgebra over S;

let s be SortSymbol of S;

let e be Element of (Equations S) . s;

end;
let A be MSAlgebra over S;

let s be SortSymbol of S;

let e be Element of (Equations S) . s;

pred A |= e means :Def5: :: EQUATION:def 5

for h being ManySortedFunction of (TermAlg S),A st h is_homomorphism TermAlg S,A holds

(h . s) . (e `1) = (h . s) . (e `2);

for h being ManySortedFunction of (TermAlg S),A st h is_homomorphism TermAlg S,A holds

(h . s) . (e `1) = (h . s) . (e `2);

:: deftheorem Def5 defines |= EQUATION:def 5 :

for S being non empty non void ManySortedSign

for A being MSAlgebra over S

for s being SortSymbol of S

for e being Element of (Equations S) . s holds

( A |= e iff for h being ManySortedFunction of (TermAlg S),A st h is_homomorphism TermAlg S,A holds

(h . s) . (e `1) = (h . s) . (e `2) );

for S being non empty non void ManySortedSign

for A being MSAlgebra over S

for s being SortSymbol of S

for e being Element of (Equations S) . s holds

( A |= e iff for h being ManySortedFunction of (TermAlg S),A st h is_homomorphism TermAlg S,A holds

(h . s) . (e `1) = (h . s) . (e `2) );

definition

let S be non empty non void ManySortedSign ;

let A be MSAlgebra over S;

let E be EqualSet of S;

end;
let A be MSAlgebra over S;

let E be EqualSet of S;

pred A |= E means :Def6: :: EQUATION:def 6

for s being SortSymbol of S

for e being Element of (Equations S) . s st e in E . s holds

A |= e;

for s being SortSymbol of S

for e being Element of (Equations S) . s st e in E . s holds

A |= e;

:: deftheorem Def6 defines |= EQUATION:def 6 :

for S being non empty non void ManySortedSign

for A being MSAlgebra over S

for E being EqualSet of S holds

( A |= E iff for s being SortSymbol of S

for e being Element of (Equations S) . s st e in E . s holds

A |= e );

for S being non empty non void ManySortedSign

for A being MSAlgebra over S

for E being EqualSet of S holds

( A |= E iff for s being SortSymbol of S

for e being Element of (Equations S) . s st e in E . s holds

A |= e );

theorem Th31: :: EQUATION:31

for S being non empty non void ManySortedSign

for U0 being non-empty MSAlgebra over S

for s being SortSymbol of S

for e being Element of (Equations S) . s

for U2 being strict non-empty MSSubAlgebra of U0 st U0 |= e holds

U2 |= e

for U0 being non-empty MSAlgebra over S

for s being SortSymbol of S

for e being Element of (Equations S) . s

for U2 being strict non-empty MSSubAlgebra of U0 st U0 |= e holds

U2 |= e

proof end;

theorem :: EQUATION:32

for S being non empty non void ManySortedSign

for U0 being non-empty MSAlgebra over S

for E being EqualSet of S

for U2 being strict non-empty MSSubAlgebra of U0 st U0 |= E holds

U2 |= E

for U0 being non-empty MSAlgebra over S

for E being EqualSet of S

for U2 being strict non-empty MSSubAlgebra of U0 st U0 |= E holds

U2 |= E

proof end;

theorem Th33: :: EQUATION:33

for S being non empty non void ManySortedSign

for U0, U1 being non-empty MSAlgebra over S

for s being SortSymbol of S

for e being Element of (Equations S) . s st U0,U1 are_isomorphic & U0 |= e holds

U1 |= e

for U0, U1 being non-empty MSAlgebra over S

for s being SortSymbol of S

for e being Element of (Equations S) . s st U0,U1 are_isomorphic & U0 |= e holds

U1 |= e

proof end;

theorem :: EQUATION:34

for S being non empty non void ManySortedSign

for U0, U1 being non-empty MSAlgebra over S

for E being EqualSet of S st U0,U1 are_isomorphic & U0 |= E holds

U1 |= E

for U0, U1 being non-empty MSAlgebra over S

for E being EqualSet of S st U0,U1 are_isomorphic & U0 |= E holds

U1 |= E

proof end;

theorem Th35: :: EQUATION:35

for S being non empty non void ManySortedSign

for U0 being non-empty MSAlgebra over S

for s being SortSymbol of S

for e being Element of (Equations S) . s

for R being MSCongruence of U0 st U0 |= e holds

QuotMSAlg (U0,R) |= e

for U0 being non-empty MSAlgebra over S

for s being SortSymbol of S

for e being Element of (Equations S) . s

for R being MSCongruence of U0 st U0 |= e holds

QuotMSAlg (U0,R) |= e

proof end;

theorem :: EQUATION:36

for S being non empty non void ManySortedSign

for U0 being non-empty MSAlgebra over S

for E being EqualSet of S

for R being MSCongruence of U0 st U0 |= E holds

QuotMSAlg (U0,R) |= E

for U0 being non-empty MSAlgebra over S

for E being EqualSet of S

for R being MSCongruence of U0 st U0 |= E holds

QuotMSAlg (U0,R) |= E

proof end;

Lm1: for S being non empty non void ManySortedSign

for s being SortSymbol of S

for e being Element of (Equations S) . s

for I being non empty set

for A being MSAlgebra-Family of I,S st ( for i being Element of I holds A . i |= e ) holds

product A |= e

proof end;

theorem Th37: :: EQUATION:37

for I being set

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for e being Element of (Equations S) . s

for F being MSAlgebra-Family of I,S st ( for i being set st i in I holds

ex A being MSAlgebra over S st

( A = F . i & A |= e ) ) holds

product F |= e

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for e being Element of (Equations S) . s

for F being MSAlgebra-Family of I,S st ( for i being set st i in I holds

ex A being MSAlgebra over S st

( A = F . i & A |= e ) ) holds

product F |= e

proof end;

theorem :: EQUATION:38

for I being set

for S being non empty non void ManySortedSign

for E being EqualSet of S

for F being MSAlgebra-Family of I,S st ( for i being set st i in I holds

ex A being MSAlgebra over S st

( A = F . i & A |= E ) ) holds

product F |= E

for S being non empty non void ManySortedSign

for E being EqualSet of S

for F being MSAlgebra-Family of I,S st ( for i being set st i in I holds

ex A being MSAlgebra over S st

( A = F . i & A |= E ) ) holds

product F |= E

proof end;