:: EQUATION semantic presentation

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
proof
let A be set ; ::_thesis: 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
let B, C be non empty set ; ::_thesis: for f being Function of A,B
for g being Function of B,C st rng (g * f) = C holds
rng g = C
let f be Function of A,B; ::_thesis: for g being Function of B,C st rng (g * f) = C holds
rng g = C
let g be Function of B,C; ::_thesis: ( rng (g * f) = C implies rng g = C )
assume A1: rng (g * f) = C ; ::_thesis: rng g = C
thus  rng g c= C ; :: according to XBOOLE_0:def_10 ::_thesis: C c= rng g
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in C or q in rng g )
assume  q in C ; ::_thesis: q in rng g
then consider x being set  such that
A2: x in dom (g * f) and
A3: q = (g * f) . x by A1, FUNCT_1:def_3;
A4: dom f = A by FUNCT_2:def_1;
then A5: f . x in rng f by A2, FUNCT_1:def_3;
 dom (g * f) = A by FUNCT_2:def_1;
then A6: rng f c= dom g by A4, FUNCT_1:15;
 q = g . (f . x) by A2, A3, FUNCT_1:12;
hence  q in rng g by A6, A5, FUNCT_1:def_3; ::_thesis: verum
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"
proof
let I be set ; ::_thesis: 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"
let A be ManySortedSet of I; ::_thesis: 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"
let B, C be V2() ManySortedSet of I; ::_thesis: for f being ManySortedFunction of A,B
for g being ManySortedFunction of B,C st g ** f is "onto" holds
g is "onto"
let f be ManySortedFunction of A,B; ::_thesis: for g being ManySortedFunction of B,C st g ** f is "onto" holds
g is "onto"
let g be ManySortedFunction of B,C; ::_thesis: ( g ** f is "onto" implies g is "onto" )
assume A1: g ** f is "onto" ; ::_thesis: g is "onto"
let i be set ; :: according to MSUALG_3:def_3 ::_thesis: ( not i in I or proj2 (g . i) = C . i )
assume A2: i in I ; ::_thesis: proj2 (g . i) = C . i
then A3: ( f . i is Function of (A . i),(B . i) & g . i is Function of (B . i),(C . i) ) by PBOOLE:def_15;
rng ((g . i) * (f . i)) = rng ((g ** f) . i) by A2, MSUALG_3:2
.= C . i by A1, A2, MSUALG_3:def_3 ;
hence  proj2 (g . i) = C . i by A2, A3, Th1; ::_thesis: verum
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 )
proof
let A, B be non empty set ; ::_thesis: 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 )
let C, y be set ; ::_thesis: 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 )
let f be Function; ::_thesis: ( f in Funcs (A,(Funcs (B,C))) & y in B implies ( dom ((commute f) . y) = A & rng ((commute f) . y) c= C ) )
assume that
A1: f in Funcs (A,(Funcs (B,C))) and
A2: y in B ; ::_thesis: ( dom ((commute f) . y) = A & rng ((commute f) . y) c= C )
set cf = commute f;
 commute f in Funcs (B,(Funcs (A,C))) by A1, FUNCT_6:55;
then A3: ex g being Function st
( g = commute f & dom g = B & rng g c= Funcs (A,C) ) by FUNCT_2:def_2;
then  (commute f) . y in rng (commute f) by A2, FUNCT_1:def_3;
then  ex t being Function st
( t = (commute f) . y & dom t = A & rng t c= C ) by A3, FUNCT_2:def_2;
hence  ( dom ((commute f) . y) = A & rng ((commute f) . y) c= C ) ; ::_thesis: verum
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
proof
let I be set ; ::_thesis: 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
let A, B be ManySortedSet of I; ::_thesis: ( A is_transformable_to B implies for f being ManySortedFunction of I st doms f = A & rngs f c= B holds
f is ManySortedFunction of A,B )
assume  for i being set st i in I & B . i = {} holds
A . i = {} ; :: according to PZFMISC1:def_3 ::_thesis: for f being ManySortedFunction of I st doms f = A & rngs f c= B holds
f is ManySortedFunction of A,B
let f be ManySortedFunction of I; ::_thesis: ( doms f = A & rngs f c= B implies f is ManySortedFunction of A,B )
assume that
A1: doms f = A and
A2: rngs f c= B ; ::_thesis: f is ManySortedFunction of A,B
let i be set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in I or f . i is Element of bool [:(A . i),(B . i):] )
assume A3: i in I ; ::_thesis: f . i is Element of bool [:(A . i),(B . i):]
then reconsider J = I as non empty set ;
reconsider s = i as Element of J by A3;
A4: dom (f . s) = A . s by A1, MSSUBFAM:14;
 rng (f . s) = (rngs f) . s by MSSUBFAM:13;
then  rng (f . s) c= B . s by A2, PBOOLE:def_2;
hence  f . i is Element of bool [:(A . i),(B . i):] by A4, FUNCT_2:2; ::_thesis: verum
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
proof
let I be set ; ::_thesis: 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
let A, B be ManySortedSet of I; ::_thesis: 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
let F be ManySortedFunction of A,B; ::_thesis: for C, E being ManySortedSubset of A
for D being ManySortedSubset of C st E = D holds
(F || C) || D = F || E
let C, E be ManySortedSubset of A; ::_thesis: for D being ManySortedSubset of C st E = D holds
(F || C) || D = F || E
let D be ManySortedSubset of C; ::_thesis: ( E = D implies (F || C) || D = F || E )
assume A1: E = D ; ::_thesis: (F || C) || D = F || E
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
((F_||_C)_||_D)_._i_=_(F_||_E)_._i
let i be set ; ::_thesis: ( i in I implies ((F || C) || D) . i = (F || E) . i )
assume A2: i in I ; ::_thesis: ((F || C) || D) . i = (F || E) . i
A3: F . i is Function of (A . i),(B . i) by A2, PBOOLE:def_15;
 D c= C by PBOOLE:def_18;
then A4: D . i c= C . i by A2, PBOOLE:def_2;
A5: (F || C) . i is Function of (C . i),(B . i) by A2, PBOOLE:def_15;
then reconsider fc = (F . i) | (C . i) as Function of (C . i),(B . i) by A2, A3, MSAFREE:def_1;
thus ((F || C) || D) . i = ((F || C) . i) | (D . i) by A2, A5, MSAFREE:def_1
.= fc | (D . i) by A2, A3, MSAFREE:def_1
.= (F . i) | (D . i) by A4, RELAT_1:74
.= (F || E) . i by A1, A2, A3, MSAFREE:def_1 ; ::_thesis: verum
end;
hence  (F || C) || D = F || E by PBOOLE:3; ::_thesis: verum
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
proof
let I be set ; ::_thesis: 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
let B be V2() ManySortedSet of I; ::_thesis: 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
let C be ManySortedSet of I; ::_thesis: for A being ManySortedSubset of C
for F being ManySortedFunction of A,B ex G being ManySortedFunction of C,B st G || A = F
let A be ManySortedSubset of C; ::_thesis: for F being ManySortedFunction of A,B ex G being ManySortedFunction of C,B st G || A = F
let F be ManySortedFunction of A,B; ::_thesis: ex G being ManySortedFunction of C,B st G || A = F
defpred S1[ set , set , set ] means  ex f being Function of (A . $3),(B . $3) st
( f = F . $3 & ( $2 in A . $3 implies $1 = f . $2 ) );
A1: for i being set st i in I holds
for x being set st x in C . i holds
ex y being set st
( y in B . i & S1[y,x,i] )
proof
let i be set ; ::_thesis: ( i in I implies for x being set st x in C . i holds
ex y being set st
( y in B . i & S1[y,x,i] ) )
assume A2: i in I ; ::_thesis: for x being set st x in C . i holds
ex y being set st
( y in B . i & S1[y,x,i] )
then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def_15;
let x be set ; ::_thesis: ( x in C . i implies ex y being set st
( y in B . i & S1[y,x,i] ) )
assume  x in C . i ; ::_thesis: ex y being set st
( y in B . i & S1[y,x,i] )
percases ( x in A . i or not x in A . i ) ;
supposeA3: x in A . i ; ::_thesis: ex y being set st
( y in B . i & S1[y,x,i] )
take  f . x ; ::_thesis: ( f . x in B . i & S1[f . x,x,i] )
thus  f . x in B . i by A2, A3, FUNCT_2:5; ::_thesis: S1[f . x,x,i]
take  f ; ::_thesis: ( f = F . i & ( x in A . i implies f . x = f . x ) )
thus  ( f = F . i & ( x in A . i implies f . x = f . x ) ) ; ::_thesis: verum
end;
supposeA4: not x in A . i ; ::_thesis: ex y being set st
( y in B . i & S1[y,x,i] )
consider y being set  such that
A5: y in B . i by A2, XBOOLE_0:def_1;
take  y ; ::_thesis: ( y in B . i & S1[y,x,i] )
thus  y in B . i by A5; ::_thesis: S1[y,x,i]
take  f ; ::_thesis: ( f = F . i & ( x in A . i implies y = f . x ) )
thus  ( f = F . i & ( x in A . i implies y = f . x ) ) by A4; ::_thesis: verum
end;
end;
end;
consider G being ManySortedFunction of C,B such that
A6: for i being set st i in I holds
ex g being Function of (C . i),(B . i) st
( g = G . i & ( for x being set st x in C . i holds
S1[g . x,x,i] ) ) from MSSUBFAM:sch_1(A1);
take  G ; ::_thesis: G || A = F
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(G_||_A)_._i_=_F_._i
let i be set ; ::_thesis: ( i in I implies (G || A) . i = F . i )
assume A7: i in I ; ::_thesis: (G || A) . i = F . i
then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def_15;
A8: dom f = A . i by A7, FUNCT_2:def_1;
consider g being Function of (C . i),(B . i) such that
A9: g = G . i and
A10: for x being set st x in C . i holds
S1[g . x,x,i] by A6, A7;
 A c= C by PBOOLE:def_18;
then A11: A . i c= C . i by A7, PBOOLE:def_2;
A12: for x being set st x in A . i holds
f . x = (g | (A . i)) . x
proof
let x be set ; ::_thesis: ( x in A . i implies f . x = (g | (A . i)) . x )
assume A13: x in A . i ; ::_thesis: f . x = (g | (A . i)) . x
then  ex h being Function of (A . i),(B . i) st
( h = F . i & ( x in A . i implies g . x = h . x ) ) by A10, A11;
hence  f . x = (g | (A . i)) . x by A13, FUNCT_1:49; ::_thesis: verum
end;
 dom g = C . i by A7, FUNCT_2:def_1;
then A14: dom (g | (A . i)) = A . i by A11, RELAT_1:62;
thus (G || A) . i = g | (A . i) by A7, A9, MSAFREE:def_1
.= F . i by A8, A14, A12, FUNCT_1:2 ; ::_thesis: verum
end;
hence  G || A = F by PBOOLE:3; ::_thesis: verum
end;

definition
let I be set ;
let A be ManySortedSet of I;
let F be ManySortedFunction of I;
funcF "" 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
 ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i = (F . i) " (A . i)
proof
deffunc H1( set ) ->  set = (F . $1) " (A . $1);
 ex f being ManySortedSet of I st
for i being set st i in I holds
f . i = H1(i) from PBOOLE:sch_4();
hence  ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i = (F . i) " (A . i) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = (F . i) " (A . i) ) & ( for i being set st i in I holds
b2 . i = (F . i) " (A . i) ) holds
b1 = b2
proof
let X, Y be ManySortedSet of I; ::_thesis: ( ( for i being set st i in I holds
X . i = (F . i) " (A . i) ) & ( for i being set st i in I holds
Y . i = (F . i) " (A . i) ) implies X = Y )
assume that
A1: for i being set st i in I holds
X . i = (F . i) " (A . i) and
A2: for i being set st i in I holds
Y . i = (F . i) " (A . i) ; ::_thesis: X = Y
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
X_._i_=_Y_._i
let i be set ; ::_thesis: ( i in I implies X . i = Y . i )
assume A3: i in I ; ::_thesis: X . i = Y . i
hence X . i = (F . i) " (A . i) by A1
.= Y . i by A2, A3 ;
::_thesis: verum
end;
hence  X = Y by PBOOLE:3; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines "" EQUATION:def_1_:_
 for I being set
for A being ManySortedSet of I
for F being ManySortedFunction of I
for b4 being ManySortedSet of I holds
( b4 = F "" A iff for i being set st i in I holds
b4 . i = (F . i) " (A . i) );

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
proof
let I be set ; ::_thesis: for A, B, C being ManySortedSet of I
for F being ManySortedFunction of A,B holds F .:.: C is ManySortedSubset of B
let A, B, C be ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,B holds F .:.: C is ManySortedSubset of B
let F be ManySortedFunction of A,B; ::_thesis: F .:.: C is ManySortedSubset of B
let i be set ; :: according to PBOOLE:def_2,PBOOLE:def_18 ::_thesis: ( not i in I or (F .:.: C) . i c= B . i )
assume A1: i in I ; ::_thesis: (F .:.: C) . i c= B . i
then reconsider J = I as non empty set ;
reconsider j = i as Element of J by A1;
reconsider A1 = A, B1 = B as ManySortedSet of J ;
reconsider F1 = F as ManySortedFunction of A1,B1 ;
 (F1 . j) .: (C . j) c= B . j ;
hence  (F .:.: C) . i c= B . i by PBOOLE:def_20; ::_thesis: verum
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
proof
let I be set ; ::_thesis: for A, B, C being ManySortedSet of I
for F being ManySortedFunction of A,B holds F "" C is ManySortedSubset of A
let A, B, C be ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,B holds F "" C is ManySortedSubset of A
let F be ManySortedFunction of A,B; ::_thesis: F "" C is ManySortedSubset of A
let i be set ; :: according to PBOOLE:def_2,PBOOLE:def_18 ::_thesis: ( not i in I or (F "" C) . i c= A . i )
assume A1: i in I ; ::_thesis: (F "" C) . i c= A . i
then reconsider J = I as non empty set ;
reconsider j = i as Element of J by A1;
reconsider A1 = A, B1 = B as ManySortedSet of J ;
reconsider F1 = F as ManySortedFunction of A1,B1 ;
 (F1 . j) " (C . j) c= A . j ;
hence  (F "" C) . i c= A . i by Def1; ::_thesis: verum
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
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I
for F being ManySortedFunction of A,B st F is "onto" holds
F .:.: A = B
let A, B be ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,B st F is "onto" holds
F .:.: A = B
let F be ManySortedFunction of A,B; ::_thesis: ( F is "onto" implies F .:.: A = B )
assume A1: F is "onto" ; ::_thesis: F .:.: A = B
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(F_.:.:_A)_._i_=_B_._i
let i be set ; ::_thesis: ( i in I implies (F .:.: A) . b1 = B . b1 )
assume A2: i in I ; ::_thesis: (F .:.: A) . b1 = B . b1
then A3: F . i is Function of (A . i),(B . i) by PBOOLE:def_15;
percases not ( B . i = {} & not A . i = {} & not ( B . i = {} & not A . i = {} ) ) ;
suppose ( B . i = {} implies A . i = {} ) ; ::_thesis: (F .:.: A) . b1 = B . b1
thus (F .:.: A) . i = (F . i) .: (A . i) by A2, PBOOLE:def_20
.= rng (F . i) by A3, RELSET_1:22
.= B . i by A1, A2, MSUALG_3:def_3 ; ::_thesis: verum
end;
supposeA4: ( B . i = {} & not A . i = {} ) ; ::_thesis: (F .:.: A) . b1 = B . b1
then A5: F . i = {} by A3;
thus (F .:.: A) . i = (F . i) .: (A . i) by A2, PBOOLE:def_20
.= B . i by A4, A5 ; ::_thesis: verum
end;
end;
end;
hence  F .:.: A = B by PBOOLE:3; ::_thesis: verum
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
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I
for F being ManySortedFunction of A,B st A is_transformable_to B holds
F "" B = A
let A, B be ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,B st A is_transformable_to B holds
F "" B = A
let F be ManySortedFunction of A,B; ::_thesis: ( A is_transformable_to B implies F "" B = A )
assume A1: A is_transformable_to B ; ::_thesis: F "" B = A
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(F_""_B)_._i_=_A_._i
let i be set ; ::_thesis: ( i in I implies (F "" B) . i = A . i )
assume A2: i in I ; ::_thesis: (F "" B) . i = A . i
then A3: F . i is Function of (A . i),(B . i) by PBOOLE:def_15;
A4: ( B . i = {} implies A . i = {} ) by A1, A2, PZFMISC1:def_3;
thus (F "" B) . i = (F . i) " (B . i) by A2, Def1
.= A . i by A4, A3, FUNCT_2:40 ; ::_thesis: verum
end;
hence  F "" B = A by PBOOLE:3; ::_thesis: verum
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
proof
let I be set ; ::_thesis: for A being ManySortedSet of I
for F being ManySortedFunction of I st A c= rngs F holds
F .:.: (F "" A) = A
let A be ManySortedSet of I; ::_thesis: for F being ManySortedFunction of I st A c= rngs F holds
F .:.: (F "" A) = A
let F be ManySortedFunction of I; ::_thesis: ( A c= rngs F implies F .:.: (F "" A) = A )
assume A1: A c= rngs F ; ::_thesis: F .:.: (F "" A) = A
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(F_.:.:_(F_""_A))_._i_=_A_._i
let i be set ; ::_thesis: ( i in I implies (F .:.: (F "" A)) . i = A . i )
assume A2: i in I ; ::_thesis: (F .:.: (F "" A)) . i = A . i
then  A . i c= (rngs F) . i by A1, PBOOLE:def_2;
then A3: A . i c= rng (F . i) by A2, MSSUBFAM:13;
thus (F .:.: (F "" A)) . i = (F . i) .: ((F "" A) . i) by A2, PBOOLE:def_20
.= (F . i) .: ((F . i) " (A . i)) by A2, Def1
.= A . i by A3, FUNCT_1:77 ; ::_thesis: verum
end;
hence  F .:.: (F "" A) = A by PBOOLE:3; ::_thesis: verum
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
proof
let I be set ; ::_thesis: for f being ManySortedFunction of I
for X being ManySortedSet of I holds f .:.: X c= rngs f
let f be ManySortedFunction of I; ::_thesis: for X being ManySortedSet of I holds f .:.: X c= rngs f
let X be ManySortedSet of I; ::_thesis: f .:.: X c= rngs f
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (f .:.: X) . i c= (rngs f) . i )
assume A1: i in I ; ::_thesis: (f .:.: X) . i c= (rngs f) . i
then  (f .:.: X) . i = (f . i) .: (X . i) by PBOOLE:def_20;
then  (f .:.: X) . i c= rng (f . i) by RELAT_1:111;
hence  (f .:.: X) . i c= (rngs f) . i by A1, MSSUBFAM:13; ::_thesis: verum
end;

theorem Th13: :: EQUATION:13
for I being set
for f being ManySortedFunction of I holds f .:.: (doms f) = rngs f
proof
let I be set ; ::_thesis: for f being ManySortedFunction of I holds f .:.: (doms f) = rngs f
let f be ManySortedFunction of I; ::_thesis: f .:.: (doms f) = rngs f
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(f_.:.:_(doms_f))_._i_=_(rngs_f)_._i
let i be set ; ::_thesis: ( i in I implies (f .:.: (doms f)) . i = (rngs f) . i )
assume A1: i in I ; ::_thesis: (f .:.: (doms f)) . i = (rngs f) . i
hence (f .:.: (doms f)) . i = (f . i) .: ((doms f) . i) by PBOOLE:def_20
.= (f . i) .: (dom (f . i)) by A1, MSSUBFAM:14
.= rng (f . i) by RELAT_1:113
.= (rngs f) . i by A1, MSSUBFAM:13 ;
::_thesis: verum
end;
hence  f .:.: (doms f) = rngs f by PBOOLE:3; ::_thesis: verum
end;

theorem Th14: :: EQUATION:14
for I being set
for f being ManySortedFunction of I holds f "" (rngs f) = doms f
proof
let I be set ; ::_thesis: for f being ManySortedFunction of I holds f "" (rngs f) = doms f
let f be ManySortedFunction of I; ::_thesis: f "" (rngs f) = doms f
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(f_""_(rngs_f))_._i_=_(doms_f)_._i
let i be set ; ::_thesis: ( i in I implies (f "" (rngs f)) . i = (doms f) . i )
assume A1: i in I ; ::_thesis: (f "" (rngs f)) . i = (doms f) . i
hence (f "" (rngs f)) . i = (f . i) " ((rngs f) . i) by Def1
.= (f . i) " (rng (f . i)) by A1, MSSUBFAM:13
.= dom (f . i) by RELAT_1:134
.= (doms f) . i by A1, MSSUBFAM:14 ;
::_thesis: verum
end;
hence  f "" (rngs f) = doms f by PBOOLE:3; ::_thesis: verum
end;

theorem :: EQUATION:15
for I being set
for A being ManySortedSet of I holds (id A) .:.: A = A
proof
let I be set ; ::_thesis: for A being ManySortedSet of I holds (id A) .:.: A = A
let A be ManySortedSet of I; ::_thesis: (id A) .:.: A = A
A1: rngs (id A) = A by EXTENS_1:9;
 doms (id A) = A by MSSUBFAM:17;
hence  (id A) .:.: A = A by A1, Th13; ::_thesis: verum
end;

theorem :: EQUATION:16
for I being set
for A being ManySortedSet of I holds (id A) "" A = A
proof
let I be set ; ::_thesis: for A being ManySortedSet of I holds (id A) "" A = A
let A be ManySortedSet of I; ::_thesis: (id A) "" A = A
A1: rngs (id A) = A by EXTENS_1:9;
 doms (id A) = A by MSSUBFAM:17;
hence  (id A) "" A = A by A1, Th14; ::_thesis: verum
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 #)
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra over S holds A is MSSubAlgebra of MSAlgebra(# the Sorts of A, the Charact of A #)
let A be MSAlgebra over S; ::_thesis: A is MSSubAlgebra of MSAlgebra(# the Sorts of A, the Charact of A #)
set IT = MSAlgebra(# the Sorts of A, the Charact of A #);
A1: MSAlgebra(# the Sorts of A, the Charact of A #) is MSSubAlgebra of MSAlgebra(# the Sorts of A, the Charact of A #) by MSUALG_2:5;
hence  the Sorts of A is MSSubset of MSAlgebra(# the Sorts of A, the Charact of A #) by MSUALG_2:def_9; :: according to MSUALG_2:def_9 ::_thesis: for b1 being ManySortedSubset of the Sorts of MSAlgebra(# the Sorts of A, the Charact of A #) holds
( not b1 = the Sorts of A or ( b1 is opers_closed & the Charact of A = Opers (MSAlgebra(# the Sorts of A, the Charact of A #),b1) ) )
let C be MSSubset of MSAlgebra(# the Sorts of A, the Charact of A #); ::_thesis: ( not C = the Sorts of A or ( C is opers_closed & the Charact of A = Opers (MSAlgebra(# the Sorts of A, the Charact of A #),C) ) )
assume A2: C = the Sorts of A ; ::_thesis: ( C is opers_closed & the Charact of A = Opers (MSAlgebra(# the Sorts of A, the Charact of A #),C) )
hence  C is opers_closed by A1, MSUALG_2:def_9; ::_thesis: the Charact of A = Opers (MSAlgebra(# the Sorts of A, the Charact of A #),C)
thus  the Charact of A = Opers (MSAlgebra(# the Sorts of A, the Charact of A #),C) by A1, A2, MSUALG_2:def_9; ::_thesis: verum
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)
proof
let S be non empty non void ManySortedSign ; ::_thesis: 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)
let U0 be MSAlgebra over S; ::_thesis: 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)
let A be MSSubAlgebra of U0; ::_thesis: for o being OperSymbol of S
for x being set st x in Args (o,A) holds
x in Args (o,U0)
let o be OperSymbol of S; ::_thesis: for x being set st x in Args (o,A) holds
x in Args (o,U0)
let x be set ; ::_thesis: ( x in Args (o,A) implies x in Args (o,U0) )
assume A1: x in Args (o,A) ; ::_thesis: x in Args (o,U0)
reconsider B0 = the Sorts of A as MSSubset of U0 by MSUALG_2:def_9;
 MSAlgebra(# the Sorts of U0, the Charact of U0 #) = MSAlgebra(# the Sorts of U0, the Charact of U0 #) ;
then  U0 is MSSubAlgebra of U0 by MSUALG_2:5;
then reconsider B1 = the Sorts of U0 as MSSubset of U0 by MSUALG_2:def_9;
 B0 c= B1 by PBOOLE:def_18;
then  ((B0 #) * the Arity of S) . o c= ((B1 #) * the Arity of S) . o by MSUALG_2:2;
hence  x in Args (o,U0) by A1; ::_thesis: verum
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
proof
let S be non empty non void ManySortedSign ; ::_thesis: 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
let U0 be MSAlgebra over S; ::_thesis: 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
let A be MSSubAlgebra of U0; ::_thesis: 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
let o be OperSymbol of S; ::_thesis: for x being set st x in Args (o,A) holds
(Den (o,A)) . x = (Den (o,U0)) . x
let x be set ; ::_thesis: ( x in Args (o,A) implies (Den (o,A)) . x = (Den (o,U0)) . x )
assume A1: x in Args (o,A) ; ::_thesis: (Den (o,A)) . x = (Den (o,U0)) . x
reconsider B = the Sorts of A as MSSubset of U0 by MSUALG_2:def_9;
 B is opers_closed by MSUALG_2:def_9;
then A2: B is_closed_on o by MSUALG_2:def_6;
thus (Den (o,A)) . x = ((Opers (U0,B)) . o) . x by MSUALG_2:def_9
.= (o /. B) . x by MSUALG_2:def_8
.= ((Den (o,U0)) | (((B #) * the Arity of S) . o)) . x by A2, MSUALG_2:def_7
.= (Den (o,U0)) . x by A1, FUNCT_1:49 ; ::_thesis: verum
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 )
proof
let I be set ; ::_thesis: 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 )
let S be non empty non void ManySortedSign ; ::_thesis: 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 )
let F be MSAlgebra-Family of I,S; ::_thesis: 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 )
let B be MSSubAlgebra of product F; ::_thesis: 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 )
let o be OperSymbol of S; ::_thesis: for x being set st x in Args (o,B) holds
( (Den (o,B)) . x is Function & (Den (o,(product F))) . x is Function )
let x be set ; ::_thesis: ( x in Args (o,B) implies ( (Den (o,B)) . x is Function & (Den (o,(product F))) . x is Function ) )
set r = the_result_sort_of o;
assume A1: x in Args (o,B) ; ::_thesis: ( (Den (o,B)) . x is Function & (Den (o,(product F))) . x is Function )
then  x in Args (o,(product F)) by Th18;
then  (Den (o,(product F))) . x in product (Carrier (F,(the_result_sort_of o))) by PRALG_3:19;
then  (Den (o,B)) . x in product (Carrier (F,(the_result_sort_of o))) by A1, Th19;
then reconsider p = (Den (o,B)) . x as Element of (SORTS F) . (the_result_sort_of o) by PRALG_2:def_10;
A2: p is Function ;
hence  (Den (o,B)) . x is Function ; ::_thesis: (Den (o,(product F))) . x is Function
thus  (Den (o,(product F))) . x is Function by A1, A2, Th19; ::_thesis: verum
end;

definition
let S be non empty non void ManySortedSign ;
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
 ex b1 being set st
for x being set holds
( x in b1 iff ex C being strict MSSubAlgebra of A st
( x = C & B is MSSubAlgebra of C ) )
proof
defpred S1[ set ] means  ex C being strict MSSubAlgebra of A st
( $1 = C & B is MSSubAlgebra of C );
consider IT being set  such that
A1: for x being set holds
( x in IT iff ( x in MSSub A & S1[x] ) ) from XBOOLE_0:sch_1();
take  IT ; ::_thesis: for x being set holds
( x in IT iff ex C being strict MSSubAlgebra of A st
( x = C & B is MSSubAlgebra of C ) )
let x be set ; ::_thesis: ( x in IT iff ex C being strict MSSubAlgebra of A st
( x = C & B is MSSubAlgebra of C ) )
thus  ( x in IT implies ex C being strict MSSubAlgebra of A st
( x = C & B is MSSubAlgebra of C ) ) by A1; ::_thesis: ( ex C being strict MSSubAlgebra of A st
( x = C & B is MSSubAlgebra of C ) implies x in IT )
given C being strict MSSubAlgebra of A such that A2: x = C and
A3: B is MSSubAlgebra of C ; ::_thesis: x in IT
 x in MSSub A by A2, MSUALG_2:def_19;
hence  x in IT by A1, A2, A3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ex C being strict MSSubAlgebra of A st
( x = C & B is MSSubAlgebra of C ) ) ) & ( for x being set holds
( x in b2 iff ex C being strict MSSubAlgebra of A st
( x = C & B is MSSubAlgebra of C ) ) ) holds
b1 = b2
proof
defpred S1[ set ] means  ex C being strict MSSubAlgebra of A st
( $1 = C & B is MSSubAlgebra of C );
 for X1, X2 being set st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from XBOOLE_0:sch_3();
hence  for b1, b2 being set st ( for x being set holds
( x in b1 iff ex C being strict MSSubAlgebra of A st
( x = C & B is MSSubAlgebra of C ) ) ) & ( for x being set holds
( x in b2 iff ex C being strict MSSubAlgebra of A st
( x = C & B is MSSubAlgebra of C ) ) ) holds
b1 = b2 ; ::_thesis: verum
end;
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 b4 being set holds
( b4 = SuperAlgebraSet B iff for x being set holds
( x in b4 iff ex C being strict MSSubAlgebra of A st
( 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;
cluster SuperAlgebraSet B ->  non empty ;
coherence
 not SuperAlgebraSet B is empty
proof
 MSAlgebra(# the Sorts of B, the Charact of B #) is MSSubAlgebra of B by MSUALG_2:37;
then A1: MSAlgebra(# the Sorts of B, the Charact of B #) is MSSubAlgebra of A by MSUALG_2:6;
 B is MSSubAlgebra of MSAlgebra(# the Sorts of B, the Charact of B #) by Th17;
hence  not SuperAlgebraSet B is empty by A1, Def2; ::_thesis: verum
end;
end;

registration
let S be non empty non void ManySortedSign ;
cluster strict non-empty free for MSAlgebra over S;
existence
 ex b1 being MSAlgebra over S st
( b1 is strict & b1 is non-empty & b1 is free )
proof
set X = the V2() ManySortedSet of the carrier of S;
take  FreeMSA the V2() ManySortedSet of the carrier of S ; ::_thesis: ( FreeMSA the V2() ManySortedSet of the carrier of S is strict & FreeMSA the V2() ManySortedSet of the carrier of S is non-empty & FreeMSA the V2() ManySortedSet of the carrier of S is free )
thus  ( FreeMSA the V2() ManySortedSet of the carrier of S is strict & FreeMSA the V2() ManySortedSet of the carrier of S is non-empty & FreeMSA the V2() ManySortedSet of the carrier of S is free ) ; ::_thesis: verum
end;
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;
cluster GenMSAlg X ->  finitely-generated ;
coherence
 GenMSAlg X is finitely-generated
proof
percases ( not S is void or S is void ) ;
:: according to MSAFREE2:def_10
case not S is void ; ::_thesis: for b1 being ManySortedSign holds
( not b1 = S or for b2 being MSAlgebra over b1 holds
( not b2 = GenMSAlg X or ex b3 being GeneratorSet of b2 st b3 is finite-yielding ) )
let S9 be non empty non void ManySortedSign ; ::_thesis: ( not S9 = S or for b1 being MSAlgebra over S9 holds
( not b1 = GenMSAlg X or ex b2 being GeneratorSet of b1 st b2 is finite-yielding ) )
assume A1: S9 = S ; ::_thesis: for b1 being MSAlgebra over S9 holds
( not b1 = GenMSAlg X or ex b2 being GeneratorSet of b1 st b2 is finite-yielding )
let H be MSAlgebra over S9; ::_thesis: ( not H = GenMSAlg X or ex b1 being GeneratorSet of H st b1 is finite-yielding )
assume A2: H = GenMSAlg X ; ::_thesis: ex b1 being GeneratorSet of H st b1 is finite-yielding
then reconsider T = X as MSSubset of H by A1, MSUALG_2:def_17;
 GenMSAlg T = H by A1, A2, EXTENS_1:18;
then reconsider T = T as GeneratorSet of H by A1, A2, MSAFREE:3;
take  T ; ::_thesis: T is finite-yielding
thus  T is finite-yielding ; ::_thesis: verum
end;
case S is void ; ::_thesis: the Sorts of (GenMSAlg X) is finite-yielding
hence  the Sorts of (GenMSAlg X) is finite-yielding ; ::_thesis: verum
end;
end;
end;
end;

registration
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
cluster strict non-empty finitely-generated for MSSubAlgebra of A;
existence
 ex b1 being MSSubAlgebra of A st
( b1 is strict & b1 is non-empty & b1 is finitely-generated )
proof
set G = the V2() V29() ManySortedSubset of the Sorts of A;
take  GenMSAlg the V2() V29() ManySortedSubset of the Sorts of A ; ::_thesis: ( GenMSAlg the V2() V29() ManySortedSubset of the Sorts of A is strict & GenMSAlg the V2() V29() ManySortedSubset of the Sorts of A is non-empty & GenMSAlg the V2() V29() ManySortedSubset of the Sorts of A is finitely-generated )
thus  ( GenMSAlg the V2() V29() ManySortedSubset of the Sorts of A is strict & GenMSAlg the V2() V29() ManySortedSubset of the Sorts of A is non-empty & GenMSAlg the V2() V29() ManySortedSubset of the Sorts of A is finitely-generated ) ; ::_thesis: verum
end;
end;

registration
let S be non empty non void ManySortedSign ;
let A be feasible MSAlgebra over S;
cluster feasible for MSSubAlgebra of A;
existence
 ex b1 being MSSubAlgebra of A st b1 is feasible
proof
 MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of A, the Charact of A #) ;
then reconsider B = A as MSSubAlgebra of A by MSUALG_2:5;
take  B ; ::_thesis: B is feasible
thus  B is feasible ; ::_thesis: verum
end;
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
proof
let S be non empty non void ManySortedSign ; ::_thesis: 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
let U0 be non-empty MSAlgebra over S; ::_thesis: 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
let A be MSAlgebra over S; ::_thesis: 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
let C be MSSubAlgebra of A; ::_thesis: 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
let D be ManySortedSubset of the Sorts of A; ::_thesis: ( D = the Sorts of C implies 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 )
assume A1: D = the Sorts of C ; ::_thesis: 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
let h be ManySortedFunction of A,U0; ::_thesis: 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
let g be ManySortedFunction of C,U0; ::_thesis: ( g = h || D implies 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 )
assume A2: g = h || D ; ::_thesis: 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
let o be OperSymbol of S; ::_thesis: 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
let x be Element of Args (o,A); ::_thesis: for y being Element of Args (o,C) st Args (o,C) <> {} & x = y holds
h # x = g # y
let y be Element of Args (o,C); ::_thesis: ( Args (o,C) <> {} & x = y implies h # x = g # y )
assume that
A3: Args (o,C) <> {} and
A4: x = y ; ::_thesis: h # x = g # y
set hx = h # x;
set gy = g # y;
set ar = the_arity_of o;
A5: y in Args (o,A) by A3, Th18;
then reconsider xx = x, yy = y as Function by MSUALG_6:1;
A6: dom yy = dom (the_arity_of o) by A3, MSUALG_3:6;
A7: dom xx = dom (the_arity_of o) by A5, MSUALG_3:6;
A8: now__::_thesis:_for_n_being_set_st_n_in_dom_(the_arity_of_o)_holds_
(h_#_x)_._n_=_(g_#_y)_._n
let n be set ; ::_thesis: ( n in dom (the_arity_of o) implies (h # x) . n = (g # y) . n )
assume A9: n in dom (the_arity_of o) ; ::_thesis: (h # x) . n = (g # y) . n
then reconsider n9 = n as Nat ;
reconsider hn = h . ((the_arity_of o) . n) as Function of ( the Sorts of A . ((the_arity_of o) . n)),( the Sorts of U0 . ((the_arity_of o) . n)) by A9, PARTFUN1:4, PBOOLE:def_15;
 (the_arity_of o) . n in the carrier of S by A9, PARTFUN1:4;
then A10: g . ((the_arity_of o) . n9) = hn | (D . ((the_arity_of o) . n)) by A2, MSAFREE:def_1;
 dom ( the Sorts of C * (the_arity_of o)) = dom (the_arity_of o) by PARTFUN1:def_2;
then  xx . n in ( the Sorts of C * (the_arity_of o)) . n by A3, A4, A9, MSUALG_3:6;
then A11: xx . n in D . ((the_arity_of o) . n) by A1, A9, FUNCT_1:13;
thus (h # x) . n = (h # x) . n9
.= (h . ((the_arity_of o) /. n)) . (xx . n) by A5, A7, A9, MSUALG_3:24
.= (h . ((the_arity_of o) . n)) . (xx . n) by A9, PARTFUN1:def_6
.= (g . ((the_arity_of o) . n)) . (xx . n) by A10, A11, FUNCT_1:49
.= (g . ((the_arity_of o) /. n)) . (yy . n) by A4, A9, PARTFUN1:def_6
.= (g # y) . n9 by A3, A6, A9, MSUALG_3:24
.= (g # y) . n ; ::_thesis: verum
end;
 ( dom (h # x) = dom (the_arity_of o) & dom (g # y) = dom (the_arity_of o) ) by MSUALG_3:6;
hence  h # x = g # y by A8, FUNCT_1:2; ::_thesis: verum
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
proof
let S be non empty non void ManySortedSign ; ::_thesis: 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
let U0 be non-empty MSAlgebra over S; ::_thesis: 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
let A be feasible MSAlgebra over S; ::_thesis: 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
let C be feasible MSSubAlgebra of A; ::_thesis: 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
let D be ManySortedSubset of the Sorts of A; ::_thesis: ( D = the Sorts of C implies 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 )
assume A1: D = the Sorts of C ; ::_thesis: 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
let h be ManySortedFunction of A,U0; ::_thesis: ( h is_homomorphism A,U0 implies for g being ManySortedFunction of C,U0 st g = h || D holds
g is_homomorphism C,U0 )
assume A2: h is_homomorphism A,U0 ; ::_thesis: for g being ManySortedFunction of C,U0 st g = h || D holds
g is_homomorphism C,U0
let g be ManySortedFunction of C,U0; ::_thesis: ( g = h || D implies g is_homomorphism C,U0 )
assume A3: g = h || D ; ::_thesis: g is_homomorphism C,U0
let o be OperSymbol of S; :: according to MSUALG_3:def_7 ::_thesis: ( Args (o,C) = {} or for b1 being Element of Args (o,C) holds (g . (the_result_sort_of o)) . ((Den (o,C)) . b1) = (Den (o,U0)) . (g # b1) )
assume A4: Args (o,C) <> {} ; ::_thesis: for b1 being Element of Args (o,C) holds (g . (the_result_sort_of o)) . ((Den (o,C)) . b1) = (Den (o,U0)) . (g # b1)
let x be Element of Args (o,C); ::_thesis: (g . (the_result_sort_of o)) . ((Den (o,C)) . x) = (Den (o,U0)) . (g # x)
reconsider y = x as Element of Args (o,A) by A4, Th18;
set r = the_result_sort_of o;
A5: x in Args (o,A) by A4, Th18;
 Result (o,C) <> {} by A4, MSUALG_6:def_1;
then  (Den (o,C)) . x in Result (o,C) by A4, FUNCT_2:5;
then A6: (Den (o,C)) . x in the Sorts of C . ( the ResultSort of S . o) by FUNCT_2:15;
 (Den (o,A)) . x = (Den (o,C)) . x by A4, Th19;
hence (g . (the_result_sort_of o)) . ((Den (o,C)) . x) = (h . (the_result_sort_of o)) . ((Den (o,A)) . x) by A1, A3, A6, INSTALG1:39
.= (Den (o,U0)) . (h # y) by A2, A5, MSUALG_3:def_7
.= (Den (o,U0)) . (g # x) by A1, A3, A4, Th21 ;
::_thesis: verum
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
proof
let S be non empty non void ManySortedSign ; ::_thesis: 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
let U0 be non-empty MSAlgebra over S; ::_thesis: 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
let B be strict non-empty MSAlgebra over S; ::_thesis: 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
let G be GeneratorSet of U0; ::_thesis: 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
let H be V2() GeneratorSet of B; ::_thesis: for f being ManySortedFunction of U0,B st H c= f .:.: G & f is_homomorphism U0,B holds
f is_epimorphism U0,B
let f be ManySortedFunction of U0,B; ::_thesis: ( H c= f .:.: G & f is_homomorphism U0,B implies f is_epimorphism U0,B )
assume that
A1: H c= f .:.: G and
A2: f is_homomorphism U0,B ; ::_thesis: f is_epimorphism U0,B
reconsider I = the Sorts of (Image f) as V2() MSSubset of B by MSUALG_2:def_9;
 f .:.: G c= f .:.: the Sorts of U0 by EXTENS_1:2;
then  H c= f .:.: the Sorts of U0 by A1, PBOOLE:13;
then  H c= the Sorts of (Image f) by A2, MSUALG_3:def_12;
then  H is ManySortedSubset of the Sorts of (Image f) by PBOOLE:def_18;
then A3: GenMSAlg H is MSSubAlgebra of GenMSAlg I by EXTENS_1:17;
reconsider I1 = the Sorts of (Image f) as V2() MSSubset of (Image f) by PBOOLE:def_18;
 ( I is GeneratorSet of Image f & GenMSAlg I = GenMSAlg I1 ) by EXTENS_1:18, MSAFREE2:6;
then  GenMSAlg I = Image f by MSAFREE:3;
then  B is MSSubAlgebra of Image f by A3, MSAFREE:3;
then  Image f = B by MSUALG_2:7;
hence  f is_epimorphism U0,B by A2, MSUALG_3:19; ::_thesis: verum
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 )
proof
let S be non empty non void ManySortedSign ; ::_thesis: 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 )
let U0, U1 be non-empty MSAlgebra over S; ::_thesis: 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 )
let W be strict non-empty free MSAlgebra over S; ::_thesis: 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 )
let F be ManySortedFunction of U0,U1; ::_thesis: ( F is_epimorphism U0,U1 implies 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 ) )
assume A1: F is_epimorphism U0,U1 ; ::_thesis: 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 )
set sU0 = the Sorts of U0;
set sU1 = the Sorts of U1;
set I = the carrier of S;
let G be ManySortedFunction of W,U1; ::_thesis: ( G is_homomorphism W,U1 implies ex H being ManySortedFunction of W,U0 st
( H is_homomorphism W,U0 & G = F ** H ) )
assume A2: G is_homomorphism W,U1 ; ::_thesis: ex H being ManySortedFunction of W,U0 st
( H is_homomorphism W,U0 & G = F ** H )
consider Gen being GeneratorSet of W such that
A3: Gen is free by MSAFREE:def_6;
defpred S1[ set , set , set ] means  ex f being Function of ( the Sorts of U0 . $3),( the Sorts of U1 . $3) ex g being Function of (Gen . $3),( the Sorts of U1 . $3) st
( f = F . $3 & g = (G || Gen) . $3 & $1 in f " {(g . $2)} );
A4: for i being set st i in the carrier of S holds
for x being set st x in Gen . i holds
ex y being set st
( y in the Sorts of U0 . i & S1[y,x,i] )
proof
let i be set ; ::_thesis: ( i in the carrier of S implies for x being set st x in Gen . i holds
ex y being set st
( y in the Sorts of U0 . i & S1[y,x,i] ) )
assume A5: i in the carrier of S ; ::_thesis: for x being set st x in Gen . i holds
ex y being set st
( y in the Sorts of U0 . i & S1[y,x,i] )
reconsider g = (G || Gen) . i as Function of (Gen . i),( the Sorts of U1 . i) by A5, PBOOLE:def_15;
reconsider f = F . i as Function of ( the Sorts of U0 . i),( the Sorts of U1 . i) by A5, PBOOLE:def_15;
let x be set ; ::_thesis: ( x in Gen . i implies ex y being set st
( y in the Sorts of U0 . i & S1[y,x,i] ) )
assume  x in Gen . i ; ::_thesis: ex y being set st
( y in the Sorts of U0 . i & S1[y,x,i] )
then A6: g . x in the Sorts of U1 . i by A5, FUNCT_2:5;
 F is "onto" by A1, MSUALG_3:def_8;
then  rng (F . i) = the Sorts of U1 . i by A5, MSUALG_3:def_3;
then  f " {(g . x)} <> {} by A6, FUNCT_2:41;
then consider y being set  such that
A7: y in f " {(g . x)} by XBOOLE_0:def_1;
take  y ; ::_thesis: ( y in the Sorts of U0 . i & S1[y,x,i] )
thus  y in the Sorts of U0 . i by A7; ::_thesis: S1[y,x,i]
thus  S1[y,x,i] by A7; ::_thesis: verum
end;
consider H being ManySortedFunction of Gen, the Sorts of U0 such that
A8: for i being set st i in the carrier of S holds
ex h being Function of (Gen . i),( the Sorts of U0 . i) st
( h = H . i & ( for x being set st x in Gen . i holds
S1[h . x,x,i] ) ) from MSSUBFAM:sch_1(A4);
consider H1 being ManySortedFunction of W,U0 such that
A9: H1 is_homomorphism W,U0 and
A10: H1 || Gen = H by A3, MSAFREE:def_5;
now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_
(G_||_Gen)_._i_=_(F_**_H)_._i
let i be set ; ::_thesis: ( i in the carrier of S implies (G || Gen) . i = (F ** H) . i )
assume A11: i in the carrier of S ; ::_thesis: (G || Gen) . i = (F ** H) . i
then reconsider f9 = F . i as Function of ( the Sorts of U0 . i),( the Sorts of U1 . i) by PBOOLE:def_15;
reconsider g9 = (G || Gen) . i as Function of (Gen . i),( the Sorts of U1 . i) by A11, PBOOLE:def_15;
consider h being Function of (Gen . i),( the Sorts of U0 . i) such that
A12: h = H . i and
A13: for x being set st x in Gen . i holds
ex f being Function of ( the Sorts of U0 . i),( the Sorts of U1 . i) ex g being Function of (Gen . i),( the Sorts of U1 . i) st
( f = F . i & g = (G || Gen) . i & h . x in f " {(g . x)} ) by A8, A11;
A14: now__::_thesis:_for_x_being_set_st_x_in_Gen_._i_holds_
(f9_*_h)_._x_=_g9_._x
let x be set ; ::_thesis: ( x in Gen . i implies (f9 * h) . x = g9 . x )
assume A15: x in Gen . i ; ::_thesis: (f9 * h) . x = g9 . x
then consider f being Function of ( the Sorts of U0 . i),( the Sorts of U1 . i), g being Function of (Gen . i),( the Sorts of U1 . i) such that
A16: ( f = F . i & g = (G || Gen) . i ) and
A17: h . x in f " {(g . x)} by A13;
 f . (h . x) in {(g . x)} by A11, A17, FUNCT_2:38;
then  f . (h . x) = g . x by TARSKI:def_1;
hence  (f9 * h) . x = g9 . x by A15, A16, A17, FUNCT_2:15; ::_thesis: verum
end;
 ( Gen . i = dom g9 & Gen . i = dom (f9 * h) ) by A11, FUNCT_2:def_1;
then  g9 = f9 * h by A14, FUNCT_1:2;
hence  (G || Gen) . i = (F ** H) . i by A11, A12, MSUALG_3:2; ::_thesis: verum
end;
then  G || Gen = F ** (H1 || Gen) by A10, PBOOLE:3;
then A18: G || Gen = (F ** H1) || Gen by EXTENS_1:4;
take  H1 ; ::_thesis: ( H1 is_homomorphism W,U0 & G = F ** H1 )
thus  H1 is_homomorphism W,U0 by A9; ::_thesis: G = F ** H1
 F is_homomorphism U0,U1 by A1, MSUALG_3:def_8;
then  F ** H1 is_homomorphism W,U1 by A9, MSUALG_3:10;
hence  G = F ** H1 by A2, A18, EXTENS_1:19; ::_thesis: verum
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
proof
let S be non empty non void ManySortedSign ; ::_thesis: 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
let I be non empty finite set ; ::_thesis: 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
let A be non-empty MSAlgebra over S; ::_thesis: 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
let F be MSAlgebra-Family of I,S; ::_thesis: ( ( for i being Element of I ex C being strict non-empty finitely-generated MSSubAlgebra of A st C = F . i ) implies 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 )
assume A1: for i being Element of I ex C being strict non-empty finitely-generated MSSubAlgebra of A st C = F . i ; ::_thesis: 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
set Z =  {  C where C is Element of MSSub A : ex i being Element of I ex D being strict non-empty finitely-generated MSSubAlgebra of A st
( C = F . i & C = D )  }  ;
set J = the carrier of S;
set m = the Element of I;
consider W being strict non-empty finitely-generated MSSubAlgebra of A such that
A2: W = F . the Element of I by A1;
 W is Element of MSSub A by MSUALG_2:def_19;
then  W in  {  C where C is Element of MSSub A : ex i being Element of I ex D being strict non-empty finitely-generated MSSubAlgebra of A st
( C = F . i & C = D )  }  by A2;
then reconsider Z =  {  C where C is Element of MSSub A : ex i being Element of I ex D being strict non-empty finitely-generated MSSubAlgebra of A st
( C = F . i & C = D )  }  as non empty set ;
defpred S1[ set , set ] means  ex Q being strict non-empty MSSubAlgebra of A ex G being GeneratorSet of Q st
( $1 = Q & $2 = G & G is V2() & G is V29() );
A3: for a being Element of Z ex b being Element of Bool the Sorts of A st S1[a,b]
proof
let a be Element of Z; ::_thesis: ex b being Element of Bool the Sorts of A st S1[a,b]
 a in Z ;
then consider C being Element of MSSub A such that
A4: a = C and
A5: ex i being Element of I ex D being strict non-empty finitely-generated MSSubAlgebra of A st
( C = F . i & C = D ) ;
consider i being Element of I, D being strict non-empty finitely-generated MSSubAlgebra of A such that
 C = F . i and
A6: C = D by A5;
consider G being GeneratorSet of D such that
A7: G is V29() by MSAFREE2:def_10;
consider S being V2() V29() ManySortedSubset of the Sorts of D such that
A8: G c= S by A7, MSUALG_9:7;
 the Sorts of D is MSSubset of A by MSUALG_2:def_9;
then  ( S c= the Sorts of D & the Sorts of D c= the Sorts of A ) by PBOOLE:def_18;
then  S c= the Sorts of A by PBOOLE:13;
then  S is ManySortedSubset of the Sorts of A by PBOOLE:def_18;
then reconsider b = S as Element of Bool the Sorts of A by CLOSURE2:def_1;
reconsider S = S as GeneratorSet of D by A8, MSSCYC_1:21;
take  b ; ::_thesis: S1[a,b]
take  D ; ::_thesis: ex G being GeneratorSet of D st
( a = D & b = G & G is V2() & G is V29() )
take  S ; ::_thesis: ( a = D & b = S & S is V2() & S is V29() )
thus  a = D by A4, A6; ::_thesis: ( b = S & S is V2() & S is V29() )
thus  ( b = S & S is V2() & S is V29() ) ; ::_thesis: verum
end;
consider f being Function of Z,(Bool the Sorts of A) such that
A9: for B being Element of Z holds S1[B,f . B] from FUNCT_2:sch_3(A3);
deffunc H1( set ) ->  set = union  {  a where a is Element of bool ( the Sorts of A . $1) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . $1 )  }  ;
consider SOR being ManySortedSet of the carrier of S such that
A10: for j being set st j in the carrier of S holds
SOR . j = H1(j) from PBOOLE:sch_4();
 SOR is ManySortedSubset of the Sorts of A
proof
let j be set ; :: according to PBOOLE:def_2,PBOOLE:def_18 ::_thesis: ( not j in the carrier of S or SOR . j c= the Sorts of A . j )
assume A11: j in the carrier of S ; ::_thesis: SOR . j c= the Sorts of A . j
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in SOR . j or q in the Sorts of A . j )
set UU =  {  a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j )  }  ;
assume  q in SOR . j ; ::_thesis: q in the Sorts of A . j
then  q in union  {  a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j )  }  by A10, A11;
then consider w being set  such that
A12: q in w and
A13: w in  {  a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j )  }  by TARSKI:def_4;
consider a being Element of bool ( the Sorts of A . j) such that
A14: w = a and
 ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j ) by A13;
thus  q in the Sorts of A . j by A12, A14; ::_thesis: verum
end;
then reconsider SOR = SOR as MSSubset of A ;
 SOR is V2()
proof
set i = the Element of I;
consider C being strict non-empty finitely-generated MSSubAlgebra of A such that
A15: C = F . the Element of I by A1;
 C is Element of MSSub A by MSUALG_2:def_19;
then A16: F . the Element of I in Z by A15;
then A17: ex Q being strict non-empty MSSubAlgebra of A ex G being GeneratorSet of Q st
( F . the Element of I = Q & f . (F . the Element of I) = G & G is V2() & G is V29() ) by A9;
then reconsider G1 = f . (F . the Element of I) as V29() Element of Bool the Sorts of A by A16, FUNCT_2:5;
let j be set ; :: according to PBOOLE:def_13 ::_thesis: ( not j in the carrier of S or not SOR . j is empty )
assume A18: j in the carrier of S ; ::_thesis: not SOR . j is empty
consider q being set  such that
A19: q in G1 . j by A18, A17, XBOOLE_0:def_1;
set UU =  {  a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j )  }  ;
 G1 c= the Sorts of A by PBOOLE:def_18;
then  G1 . j c= the Sorts of A . j by A18, PBOOLE:def_2;
then  G1 . j in  {  a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j )  }  ;
then  q in union  {  a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j )  }  by A19, TARSKI:def_4;
hence  not SOR . j is empty by A10, A18; ::_thesis: verum
end;
then reconsider SOR = SOR as V2() MSSubset of A ;
A20: now__::_thesis:_for_j_being_set_st_j_in_the_carrier_of_S_holds_
not__{__a_where_a_is_Element_of_bool_(_the_Sorts_of_A_._j)_:_ex_i_being_Element_of_I_ex_K_being_ManySortedSet_of_the_carrier_of_S_st_
(_K_=_f_._(F_._i)_&_a_=_K_._j_)__}__is_empty
set i = the Element of I;
let j be set ; ::_thesis: ( j in the carrier of S implies not  {  a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j )  }  is empty )
assume A21: j in the carrier of S ; ::_thesis: not  {  a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j )  }  is empty
set UU =  {  a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j )  }  ;
consider C being strict non-empty finitely-generated MSSubAlgebra of A such that
A22: C = F . the Element of I by A1;
 C is Element of MSSub A by MSUALG_2:def_19;
then A23: F . the Element of I in Z by A22;
then  ex Q being strict non-empty MSSubAlgebra of A ex G being GeneratorSet of Q st
( F . the Element of I = Q & f . (F . the Element of I) = G & G is V2() & G is V29() ) by A9;
then reconsider G1 = f . (F . the Element of I) as V29() Element of Bool the Sorts of A by A23, FUNCT_2:5;
 G1 c= the Sorts of A by PBOOLE:def_18;
then  G1 . j c= the Sorts of A . j by A21, PBOOLE:def_2;
then  G1 . j in  {  a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j )  }  ;
hence  not  {  a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j )  }  is empty ; ::_thesis: verum
end;
 SOR is V29()
proof
let j be set ; :: according to FINSET_1:def_5 ::_thesis: ( not j in the carrier of S or SOR . j is finite )
assume A24: j in the carrier of S ; ::_thesis: SOR . j is finite
set UU =  {  a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j )  }  ;
reconsider VV =  {  a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j )  }  as non empty set by A20, A24;
A25: now__::_thesis:_ex_p_being_FinSequence_st_rng_p_=_VV
defpred S2[ set , set ] means  ex L being ManySortedSet of the carrier of S st
( f . (F . $1) = L & $2 = L . j );
consider r being FinSequence such that
A26: rng r = I by FINSEQ_1:52;
A27: for a being Element of I ex b being Element of VV st S2[a,b]
proof
let a be Element of I; ::_thesis: ex b being Element of VV st S2[a,b]
consider W being strict non-empty finitely-generated MSSubAlgebra of A such that
A28: W = F . a by A1;
 W is Element of MSSub A by MSUALG_2:def_19;
then A29: W in Z by A28;
then  ex Q being strict non-empty MSSubAlgebra of A ex G being GeneratorSet of Q st
( W = Q & f . W = G & G is V2() & G is V29() ) by A9;
then reconsider G1 = f . (F . a) as V29() Element of Bool the Sorts of A by A28, A29, FUNCT_2:5;
 G1 c= the Sorts of A by PBOOLE:def_18;
then  G1 . j c= the Sorts of A . j by A24, PBOOLE:def_2;
then  G1 . j in  {  a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j )  }  ;
then reconsider b = G1 . j as Element of VV ;
take  b ; ::_thesis: S2[a,b]
take  G1 ; ::_thesis: ( f . (F . a) = G1 & b = G1 . j )
thus  ( f . (F . a) = G1 & b = G1 . j ) ; ::_thesis: verum
end;
consider h being Function of I,VV such that
A30: for i being Element of I holds S2[i,h . i] from FUNCT_2:sch_3(A27);
A31: rng r = dom h by A26, FUNCT_2:def_1;
then reconsider p = h * r as FinSequence by FINSEQ_1:16;
A32: VV c= rng p
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in VV or q in rng p )
assume  q in VV ; ::_thesis: q in rng p
then consider a being Element of bool ( the Sorts of A . j) such that
A33: q = a and
A34: ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j ) ;
consider i being Element of I, K being ManySortedSet of the carrier of S such that
A35: ( K = f . (F . i) & a = K . j ) by A34;
A36: ( rng p = rng h & dom h = I ) by A31, FUNCT_2:def_1, RELAT_1:28;
 ex L being ManySortedSet of the carrier of S st
( f . (F . i) = L & h . i = L . j ) by A30;
hence  q in rng p by A33, A35, A36, FUNCT_1:def_3; ::_thesis: verum
end;
take p = p; ::_thesis: rng p = VV
 rng p c= rng h
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in rng p or q in rng h )
assume  q in rng p ; ::_thesis: q in rng h
hence  q in rng h by FUNCT_1:14; ::_thesis: verum
end;
then  rng p c= VV by XBOOLE_1:1;
hence  rng p = VV by A32, XBOOLE_0:def_10; ::_thesis: verum
end;
 for x being set st x in  {  a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j )  }  holds
x is finite
proof
let x be set ; ::_thesis: ( x in  {  a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j )  }  implies x is finite )
assume  x in  {  a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j )  }  ; ::_thesis: x is finite
then consider a being Element of bool ( the Sorts of A . j) such that
A37: x = a and
A38: ex w being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . w) & a = K . j ) ;
consider w being Element of I, K being ManySortedSet of the carrier of S such that
A39: ( K = f . (F . w) & a = K . j ) by A38;
A40: ex E being strict non-empty finitely-generated MSSubAlgebra of A st E = F . w by A1;
then  F . w is Element of MSSub A by MSUALG_2:def_19;
then  F . w in Z by A40;
then  S1[F . w,f . (F . w)] by A9;
hence  x is finite by A37, A39; ::_thesis: verum
end;
then  union  {  a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j )  }  is finite by A25, FINSET_1:7;
hence  SOR . j is finite by A10, A24; ::_thesis: verum
end;
then reconsider SOR = SOR as V2() V29() MSSubset of A ;
take  GenMSAlg SOR ; ::_thesis: for i being Element of I holds F . i is MSSubAlgebra of GenMSAlg SOR
let i be Element of I; ::_thesis: F . i is MSSubAlgebra of GenMSAlg SOR
consider C being strict non-empty finitely-generated MSSubAlgebra of A such that
A41: C = F . i by A1;
 C is Element of MSSub A by MSUALG_2:def_19;
then  F . i in Z by A41;
then consider Q being strict non-empty MSSubAlgebra of A, G being GeneratorSet of Q such that
A42: F . i = Q and
A43: f . (F . i) = G and
A44: ( G is V2() & G is V29() ) by A9;
 the Sorts of Q is MSSubset of A by MSUALG_2:def_9;
then  ( G c= the Sorts of Q & the Sorts of Q c= the Sorts of A ) by PBOOLE:def_18;
then A45: G c= the Sorts of A by PBOOLE:13;
then reconsider G1 = G as V2() MSSubset of A by A44, PBOOLE:def_18;
A46: G1 is ManySortedSubset of SOR
proof
let j be set ; :: according to PBOOLE:def_2,PBOOLE:def_18 ::_thesis: ( not j in the carrier of S or G1 . j c= SOR . j )
assume A47: j in the carrier of S ; ::_thesis: G1 . j c= SOR . j
set UU =  {  a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j )  }  ;
 G1 . j c= the Sorts of A . j by A45, A47, PBOOLE:def_2;
then A48: G1 . j in  {  a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j )  }  by A43;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in G1 . j or q in SOR . j )
assume  q in G1 . j ; ::_thesis: q in SOR . j
then  q in union  {  a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j )  }  by A48, TARSKI:def_4;
hence  q in SOR . j by A10, A47; ::_thesis: verum
end;
C = GenMSAlg G by A41, A42, MSAFREE:3
.= GenMSAlg G1 by EXTENS_1:18 ;
hence  F . i is MSSubAlgebra of GenMSAlg SOR by A41, A46, EXTENS_1:17; ::_thesis: verum
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 )
proof
let S be non empty non void ManySortedSign ; ::_thesis: 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 )
let U0 be non-empty MSAlgebra over S; ::_thesis: 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 )
let A, B be strict non-empty finitely-generated MSSubAlgebra of U0; ::_thesis: ex M being strict non-empty finitely-generated MSSubAlgebra of U0 st
( A is MSSubAlgebra of M & B is MSSubAlgebra of M )
defpred S1[ set , set ] means ( ( $1 = 0 implies $2 = A ) & ( $1 = 1 implies $2 = B ) );
A1: for i being set st i in {0,1} holds
ex j being set st S1[i,j]
proof
let i be set ; ::_thesis: ( i in {0,1} implies ex j being set st S1[i,j] )
assume A2: i in {0,1} ; ::_thesis: ex j being set st S1[i,j]
percases ( i = 0 or i = 1 ) by A2, TARSKI:def_2;
supposeA3: i = 0 ; ::_thesis: ex j being set st S1[i,j]
take  A ; ::_thesis: S1[i,A]
thus  S1[i,A] by A3; ::_thesis: verum
end;
supposeA4: i = 1 ; ::_thesis: ex j being set st S1[i,j]
take  B ; ::_thesis: S1[i,B]
thus  S1[i,B] by A4; ::_thesis: verum
end;
end;
end;
consider F being ManySortedSet of {0,1} such that
A5: for i being set st i in {0,1} holds
S1[i,F . i] from PBOOLE:sch_3(A1);
 F is MSAlgebra-Family of {0,1},S
proof
let i be set ; :: according to PRALG_2:def_5 ::_thesis: ( not i in {0,1} or F . i is MSAlgebra over S )
assume A6: i in {0,1} ; ::_thesis: F . i is MSAlgebra over S
then A7: ( i = 1 implies F . i = B ) by A5;
 ( i = 0 implies F . i = A ) by A5, A6;
hence  F . i is MSAlgebra over S by A6, A7, TARSKI:def_2; ::_thesis: verum
end;
then reconsider F = F as MSAlgebra-Family of {0,1},S ;
 for i being Element of {0,1} ex C being strict non-empty finitely-generated MSSubAlgebra of U0 st C = F . i
proof
let i be Element of {0,1}; ::_thesis: ex C being strict non-empty finitely-generated MSSubAlgebra of U0 st C = F . i
percases ( i = 0 or i = 1 ) by TARSKI:def_2;
supposeA8: i = 0 ; ::_thesis: ex C being strict non-empty finitely-generated MSSubAlgebra of U0 st C = F . i
take  A ; ::_thesis: A = F . i
thus  A = F . i by A5, A8; ::_thesis: verum
end;
supposeA9: i = 1 ; ::_thesis: ex C being strict non-empty finitely-generated MSSubAlgebra of U0 st C = F . i
take  B ; ::_thesis: B = F . i
thus  B = F . i by A5, A9; ::_thesis: verum
end;
end;
end;
then consider M being strict non-empty finitely-generated MSSubAlgebra of U0 such that
A10: for i being Element of {0,1} holds F . i is MSSubAlgebra of M by Th25;
take  M ; ::_thesis: ( A is MSSubAlgebra of M & B is MSSubAlgebra of M )
A11: 0 in {0,1} by TARSKI:def_2;
then  F . 0 = A by A5;
hence  A is MSSubAlgebra of M by A10, A11; ::_thesis: B is MSSubAlgebra of M
A12: 1 in {0,1} by TARSKI:def_2;
then  F . 1 = B by A5;
hence  B is MSSubAlgebra of M by A10, A12; ::_thesis: verum
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
proof
let SG be non empty non void ManySortedSign ; ::_thesis: 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
let AG be non-empty MSAlgebra over SG; ::_thesis: 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
let C be set ; ::_thesis: ( C =  {  A where A is Element of MSSub AG : ex R being strict non-empty finitely-generated MSSubAlgebra of AG st R = A  }  implies 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 )
assume A1: C =  {  A where A is Element of MSSub AG : ex R being strict non-empty finitely-generated MSSubAlgebra of AG st R = A  }  ; ::_thesis: 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
A2: now__::_thesis:_for_A_being_strict_non-empty_finitely-generated_MSSubAlgebra_of_AG_holds_A_in_C
let A be strict non-empty finitely-generated MSSubAlgebra of AG; ::_thesis: A in C
 A in MSSub AG by MSUALG_2:def_19;
hence  A in C by A1; ::_thesis: verum
end;
then reconsider CC = C as non empty set ;
set T = the strict non-empty finitely-generated MSSubAlgebra of AG;
set I = the carrier of SG;
let F be MSAlgebra-Family of C,SG; ::_thesis: ( ( for c being set st c in C holds
c = F . c ) implies ex PS being strict non-empty MSSubAlgebra of product F ex BA being ManySortedFunction of PS,AG st BA is_epimorphism PS,AG )
assume A3: for c being set st c in C holds
c = F . c ; ::_thesis: ex PS being strict non-empty MSSubAlgebra of product F ex BA being ManySortedFunction of PS,AG st BA is_epimorphism PS,AG
reconsider FF = F as MSAlgebra-Family of CC,SG ;
set pr = product FF;
defpred S1[ set , set ] means  ex t being SortSymbol of SG ex f being Element of (SORTS FF) . t ex A being strict non-empty finitely-generated MSSubAlgebra of AG st
( t = $1 & f = $2 & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
f . A = f . B ) );
consider SOR being ManySortedSet of the carrier of SG such that
A4: for i being set st i in the carrier of SG holds
for e being set holds
( e in SOR . i iff ( e in (SORTS FF) . i & S1[i,e] ) ) from PBOOLE:sch_2();
 SOR is MSSubset of (product FF)
proof
let i be set ; :: according to PBOOLE:def_2,PBOOLE:def_18 ::_thesis: ( not i in the carrier of SG or SOR . i c= the Sorts of (product FF) . i )
assume A5: i in the carrier of SG ; ::_thesis: SOR . i c= the Sorts of (product FF) . i
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in SOR . i or e in the Sorts of (product FF) . i )
assume  e in SOR . i ; ::_thesis: e in the Sorts of (product FF) . i
hence  e in the Sorts of (product FF) . i by A4, A5; ::_thesis: verum
end;
then reconsider SOR = SOR as MSSubset of (product FF) ;
 SOR is opers_closed
proof
let o be OperSymbol of SG; :: according to MSUALG_2:def_6 ::_thesis: SOR is_closed_on o
set r = the_result_sort_of o;
set ar = the_arity_of o;
let q be set ; :: according to TARSKI:def_3,MSUALG_2:def_5 ::_thesis: ( not q in proj2 ((Den (o,(product FF))) | (( the Arity of SG * (SOR #)) . o)) or q in ( the ResultSort of SG * SOR) . o )
assume A6: q in rng ((Den (o,(product FF))) | (((SOR #) * the Arity of SG) . o)) ; ::_thesis: q in ( the ResultSort of SG * SOR) . o
reconsider q1 = q as Element of (SORTS FF) . (the_result_sort_of o) by A6, PRALG_2:3;
consider g being set  such that
A7: g in dom ((Den (o,(product FF))) | (((SOR #) * the Arity of SG) . o)) and
A8: q = ((Den (o,(product FF))) | (((SOR #) * the Arity of SG) . o)) . g by A6, FUNCT_1:def_3;
A9: q = (Den (o,(product FF))) . g by A7, A8, FUNCT_1:47;
A10: g in ((SOR #) * the Arity of SG) . o by A7;
 g in dom (Den (o,(product FF))) by A7, RELAT_1:57;
then reconsider g = g as Element of Args (o,(product FF)) ;
 S1[ the_result_sort_of o,q]
proof
take  the_result_sort_of o ; ::_thesis: ex f being Element of (SORTS FF) . (the_result_sort_of o) ex A being strict non-empty finitely-generated MSSubAlgebra of AG st
( the_result_sort_of o = the_result_sort_of o & f = q & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
f . A = f . B ) )
take  q1 ; ::_thesis: ex A being strict non-empty finitely-generated MSSubAlgebra of AG st
( the_result_sort_of o = the_result_sort_of o & q1 = q & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
q1 . A = q1 . B ) )
percases ( the_arity_of o = {} or the_arity_of o <> {} ) ;
supposeA11: the_arity_of o = {} ; ::_thesis: ex A being strict non-empty finitely-generated MSSubAlgebra of AG st
( the_result_sort_of o = the_result_sort_of o & q1 = q & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
q1 . A = q1 . B ) )
set A = the strict non-empty finitely-generated MSSubAlgebra of AG;
 Args (o, the strict non-empty finitely-generated MSSubAlgebra of AG) = {{}} by A11, PRALG_2:4;
then A12: {} in Args (o, the strict non-empty finitely-generated MSSubAlgebra of AG) by TARSKI:def_1;
take  the strict non-empty finitely-generated MSSubAlgebra of AG ; ::_thesis: ( the_result_sort_of o = the_result_sort_of o & q1 = q & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st the strict non-empty finitely-generated MSSubAlgebra of AG is MSSubAlgebra of B holds
q1 . the strict non-empty finitely-generated MSSubAlgebra of AG = q1 . B ) )
thus  the_result_sort_of o = the_result_sort_of o ; ::_thesis: ( q1 = q & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st the strict non-empty finitely-generated MSSubAlgebra of AG is MSSubAlgebra of B holds
q1 . the strict non-empty finitely-generated MSSubAlgebra of AG = q1 . B ) )
thus  q1 = q ; ::_thesis: for B being strict non-empty finitely-generated MSSubAlgebra of AG st the strict non-empty finitely-generated MSSubAlgebra of AG is MSSubAlgebra of B holds
q1 . the strict non-empty finitely-generated MSSubAlgebra of AG = q1 . B
let B be strict non-empty finitely-generated MSSubAlgebra of AG; ::_thesis: ( the strict non-empty finitely-generated MSSubAlgebra of AG is MSSubAlgebra of B implies q1 . the strict non-empty finitely-generated MSSubAlgebra of AG = q1 . B )
assume  the strict non-empty finitely-generated MSSubAlgebra of AG is MSSubAlgebra of B ; ::_thesis: q1 . the strict non-empty finitely-generated MSSubAlgebra of AG = q1 . B
 Args (o,B) = {{}} by A11, PRALG_2:4;
then A13: {} in Args (o,B) by TARSKI:def_1;
 B in MSSub AG by MSUALG_2:def_19;
then A14: B in CC by A1;
 the strict non-empty finitely-generated MSSubAlgebra of AG in MSSub AG by MSUALG_2:def_19;
then  the strict non-empty finitely-generated MSSubAlgebra of AG in CC by A1;
then reconsider iA = the strict non-empty finitely-generated MSSubAlgebra of AG, iB = B as Element of CC by A14;
A15: iA = FF . iA by A3;
A16: iB = FF . iB by A3;
 Args (o,(product FF)) = {{}} by A11, PRALG_2:4;
then A17: g = {} by TARSKI:def_1;
hence q1 . the strict non-empty finitely-generated MSSubAlgebra of AG = (const (o,(product FF))) . iA by A9, PRALG_3:def_1
.= const (o,(FF . iA)) by A11, PRALG_3:9
.= (Den (o,(FF . iA))) . {} by PRALG_3:def_1
.= (Den (o,AG)) . {} by A15, A12, Th19
.= (Den (o,(FF . iB))) . {} by A16, A13, Th19
.= const (o,(FF . iB)) by PRALG_3:def_1
.= (const (o,(product FF))) . iB by A11, PRALG_3:9
.= q1 . B by A9, A17, PRALG_3:def_1 ;
::_thesis: verum
end;
supposeA18: the_arity_of o <> {} ; ::_thesis: ex A being strict non-empty finitely-generated MSSubAlgebra of AG st
( the_result_sort_of o = the_result_sort_of o & q1 = q & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
q1 . A = q1 . B ) )
then reconsider domar = dom (the_arity_of o) as non empty finite set ;
defpred S2[ set , set ] means  ex gn being Function ex A being strict non-empty finitely-generated MSSubAlgebra of AG st
( gn = g . $1 & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
gn . A = gn . B ) & $2 = A );
 g in (SOR #) . ( the Arity of SG . o) by A10, FUNCT_2:15;
then A19: g in product (SOR * (the_arity_of o)) by FINSEQ_2:def_5;
then A20: dom (SOR * (the_arity_of o)) = dom g by CARD_3:9
.= domar by MSUALG_3:6 ;
A21: for a being Element of domar ex b being Element of MSSub AG st S2[a,b]
proof
let n be Element of domar; ::_thesis: ex b being Element of MSSub AG st S2[n,b]
 g . n in (SOR * (the_arity_of o)) . n by A19, A20, CARD_3:9;
then  ( (the_arity_of o) . n in the carrier of SG & g . n in SOR . ((the_arity_of o) . n) ) by FUNCT_1:13, PARTFUN1:4;
then consider s being SortSymbol of SG, f being Element of (SORTS FF) . s, A being strict non-empty finitely-generated MSSubAlgebra of AG such that
 s = (the_arity_of o) . n and
A22: f = g . n and
A23: for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
f . A = f . B by A4;
reconsider b = A as Element of MSSub AG by MSUALG_2:def_19;
take  b ; ::_thesis: S2[n,b]
take  f ; ::_thesis: ex A being strict non-empty finitely-generated MSSubAlgebra of AG st
( f = g . n & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
f . A = f . B ) & b = A )
take  A ; ::_thesis: ( f = g . n & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
f . A = f . B ) & b = A )
thus  f = g . n by A22; ::_thesis: ( ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
f . A = f . B ) & b = A )
thus  for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
f . A = f . B by A23; ::_thesis: b = A
thus  b = A ; ::_thesis: verum
end;
consider KK being Function of domar,(MSSub AG) such that
A24: for n being Element of domar holds S2[n,KK . n] from FUNCT_2:sch_3(A21);
reconsider KK = KK as ManySortedSet of domar ;
 KK is MSAlgebra-Family of domar,SG
proof
let n be set ; :: according to PRALG_2:def_5 ::_thesis: ( not n in domar or KK . n is MSAlgebra over SG )
assume  n in domar ; ::_thesis: KK . n is MSAlgebra over SG
then  ex gn being Function ex A being strict non-empty finitely-generated MSSubAlgebra of AG st
( gn = g . n & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
gn . A = gn . B ) & KK . n = A ) by A24;
hence  KK . n is MSAlgebra over SG ; ::_thesis: verum
end;
then reconsider KK = KK as MSAlgebra-Family of domar,SG ;
 for n being Element of domar ex C being strict non-empty finitely-generated MSSubAlgebra of AG st C = KK . n
proof
let n be Element of domar; ::_thesis: ex C being strict non-empty finitely-generated MSSubAlgebra of AG st C = KK . n
 ex gn being Function ex A being strict non-empty finitely-generated MSSubAlgebra of AG st
( gn = g . n & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
gn . A = gn . B ) & KK . n = A ) by A24;
hence  ex C being strict non-empty finitely-generated MSSubAlgebra of AG st C = KK . n ; ::_thesis: verum
end;
then consider K being strict non-empty finitely-generated MSSubAlgebra of AG such that
A25: for n being Element of domar holds KK . n is MSSubAlgebra of K by Th25;
take  K ; ::_thesis: ( the_result_sort_of o = the_result_sort_of o & q1 = q & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st K is MSSubAlgebra of B holds
q1 . K = q1 . B ) )
thus  the_result_sort_of o = the_result_sort_of o ; ::_thesis: ( q1 = q & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st K is MSSubAlgebra of B holds
q1 . K = q1 . B ) )
thus  q1 = q ; ::_thesis: for B being strict non-empty finitely-generated MSSubAlgebra of AG st K is MSSubAlgebra of B holds
q1 . K = q1 . B
let B be strict non-empty finitely-generated MSSubAlgebra of AG; ::_thesis: ( K is MSSubAlgebra of B implies q1 . K = q1 . B )
assume A26: K is MSSubAlgebra of B ; ::_thesis: q1 . K = q1 . B
 K in MSSub AG by MSUALG_2:def_19;
then A27: K in CC by A1;
 B in MSSub AG by MSUALG_2:def_19;
then  B in CC by A1;
then reconsider iB = B, iK = K as Element of CC by A27;
A28: g in Funcs ((dom (the_arity_of o)),(Funcs (CC,(union  {  ( the Sorts of (FF . i) . s) where i is Element of CC, s is Element of the carrier of SG : verum  }  )))) by PRALG_3:14;
then A29: dom ((commute g) . iB) = domar by Th3;
A30: dom ((commute g) . iK) = domar by A28, Th3;
A31: for n being set st n in dom ((commute g) . iK) holds
((commute g) . iB) . n = ((commute g) . iK) . n
proof
let x be set ; ::_thesis: ( x in dom ((commute g) . iK) implies ((commute g) . iB) . x = ((commute g) . iK) . x )
assume A32: x in dom ((commute g) . iK) ; ::_thesis: ((commute g) . iB) . x = ((commute g) . iK) . x
then consider gn being Function, A being strict non-empty finitely-generated MSSubAlgebra of AG such that
A33: gn = g . x and
A34: ( ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
gn . A = gn . B ) & KK . x = A ) by A24, A30;
A35: KK . x is MSSubAlgebra of K by A25, A30, A32;
thus ((commute g) . iB) . x = gn . iB by A30, A32, A33, PRALG_3:21
.= gn . A by A26, A34, A35, MSUALG_2:6
.= gn . iK by A25, A30, A32, A34
.= ((commute g) . iK) . x by A30, A32, A33, PRALG_3:21 ; ::_thesis: verum
end;
A36: iK = FF . iK by A3;
A37: (commute g) . iK is Element of Args (o,(FF . iK)) by A18, PRALG_3:20;
A38: (commute g) . iB is Element of Args (o,(FF . iB)) by A18, PRALG_3:20;
A39: iB = FF . iB by A3;
thus q1 . K = (Den (o,(FF . iK))) . ((commute g) . iK) by A9, A18, PRALG_3:22
.= (Den (o,AG)) . ((commute g) . iK) by A36, A37, Th19
.= (Den (o,AG)) . ((commute g) . iB) by A28, A29, A31, Th3, FUNCT_1:2
.= (Den (o,(FF . iB))) . ((commute g) . iB) by A39, A38, Th19
.= q1 . B by A9, A18, PRALG_3:22 ; ::_thesis: verum
end;
end;
end;
then  q in SOR . (the_result_sort_of o) by A4;
hence  q in ( the ResultSort of SG * SOR) . o by FUNCT_2:15; ::_thesis: verum
end;
then A40: (product FF) | SOR = MSAlgebra(# SOR,(Opers ((product FF),SOR)) #) by MSUALG_2:def_15;
defpred S2[ set , set , set ] means  ex s being SortSymbol of SG ex f being Element of (SORTS FF) . s ex A being strict non-empty finitely-generated MSSubAlgebra of AG st
( s = $3 & f = $2 & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
f . A = f . B ) & $1 = f . A );
 SOR is V2()
proof
defpred S3[ set ] means  ex C being strict non-empty MSSubAlgebra of AG st
( $1 = C & C is finitely-generated );
let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in the carrier of SG or not SOR . i is empty )
consider ST1 being set  such that
A41: for x being set holds
( x in ST1 iff ( x in SuperAlgebraSet the strict non-empty finitely-generated MSSubAlgebra of AG & S3[x] ) ) from XBOOLE_0:sch_1();
A42: ST1 c= CC
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in ST1 or q in CC )
assume  q in ST1 ; ::_thesis: q in CC
then A43: ex C being strict non-empty MSSubAlgebra of AG st
( q = C & C is finitely-generated ) by A41;
then  q in MSSub AG by MSUALG_2:def_19;
hence  q in CC by A1, A43; ::_thesis: verum
end;
defpred S4[ set , set ] means  ex K being MSSubAlgebra of AG ex t being set st
( $1 = K & t in the Sorts of K . i & $2 = t );
assume A44: i in the carrier of SG ; ::_thesis: not SOR . i is empty
then consider x being set  such that
A45: x in the Sorts of the strict non-empty finitely-generated MSSubAlgebra of AG . i by XBOOLE_0:def_1;
reconsider s = i as SortSymbol of SG by A44;
A46: for c being set st c in CC holds
ex j being set st S4[c,j]
proof
let c be set ; ::_thesis: ( c in CC implies ex j being set st S4[c,j] )
assume  c in CC ; ::_thesis: ex j being set st S4[c,j]
then consider C being Element of MSSub AG such that
A47: c = C and
A48: ex R being strict non-empty finitely-generated MSSubAlgebra of AG st R = C by A1;
consider R being strict non-empty finitely-generated MSSubAlgebra of AG such that
A49: R = C by A48;
consider t being set  such that
A50: t in the Sorts of R . i by A44, XBOOLE_0:def_1;
take  t ; ::_thesis: S4[c,t]
take  R ; ::_thesis: ex t being set st
( c = R & t in the Sorts of R . i & t = t )
take  t ; ::_thesis: ( c = R & t in the Sorts of R . i & t = t )
thus  c = R by A47, A49; ::_thesis: ( t in the Sorts of R . i & t = t )
thus  ( t in the Sorts of R . i & t = t ) by A50; ::_thesis: verum
end;
consider f being ManySortedSet of CC such that
A51: for c being set st c in CC holds
S4[c,f . c] from PBOOLE:sch_3(A46);
set g = f +* (ST1 --> x);
A52: dom (ST1 --> x) = ST1 by FUNCOP_1:13;
A53: for a being set st a in dom (Carrier (FF,s)) holds
(f +* (ST1 --> x)) . a in (Carrier (FF,s)) . a
proof
let a be set ; ::_thesis: ( a in dom (Carrier (FF,s)) implies (f +* (ST1 --> x)) . a in (Carrier (FF,s)) . a )
assume  a in dom (Carrier (FF,s)) ; ::_thesis: (f +* (ST1 --> x)) . a in (Carrier (FF,s)) . a
then A54: a in CC ;
then A55: ex U0 being MSAlgebra over SG st
( U0 = FF . a & (Carrier (FF,s)) . a = the Sorts of U0 . s ) by PRALG_2:def_9;
consider K being MSSubAlgebra of AG, t being set  such that
A56: ( a = K & t in the Sorts of K . i ) and
A57: f . a = t by A51, A54;
percases ( a in ST1 or not a in ST1 ) ;
supposeA58: a in ST1 ; ::_thesis: (f +* (ST1 --> x)) . a in (Carrier (FF,s)) . a
then  a in dom (ST1 --> x) by FUNCOP_1:13;
then  (f +* (ST1 --> x)) . a = (ST1 --> x) . a by FUNCT_4:13;
then A59: (f +* (ST1 --> x)) . a = x by A58, FUNCOP_1:7;
 a in SuperAlgebraSet the strict non-empty finitely-generated MSSubAlgebra of AG by A41, A58;
then consider M being strict MSSubAlgebra of AG such that
A60: a = M and
A61: the strict non-empty finitely-generated MSSubAlgebra of AG is MSSubAlgebra of M by Def2;
 the Sorts of the strict non-empty finitely-generated MSSubAlgebra of AG is ManySortedSubset of the Sorts of M by A61, MSUALG_2:def_9;
then  the Sorts of the strict non-empty finitely-generated MSSubAlgebra of AG c= the Sorts of M by PBOOLE:def_18;
then  the Sorts of the strict non-empty finitely-generated MSSubAlgebra of AG . i c= the Sorts of M . i by A44, PBOOLE:def_2;
then  x in the Sorts of M . i by A45;
hence  (f +* (ST1 --> x)) . a in (Carrier (FF,s)) . a by A3, A54, A55, A59, A60; ::_thesis: verum
end;
suppose not a in ST1 ; ::_thesis: (f +* (ST1 --> x)) . a in (Carrier (FF,s)) . a
then  (f +* (ST1 --> x)) . a = t by A52, A57, FUNCT_4:11;
hence  (f +* (ST1 --> x)) . a in (Carrier (FF,s)) . a by A3, A54, A55, A56; ::_thesis: verum
end;
end;
end;
dom (f +* (ST1 --> x)) = (dom f) \/ (dom (ST1 --> x)) by FUNCT_4:def_1
.= CC \/ (dom (ST1 --> x)) by PARTFUN1:def_2
.= CC \/ ST1 by FUNCOP_1:13
.= CC by A42, XBOOLE_1:12
.= dom (Carrier (FF,s)) by PARTFUN1:def_2 ;
then A62: f +* (ST1 --> x) in product (Carrier (FF,s)) by A53, CARD_3:9;
 S1[i,f +* (ST1 --> x)]
proof
reconsider g1 = f +* (ST1 --> x) as Element of (SORTS FF) . s by A62, PRALG_2:def_10;
take  s ; ::_thesis: ex f being Element of (SORTS FF) . s ex A being strict non-empty finitely-generated MSSubAlgebra of AG st
( s = i & f = f +* (ST1 --> x) & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
f . A = f . B ) )
take  g1 ; ::_thesis: ex A being strict non-empty finitely-generated MSSubAlgebra of AG st
( s = i & g1 = f +* (ST1 --> x) & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
g1 . A = g1 . B ) )
take  the strict non-empty finitely-generated MSSubAlgebra of AG ; ::_thesis: ( s = i & g1 = f +* (ST1 --> x) & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st the strict non-empty finitely-generated MSSubAlgebra of AG is MSSubAlgebra of B holds
g1 . the strict non-empty finitely-generated MSSubAlgebra of AG = g1 . B ) )
thus  s = i ; ::_thesis: ( g1 = f +* (ST1 --> x) & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st the strict non-empty finitely-generated MSSubAlgebra of AG is MSSubAlgebra of B holds
g1 . the strict non-empty finitely-generated MSSubAlgebra of AG = g1 . B ) )
thus  g1 = f +* (ST1 --> x) ; ::_thesis: for B being strict non-empty finitely-generated MSSubAlgebra of AG st the strict non-empty finitely-generated MSSubAlgebra of AG is MSSubAlgebra of B holds
g1 . the strict non-empty finitely-generated MSSubAlgebra of AG = g1 . B
let B be strict non-empty finitely-generated MSSubAlgebra of AG; ::_thesis: ( the strict non-empty finitely-generated MSSubAlgebra of AG is MSSubAlgebra of B implies g1 . the strict non-empty finitely-generated MSSubAlgebra of AG = g1 . B )
assume  the strict non-empty finitely-generated MSSubAlgebra of AG is MSSubAlgebra of B ; ::_thesis: g1 . the strict non-empty finitely-generated MSSubAlgebra of AG = g1 . B
then  B in SuperAlgebraSet the strict non-empty finitely-generated MSSubAlgebra of AG by Def2;
then A63: B in ST1 by A41;
 the strict non-empty finitely-generated MSSubAlgebra of AG is MSSubAlgebra of the strict non-empty finitely-generated MSSubAlgebra of AG by MSUALG_2:5;
then  the strict non-empty finitely-generated MSSubAlgebra of AG in SuperAlgebraSet the strict non-empty finitely-generated MSSubAlgebra of AG by Def2;
then A64: the strict non-empty finitely-generated MSSubAlgebra of AG in ST1 by A41;
hence g1 . the strict non-empty finitely-generated MSSubAlgebra of AG = (ST1 --> x) . the strict non-empty finitely-generated MSSubAlgebra of AG by A52, FUNCT_4:13
.= x by A64, FUNCOP_1:7
.= (ST1 --> x) . B by A63, FUNCOP_1:7
.= g1 . B by A52, A63, FUNCT_4:13 ;
::_thesis: verum
end;
hence  not SOR . i is empty by A4; ::_thesis: verum
end;
then reconsider PS = (product FF) | SOR as strict non-empty MSSubAlgebra of product F by A40, MSUALG_1:def_3;
A65: now__::_thesis:_for_s_being_SortSymbol_of_SG
for_f_being_Element_of_(SORTS_FF)_._s
for_A_being_strict_non-empty_finitely-generated_MSSubAlgebra_of_AG_holds_f_._A_in_the_Sorts_of_AG_._s
let s be SortSymbol of SG; ::_thesis: for f being Element of (SORTS FF) . s
for A being strict non-empty finitely-generated MSSubAlgebra of AG holds f . A in the Sorts of AG . s
let f be Element of (SORTS FF) . s; ::_thesis: for A being strict non-empty finitely-generated MSSubAlgebra of AG holds f . A in the Sorts of AG . s
let A be strict non-empty finitely-generated MSSubAlgebra of AG; ::_thesis: f . A in the Sorts of AG . s
A66: dom (Carrier (FF,s)) = CC by PARTFUN1:def_2;
 A in MSSub AG by MSUALG_2:def_19;
then A67: A in dom (Carrier (FF,s)) by A1, A66;
then consider U0 being MSAlgebra over SG such that
A68: U0 = FF . A and
A69: (Carrier (FF,s)) . A = the Sorts of U0 . s by PRALG_2:def_9;
 (SORTS FF) . s = product (Carrier (FF,s)) by PRALG_2:def_10;
then A70: f . A in (Carrier (FF,s)) . A by A67, CARD_3:9;
 FF . A = A by A3, A67;
then  the Sorts of U0 is ManySortedSubset of the Sorts of AG by A68, MSUALG_2:def_9;
then  the Sorts of U0 c= the Sorts of AG by PBOOLE:def_18;
then  the Sorts of U0 . s c= the Sorts of AG . s by PBOOLE:def_2;
hence  f . A in the Sorts of AG . s by A69, A70; ::_thesis: verum
end;
A71: now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_SG_holds_
for_x_being_set_st_x_in_the_Sorts_of_PS_._i_holds_
ex_y_being_set_st_
(_y_in_the_Sorts_of_AG_._i_&_S2[y,x,i]_)
let i be set ; ::_thesis: ( i in the carrier of SG implies for x being set st x in the Sorts of PS . i holds
ex y being set st
( y in the Sorts of AG . i & S2[y,x,i] ) )
assume A72: i in the carrier of SG ; ::_thesis: for x being set st x in the Sorts of PS . i holds
ex y being set st
( y in the Sorts of AG . i & S2[y,x,i] )
let x be set ; ::_thesis: ( x in the Sorts of PS . i implies ex y being set st
( y in the Sorts of AG . i & S2[y,x,i] ) )
assume  x in the Sorts of PS . i ; ::_thesis: ex y being set st
( y in the Sorts of AG . i & S2[y,x,i] )
then consider s being SortSymbol of SG, f being Element of (SORTS FF) . s, A being strict non-empty finitely-generated MSSubAlgebra of AG such that
A73: s = i and
A74: ( f = x & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
f . A = f . B ) ) by A4, A40, A72;
take y = f . A; ::_thesis: ( y in the Sorts of AG . i & S2[y,x,i] )
thus  y in the Sorts of AG . i by A65, A73; ::_thesis: S2[y,x,i]
thus  S2[y,x,i] by A73, A74; ::_thesis: verum
end;
consider BA being ManySortedFunction of PS,AG such that
A75: for i being set st i in the carrier of SG holds
ex g being Function of ( the Sorts of PS . i),( the Sorts of AG . i) st
( g = BA . i & ( for x being set st x in the Sorts of PS . i holds
S2[g . x,x,i] ) ) from MSSUBFAM:sch_1(A71);
take  PS ; ::_thesis: ex BA being ManySortedFunction of PS,AG st BA is_epimorphism PS,AG
take  BA ; ::_thesis: BA is_epimorphism PS,AG
thus  BA is_homomorphism PS,AG :: according to MSUALG_3:def_8 ::_thesis: BA is "onto"
proof
let o be OperSymbol of SG; :: according to MSUALG_3:def_7 ::_thesis: ( Args (o,PS) = {} or for b1 being Element of Args (o,PS) holds (BA . (the_result_sort_of o)) . ((Den (o,PS)) . b1) = (Den (o,AG)) . (BA # b1) )
assume  Args (o,PS) <> {} ; ::_thesis: for b1 being Element of Args (o,PS) holds (BA . (the_result_sort_of o)) . ((Den (o,PS)) . b1) = (Den (o,AG)) . (BA # b1)
let k be Element of Args (o,PS); ::_thesis: (BA . (the_result_sort_of o)) . ((Den (o,PS)) . k) = (Den (o,AG)) . (BA # k)
set r = the_result_sort_of o;
set ar = the_arity_of o;
consider g being Function of ( the Sorts of PS . (the_result_sort_of o)),( the Sorts of AG . (the_result_sort_of o)) such that
A76: g = BA . (the_result_sort_of o) and
A77: for k being set st k in the Sorts of PS . (the_result_sort_of o) holds
S2[g . k,k, the_result_sort_of o] by A75;
consider s being SortSymbol of SG, f being Element of (SORTS FF) . s, A being strict non-empty finitely-generated MSSubAlgebra of AG such that
 s = the_result_sort_of o and
A78: f = (Den (o,PS)) . k and
A79: for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
f . A = f . B and
A80: g . ((Den (o,PS)) . k) = f . A by A77, MSUALG_9:18;
percases ( the_arity_of o = {} or the_arity_of o <> {} ) ;
supposeA81: the_arity_of o = {} ; ::_thesis: (BA . (the_result_sort_of o)) . ((Den (o,PS)) . k) = (Den (o,AG)) . (BA # k)
 A in MSSub AG by MSUALG_2:def_19;
then  A in CC by A1;
then reconsider iA = A as Element of CC ;
reconsider ff1 = (Den (o,(product FF))) . k as Function by Th20;
A82: (Den (o,(product FF))) . {} = const (o,(product FF)) by PRALG_3:def_1;
 Args (o,A) = {{}} by A81, PRALG_2:4;
then A83: {} in Args (o,A) by TARSKI:def_1;
A84: Args (o,PS) = {{}} by A81, PRALG_2:4;
then A85: k = {} by TARSKI:def_1;
thus (BA . (the_result_sort_of o)) . ((Den (o,PS)) . k) = ff1 . A by A76, A78, A80, Th19
.= (const (o,(product FF))) . iA by A84, A82, TARSKI:def_1
.= const (o,(FF . iA)) by A81, PRALG_3:9
.= (Den (o,(FF . iA))) . {} by PRALG_3:def_1
.= (Den (o,A)) . {} by A3
.= (Den (o,AG)) . {} by A83, Th19
.= (Den (o,AG)) . (BA # k) by A81, A85, PRALG_3:11 ; ::_thesis: verum
end;
supposeA86: the_arity_of o <> {} ; ::_thesis: (BA . (the_result_sort_of o)) . ((Den (o,PS)) . k) = (Den (o,AG)) . (BA # k)
then reconsider domar = dom (the_arity_of o) as non empty finite set ;
defpred S3[ set , set ] means  ex kn being Function ex A being strict non-empty finitely-generated MSSubAlgebra of AG st
( kn = k . $1 & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
kn . A = kn . B ) & (BA . ((the_arity_of o) . $1)) . kn = kn . A & $2 = A );
A87: for n being Element of domar ex b being Element of MSSub AG st S3[n,b]
proof
let n be Element of domar; ::_thesis: ex b being Element of MSSub AG st S3[n,b]
consider g being Function of ( the Sorts of PS . ((the_arity_of o) . n)),( the Sorts of AG . ((the_arity_of o) . n)) such that
A88: g = BA . ((the_arity_of o) . n) and
A89: for x being set st x in the Sorts of PS . ((the_arity_of o) . n) holds
S2[g . x,x,(the_arity_of o) . n] by A75, PARTFUN1:4;
 k . n in the Sorts of PS . ((the_arity_of o) /. n) by MSUALG_6:2;
then  k . n in the Sorts of PS . ((the_arity_of o) . n) by PARTFUN1:def_6;
then consider s being SortSymbol of SG, f being Element of (SORTS FF) . s, A being strict non-empty finitely-generated MSSubAlgebra of AG such that
 s = (the_arity_of o) . n and
A90: f = k . n and
A91: for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
f . A = f . B and
A92: g . (k . n) = f . A by A89;
reconsider b = A as Element of MSSub AG by MSUALG_2:def_19;
take  b ; ::_thesis: S3[n,b]
take  f ; ::_thesis: ex A being strict non-empty finitely-generated MSSubAlgebra of AG st
( f = k . n & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
f . A = f . B ) & (BA . ((the_arity_of o) . n)) . f = f . A & b = A )
take  A ; ::_thesis: ( f = k . n & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
f . A = f . B ) & (BA . ((the_arity_of o) . n)) . f = f . A & b = A )
thus  f = k . n by A90; ::_thesis: ( ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
f . A = f . B ) & (BA . ((the_arity_of o) . n)) . f = f . A & b = A )
thus  for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
f . A = f . B by A91; ::_thesis: ( (BA . ((the_arity_of o) . n)) . f = f . A & b = A )
thus  (BA . ((the_arity_of o) . n)) . f = f . A by A88, A90, A92; ::_thesis: b = A
thus  b = A ; ::_thesis: verum
end;
consider KK being Function of domar,(MSSub AG) such that
A93: for n being Element of domar holds S3[n,KK . n] from FUNCT_2:sch_3(A87);
reconsider KK = KK as ManySortedSet of domar ;
 KK is MSAlgebra-Family of domar,SG
proof
let n be set ; :: according to PRALG_2:def_5 ::_thesis: ( not n in domar or KK . n is MSAlgebra over SG )
assume  n in domar ; ::_thesis: KK . n is MSAlgebra over SG
then  ex kn being Function ex A being strict non-empty finitely-generated MSSubAlgebra of AG st
( kn = k . n & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
kn . A = kn . B ) & (BA . ((the_arity_of o) . n)) . kn = kn . A & KK . n = A ) by A93;
hence  KK . n is MSAlgebra over SG ; ::_thesis: verum
end;
then reconsider KK = KK as MSAlgebra-Family of domar,SG ;
 for n being Element of domar ex C being strict non-empty finitely-generated MSSubAlgebra of AG st C = KK . n
proof
let n be Element of domar; ::_thesis: ex C being strict non-empty finitely-generated MSSubAlgebra of AG st C = KK . n
 ex kn being Function ex A being strict non-empty finitely-generated MSSubAlgebra of AG st
( kn = k . n & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
kn . A = kn . B ) & (BA . ((the_arity_of o) . n)) . kn = kn . A & KK . n = A ) by A93;
hence  ex C being strict non-empty finitely-generated MSSubAlgebra of AG st C = KK . n ; ::_thesis: verum
end;
then consider K being strict non-empty finitely-generated MSSubAlgebra of AG such that
A94: for n being Element of domar holds KK . n is MSSubAlgebra of K by Th25;
consider MAX being strict non-empty finitely-generated MSSubAlgebra of AG such that
A95: A is MSSubAlgebra of MAX and
A96: K is MSSubAlgebra of MAX by Th26;
 MAX in MSSub AG by MSUALG_2:def_19;
then  MAX in CC by A1;
then reconsider iA = MAX as Element of CC ;
A97: k in Args (o,(product FF)) by Th18;
then A98: (commute k) . iA is Element of Args (o,(FF . iA)) by A86, PRALG_3:20;
then  (commute k) . iA in Args (o,(FF . iA)) ;
then A99: (commute k) . iA in Args (o,MAX) by A3;
A100: k in Funcs ((dom (the_arity_of o)),(Funcs (CC,(union  {  ( the Sorts of (FF . i) . m) where i is Element of CC, m is Element of the carrier of SG : verum  }  )))) by A97, PRALG_3:14;
then A101: dom ((commute k) . iA) = domar by Th3;
A102: for n being set st n in dom ((commute k) . iA) holds
(BA # k) . n = ((commute k) . iA) . n
proof
set fs = (commute k) . iA;
reconsider fs = (commute k) . iA as Element of Args (o,MAX) by A3, A98;
let n be set ; ::_thesis: ( n in dom ((commute k) . iA) implies (BA # k) . n = ((commute k) . iA) . n )
assume A103: n in dom ((commute k) . iA) ; ::_thesis: (BA # k) . n = ((commute k) . iA) . n
then reconsider arn = (the_arity_of o) . n as SortSymbol of SG by A101, PARTFUN1:4;
 n in Seg (len fs) by A103, FINSEQ_1:def_3;
then reconsider n9 = n as Nat ;
consider kn being Function, Ki being strict non-empty finitely-generated MSSubAlgebra of AG such that
A104: kn = k . n and
A105: for B being strict non-empty finitely-generated MSSubAlgebra of AG st Ki is MSSubAlgebra of B holds
kn . Ki = kn . B and
A106: (BA . arn) . kn = kn . Ki and
A107: KK . n = Ki by A93, A101, A103;
A108: Ki is MSSubAlgebra of K by A94, A101, A103, A107;
 dom k = domar by A100, FUNCT_2:92;
hence (BA # k) . n = (BA . ((the_arity_of o) /. n9)) . (k . n) by A101, A103, MSUALG_3:def_6
.= kn . (KK . n) by A101, A103, A104, A106, A107, PARTFUN1:def_6
.= kn . iA by A96, A105, A107, A108, MSUALG_2:6
.= ((commute k) . iA) . n by A97, A101, A103, A104, PRALG_3:21 ;
::_thesis: verum
end;
reconsider ff1 = (Den (o,(product FF))) . k as Function by Th20;
A109: dom (BA # k) = domar by MSUALG_6:2;
thus (BA . (the_result_sort_of o)) . ((Den (o,PS)) . k) = f . MAX by A76, A79, A80, A95
.= ff1 . MAX by A78, Th19
.= (Den (o,(FF . iA))) . ((commute k) . iA) by A86, A97, PRALG_3:22
.= (Den (o,MAX)) . ((commute k) . iA) by A3
.= (Den (o,AG)) . ((commute k) . iA) by A99, Th19
.= (Den (o,AG)) . (BA # k) by A100, A109, A102, Th3, FUNCT_1:2 ; ::_thesis: verum
end;
end;
end;
let i be set ; :: according to MSUALG_3:def_3 ::_thesis: ( not i in the carrier of SG or proj2 (BA . i) = the Sorts of AG . i )
assume  i in the carrier of SG ; ::_thesis: proj2 (BA . i) = the Sorts of AG . i
then reconsider s = i as SortSymbol of SG ;
consider ff being set  such that
A110: ff in the Sorts of PS . s by XBOOLE_0:def_1;
 rng (BA . s) c= the Sorts of AG . s ;
hence  rng (BA . i) c= the Sorts of AG . i ; :: according to XBOOLE_0:def_10 ::_thesis: the Sorts of AG . i c= proj2 (BA . i)
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in the Sorts of AG . i or y in proj2 (BA . i) )
assume A111: y in the Sorts of AG . i ; ::_thesis: y in proj2 (BA . i)
A112: (SORTS FF) . s = product (Carrier (FF,s)) by PRALG_2:def_10;
then  ff in product (Carrier (FF,s)) by A4, A40, A110;
then consider aa being Function such that
 ff = aa and
A113: dom aa = dom (Carrier (FF,s)) and
A114: for x being set st x in dom (Carrier (FF,s)) holds
aa . x in (Carrier (FF,s)) . x by CARD_3:def_5;
defpred S3[ set ] means  ex Axx being MSSubAlgebra of AG st
( Axx = $1 & y in the Sorts of Axx . s );
consider WW being set  such that
A115: for a being set holds
( a in WW iff ( a in CC & S3[a] ) ) from XBOOLE_0:sch_1();
set XX = aa +* (WW --> y);
A116: dom (WW --> y) = WW by FUNCOP_1:13;
A117: for xx being Element of CC st S3[xx] holds
(aa +* (WW --> y)) . xx = y
proof
let xx be Element of CC; ::_thesis: ( S3[xx] implies (aa +* (WW --> y)) . xx = y )
assume  S3[xx] ; ::_thesis: (aa +* (WW --> y)) . xx = y
then A118: xx in WW by A115;
hence (aa +* (WW --> y)) . xx = (WW --> y) . xx by A116, FUNCT_4:13
.= y by A118, FUNCOP_1:7 ;
::_thesis: verum
end;
A119: dom (Carrier (FF,s)) = CC by PARTFUN1:def_2;
A120: for x being set st x in dom (Carrier (FF,s)) holds
(aa +* (WW --> y)) . x in (Carrier (FF,s)) . x
proof
let x be set ; ::_thesis: ( x in dom (Carrier (FF,s)) implies (aa +* (WW --> y)) . x in (Carrier (FF,s)) . x )
assume A121: x in dom (Carrier (FF,s)) ; ::_thesis: (aa +* (WW --> y)) . x in (Carrier (FF,s)) . x
then consider C being Element of MSSub AG such that
A122: x = C and
A123: ex R being strict non-empty finitely-generated MSSubAlgebra of AG st R = C by A1, A119;
consider R being strict non-empty finitely-generated MSSubAlgebra of AG such that
A124: R = C by A123;
A125: R in CC by A1, A124;
then A126: ( ex U0 being MSAlgebra over SG st
( U0 = FF . R & (Carrier (FF,s)) . R = the Sorts of U0 . s ) & FF . R = R ) by A3, PRALG_2:def_9;
percases ( S3[x] or not S3[x] ) ;
suppose S3[x] ; ::_thesis: (aa +* (WW --> y)) . x in (Carrier (FF,s)) . x
hence  (aa +* (WW --> y)) . x in (Carrier (FF,s)) . x by A117, A122, A124, A125, A126; ::_thesis: verum
end;
suppose not S3[x] ; ::_thesis: (aa +* (WW --> y)) . x in (Carrier (FF,s)) . x
then  not x in WW by A115;
then  (aa +* (WW --> y)) . x = aa . x by A116, FUNCT_4:11;
hence  (aa +* (WW --> y)) . x in (Carrier (FF,s)) . x by A114, A121; ::_thesis: verum
end;
end;
end;
A127: WW c= CC
proof
let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in WW or w in CC )
assume  w in WW ; ::_thesis: w in CC
hence  w in CC by A115; ::_thesis: verum
end;
set L = the V2() V29() MSSubset of AG;
A128: dom (BA . s) = the Sorts of PS . s by FUNCT_2:def_1;
set SY = {s} --> {y};
dom ( the V2() V29() MSSubset of AG +* ({s} --> {y})) = (dom the V2() V29() MSSubset of AG) \/ (dom ({s} --> {y})) by FUNCT_4:def_1
.= the carrier of SG \/ (dom ({s} --> {y})) by PARTFUN1:def_2
.= the carrier of SG \/ {s} by FUNCOP_1:13
.= the carrier of SG by ZFMISC_1:40 ;
then reconsider Y = the V2() V29() MSSubset of AG +* ({s} --> {y}) as ManySortedSet of the carrier of SG by PARTFUN1:def_2, RELAT_1:def_18;
A129: s in {s} by TARSKI:def_1;
 dom ({s} --> {y}) = {s} by FUNCOP_1:13;
then A130: Y . s = ({s} --> {y}) . s by A129, FUNCT_4:13
.= {y} by A129, FUNCOP_1:7 ;
A131: now__::_thesis:_for_k_being_set_st_k_in_the_carrier_of_SG_&_k_<>_s_holds_
Y_._k_=_the_V2()_V29()_MSSubset_of_AG_._k
let k be set ; ::_thesis: ( k in the carrier of SG & k <> s implies Y . k = the V2() V29() MSSubset of AG . k )
assume that
 k in the carrier of SG and
A132: k <> s ; ::_thesis: Y . k = the V2() V29() MSSubset of AG . k
 not k in dom ({s} --> {y}) by A132, TARSKI:def_1;
hence  Y . k = the V2() V29() MSSubset of AG . k by FUNCT_4:11; ::_thesis: verum
end;
 Y is ManySortedSubset of the Sorts of AG
proof
let j be set ; :: according to PBOOLE:def_2,PBOOLE:def_18 ::_thesis: ( not j in the carrier of SG or Y . j c= the Sorts of AG . j )
assume A133: j in the carrier of SG ; ::_thesis: Y . j c= the Sorts of AG . j
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y . j or x in the Sorts of AG . j )
assume A134: x in Y . j ; ::_thesis: x in the Sorts of AG . j
percases ( j <> s or j = s ) ;
supposeA135: j <> s ; ::_thesis: x in the Sorts of AG . j
 the V2() V29() MSSubset of AG c= the Sorts of AG by PBOOLE:def_18;
then A136: the V2() V29() MSSubset of AG . j c= the Sorts of AG . j by A133, PBOOLE:def_2;
 x in the V2() V29() MSSubset of AG . j by A131, A133, A134, A135;
hence  x in the Sorts of AG . j by A136; ::_thesis: verum
end;
suppose j = s ; ::_thesis: x in the Sorts of AG . j
hence  x in the Sorts of AG . j by A111, A130, A134, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
then reconsider Y = Y as MSSubset of AG ;
 Y is V2()
proof
let j be set ; :: according to PBOOLE:def_13 ::_thesis: ( not j in the carrier of SG or not Y . j is empty )
assume A137: j in the carrier of SG ; ::_thesis: not Y . j is empty
percases ( j <> s or j = s ) ;
suppose j <> s ; ::_thesis: not Y . j is empty
then  Y . j = the V2() V29() MSSubset of AG . j by A131, A137;
hence  not Y . j is empty by A137; ::_thesis: verum
end;
suppose j = s ; ::_thesis: not Y . j is empty
hence  not Y . j is empty by A130; ::_thesis: verum
end;
end;
end;
then reconsider Y = Y as V2() MSSubset of AG ;
 Y is V29()
proof
let j be set ; :: according to FINSET_1:def_5 ::_thesis: ( not j in the carrier of SG or Y . j is finite )
assume A138: j in the carrier of SG ; ::_thesis: Y . j is finite
percases ( j <> s or j = s ) ;
suppose j <> s ; ::_thesis: Y . j is finite
then  Y . j = the V2() V29() MSSubset of AG . j by A131, A138;
hence  Y . j is finite ; ::_thesis: verum
end;
suppose j = s ; ::_thesis: Y . j is finite
hence  Y . j is finite by A130; ::_thesis: verum
end;
end;
end;
then reconsider Y = Y as V2() V29() MSSubset of AG ;
 Y is MSSubset of (GenMSAlg Y) by MSUALG_2:def_17;
then  Y c= the Sorts of (GenMSAlg Y) by PBOOLE:def_18;
then A139: Y . s c= the Sorts of (GenMSAlg Y) . s by PBOOLE:def_2;
dom (aa +* (WW --> y)) = (dom aa) \/ (dom (WW --> y)) by FUNCT_4:def_1
.= CC \/ (dom (WW --> y)) by A113, PARTFUN1:def_2
.= CC \/ WW by FUNCOP_1:13
.= CC by A127, XBOOLE_1:12 ;
then reconsider XX = aa +* (WW --> y) as Element of (SORTS FF) . s by A112, A119, A120, CARD_3:9;
consider h being Function of ( the Sorts of PS . s),( the Sorts of AG . s) such that
A140: h = BA . s and
A141: for x being set st x in the Sorts of PS . s holds
S2[h . x,x,s] by A75;
A142: y in Y . s by A130, TARSKI:def_1;
then A143: y in the Sorts of (GenMSAlg Y) . s by A139;
 S1[s,XX]
proof
take  s ; ::_thesis: ex f being Element of (SORTS FF) . s ex A being strict non-empty finitely-generated MSSubAlgebra of AG st
( s = s & f = XX & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
f . A = f . B ) )
take  XX ; ::_thesis: ex A being strict non-empty finitely-generated MSSubAlgebra of AG st
( s = s & XX = XX & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
XX . A = XX . B ) )
take TT = GenMSAlg Y; ::_thesis: ( s = s & XX = XX & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st TT is MSSubAlgebra of B holds
XX . TT = XX . B ) )
thus  s = s ; ::_thesis: ( XX = XX & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st TT is MSSubAlgebra of B holds
XX . TT = XX . B ) )
thus  XX = XX ; ::_thesis: for B being strict non-empty finitely-generated MSSubAlgebra of AG st TT is MSSubAlgebra of B holds
XX . TT = XX . B
let B be strict non-empty finitely-generated MSSubAlgebra of AG; ::_thesis: ( TT is MSSubAlgebra of B implies XX . TT = XX . B )
assume  TT is MSSubAlgebra of B ; ::_thesis: XX . TT = XX . B
then  the Sorts of TT is ManySortedSubset of the Sorts of B by MSUALG_2:def_9;
then  the Sorts of TT c= the Sorts of B by PBOOLE:def_18;
then A144: the Sorts of TT . s c= the Sorts of B . s by PBOOLE:def_2;
A145: B in CC by A2;
 TT in CC by A2;
hence XX . TT = y by A139, A142, A117
.= XX . B by A143, A117, A145, A144 ;
::_thesis: verum
end;
then A146: XX in SOR . s by A4;
then  S2[h . XX,XX,s] by A40, A141;
then consider t being SortSymbol of SG, f being Element of (SORTS FF) . s, A being strict non-empty finitely-generated MSSubAlgebra of AG such that
 s = t and
A147: ( f = XX & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
f . A = f . B ) & h . XX = f . A ) ;
consider MAX being strict non-empty finitely-generated MSSubAlgebra of AG such that
A148: A is MSSubAlgebra of MAX and
A149: GenMSAlg Y is MSSubAlgebra of MAX by Th26;
A150: MAX in CC by A2;
 the Sorts of (GenMSAlg Y) is ManySortedSubset of the Sorts of MAX by A149, MSUALG_2:def_9;
then  the Sorts of (GenMSAlg Y) c= the Sorts of MAX by PBOOLE:def_18;
then A151: the Sorts of (GenMSAlg Y) . s c= the Sorts of MAX . s by PBOOLE:def_2;
h . XX = XX . MAX by A147, A148
.= y by A143, A117, A151, A150 ;
hence  y in proj2 (BA . i) by A40, A128, A140, A146, FUNCT_1:def_3; ::_thesis: verum
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
proof
let S be non empty non void ManySortedSign ; ::_thesis: 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
let U0 be free feasible MSAlgebra over S; ::_thesis: 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
let A be free GeneratorSet of U0; ::_thesis: for Z being MSSubset of U0 st Z c= A & GenMSAlg Z is feasible holds
GenMSAlg Z is free
let Z be MSSubset of U0; ::_thesis: ( Z c= A & GenMSAlg Z is feasible implies GenMSAlg Z is free )
assume that
A1: Z c= A and
A2: GenMSAlg Z is feasible ; ::_thesis: GenMSAlg Z is free
reconsider Z1 = Z as MSSubset of (GenMSAlg Z) by MSUALG_2:def_17;
 the Sorts of (GenMSAlg Z1) = the Sorts of (GenMSAlg Z) by EXTENS_1:18;
then reconsider z = Z as GeneratorSet of GenMSAlg Z by MSAFREE:def_4;
reconsider z1 = z as ManySortedSubset of A by A1, PBOOLE:def_18;
take  z ; :: according to MSAFREE:def_6 ::_thesis: z is free
 z is free
proof
reconsider D = the Sorts of (GenMSAlg Z) as MSSubset of U0 by MSUALG_2:def_9;
let U1 be non-empty MSAlgebra over S; :: according to MSAFREE:def_5 ::_thesis: for b1 being ManySortedFunction of z, the Sorts of U1 ex b2 being ManySortedFunction of the Sorts of (GenMSAlg Z), the Sorts of U1 st
( b2 is_homomorphism GenMSAlg Z,U1 & b2 || z = b1 )
let g be ManySortedFunction of z, the Sorts of U1; ::_thesis: ex b1 being ManySortedFunction of the Sorts of (GenMSAlg Z), the Sorts of U1 st
( b1 is_homomorphism GenMSAlg Z,U1 & b1 || z = g )
consider G being ManySortedFunction of A, the Sorts of U1 such that
A3: G || z1 = g by Th6;
consider h being ManySortedFunction of U0,U1 such that
A4: h is_homomorphism U0,U1 and
A5: h || A = G by MSAFREE:def_5;
reconsider H = h || D as ManySortedFunction of (GenMSAlg Z),U1 ;
take  H ; ::_thesis: ( H is_homomorphism GenMSAlg Z,U1 & H || z = g )
thus  H is_homomorphism GenMSAlg Z,U1 by A2, A4, Th22; ::_thesis: H || z = g
thus g = h || Z by A3, A5, Th5
.= H || z by Th5 ; ::_thesis: verum
end;
hence  z is free ; ::_thesis: verum
end;

begin

definition
let S be non empty non void ManySortedSign ;
func TermAlg S ->  MSAlgebra over S equals :: EQUATION:def 3
 FreeMSA ( the carrier of S --> NAT);
correctness
coherence
FreeMSA ( the carrier of S --> NAT) is MSAlgebra over S;
;
end;

:: deftheorem  defines TermAlg EQUATION:def_3_:_
 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 ;
cluster TermAlg S ->  strict non-empty free ;
coherence
 ( TermAlg S is strict & TermAlg S is non-empty & TermAlg S is free ) ;
end;

definition
let S be non empty non void ManySortedSign ;
func Equations S ->  ManySortedSet of the carrier of S equals :: EQUATION:def 4
[| the Sorts of (TermAlg S), the Sorts of (TermAlg S)|];
correctness
coherence
[| the Sorts of (TermAlg S), the Sorts of (TermAlg S)|] is ManySortedSet of the carrier of S;
;
end;

:: 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)|];

registration
let S be non empty non void ManySortedSign ;
cluster Equations S -> V2() ;
coherence
 Equations S is non-empty ;
end;

definition
let S be non empty non void ManySortedSign ;
mode EqualSet of S is ManySortedSubset of Equations S;
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;

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 funcx '=' y ->  Element of (Equations S) . s;
coherence
 '=' is Element of (Equations S) . s
proof
 [x,y] in [:( the Sorts of (TermAlg S) . s),( the Sorts of (TermAlg S) . s):] by ZFMISC_1:87;
hence  '=' is Element of (Equations S) . s by PBOOLE:def_16; ::_thesis: verum
end;
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
proof
let S be non empty non void ManySortedSign ; ::_thesis: for s being SortSymbol of S
for e being Element of (Equations S) . s holds e `1 in the Sorts of (TermAlg S) . s
let s be SortSymbol of S; ::_thesis: for e being Element of (Equations S) . s holds e `1 in the Sorts of (TermAlg S) . s
let e be Element of (Equations S) . s; ::_thesis: e `1 in the Sorts of (TermAlg S) . s
set T = the Sorts of (TermAlg S);
 e is Element of [:( the Sorts of (TermAlg S) . s),( the Sorts of (TermAlg S) . s):] by PBOOLE:def_16;
hence  e `1 in the Sorts of (TermAlg S) . s by MCART_1:10; ::_thesis: verum
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
proof
let S be non empty non void ManySortedSign ; ::_thesis: for s being SortSymbol of S
for e being Element of (Equations S) . s holds e `2 in the Sorts of (TermAlg S) . s
let s be SortSymbol of S; ::_thesis: for e being Element of (Equations S) . s holds e `2 in the Sorts of (TermAlg S) . s
let e be Element of (Equations S) . s; ::_thesis: e `2 in the Sorts of (TermAlg S) . s
set T = the Sorts of (TermAlg S);
 e is Element of [:( the Sorts of (TermAlg S) . s),( the Sorts of (TermAlg S) . s):] by PBOOLE:def_16;
hence  e `2 in the Sorts of (TermAlg S) . s by MCART_1:10; ::_thesis: verum
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;
predA |= 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);
end;

:: 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) );

definition
let S be non empty non void ManySortedSign ;
let A be MSAlgebra over S;
let E be EqualSet of S;
predA |= 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;
end;

:: 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 );

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
proof
let S be non empty non void ManySortedSign ; ::_thesis: 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
let U0 be non-empty MSAlgebra over S; ::_thesis: 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
let s be SortSymbol of S; ::_thesis: for e being Element of (Equations S) . s
for U2 being strict non-empty MSSubAlgebra of U0 st U0 |= e holds
U2 |= e
let e be Element of (Equations S) . s; ::_thesis: for U2 being strict non-empty MSSubAlgebra of U0 st U0 |= e holds
U2 |= e
let U2 be strict non-empty MSSubAlgebra of U0; ::_thesis: ( U0 |= e implies U2 |= e )
assume A1: U0 |= e ; ::_thesis: U2 |= e
let h be ManySortedFunction of (TermAlg S),U2; :: according to EQUATION:def_5 ::_thesis: ( h is_homomorphism TermAlg S,U2 implies (h . s) . (e `1) = (h . s) . (e `2) )
assume A2: h is_homomorphism TermAlg S,U2 ; ::_thesis: (h . s) . (e `1) = (h . s) . (e `2)
A3: the Sorts of (TermAlg S) is_transformable_to the Sorts of U2
proof
let i be set ; :: according to PZFMISC1:def_3 ::_thesis: ( not i in the carrier of S or not the Sorts of U2 . i = {} or the Sorts of (TermAlg S) . i = {} )
assume  i in the carrier of S ; ::_thesis: ( not the Sorts of U2 . i = {} or the Sorts of (TermAlg S) . i = {} )
hence  ( not the Sorts of U2 . i = {} or the Sorts of (TermAlg S) . i = {} ) ; ::_thesis: verum
end;
 the Sorts of U2 is MSSubset of U0 by MSUALG_2:def_9;
then reconsider f1 = h as ManySortedFunction of (TermAlg S),U0 by A3, EXTENS_1:5;
 f1 is_homomorphism TermAlg S,U0 by A2, MSUALG_9:15;
hence  (h . s) . (e `1) = (h . s) . (e `2) by A1, Def5; ::_thesis: verum
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
proof
let S be non empty non void ManySortedSign ; ::_thesis: 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
let U0 be non-empty MSAlgebra over S; ::_thesis: for E being EqualSet of S
for U2 being strict non-empty MSSubAlgebra of U0 st U0 |= E holds
U2 |= E
let E be EqualSet of S; ::_thesis: for U2 being strict non-empty MSSubAlgebra of U0 st U0 |= E holds
U2 |= E
let U2 be strict non-empty MSSubAlgebra of U0; ::_thesis: ( U0 |= E implies U2 |= E )
assume A1: U0 |= E ; ::_thesis: U2 |= E
let s be SortSymbol of S; :: according to EQUATION:def_6 ::_thesis: for e being Element of (Equations S) . s st e in E . s holds
U2 |= e
let e be Element of (Equations S) . s; ::_thesis: ( e in E . s implies U2 |= e )
assume  e in E . s ; ::_thesis: U2 |= e
then  U0 |= e by A1, Def6;
hence  U2 |= e by Th31; ::_thesis: verum
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
proof
let S be non empty non void ManySortedSign ; ::_thesis: 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
let U0, U1 be non-empty MSAlgebra over S; ::_thesis: for s being SortSymbol of S
for e being Element of (Equations S) . s st U0,U1 are_isomorphic & U0 |= e holds
U1 |= e
let s be SortSymbol of S; ::_thesis: for e being Element of (Equations S) . s st U0,U1 are_isomorphic & U0 |= e holds
U1 |= e
let e be Element of (Equations S) . s; ::_thesis: ( U0,U1 are_isomorphic & U0 |= e implies U1 |= e )
assume that
A1: U0,U1 are_isomorphic and
A2: U0 |= e ; ::_thesis: U1 |= e
consider F being ManySortedFunction of U0,U1 such that
A3: F is_isomorphism U0,U1 by A1, MSUALG_3:def_11;
consider G being ManySortedFunction of U1,U0 such that
A4: G = F "" ;
 ( F is "1-1" & F is "onto" ) by A3, MSUALG_3:13;
then A5: G . s = (F . s) " by A4, MSUALG_3:def_4;
 F is "onto" by A3, MSUALG_3:13;
then A6: rng (F . s) = the Sorts of U1 . s by MSUALG_3:def_3;
let h1 be ManySortedFunction of (TermAlg S),U1; :: according to EQUATION:def_5 ::_thesis: ( h1 is_homomorphism TermAlg S,U1 implies (h1 . s) . (e `1) = (h1 . s) . (e `2) )
assume A7: h1 is_homomorphism TermAlg S,U1 ; ::_thesis: (h1 . s) . (e `1) = (h1 . s) . (e `2)
set F1 = G ** h1;
 G is_isomorphism U1,U0 by A3, A4, MSUALG_3:14;
then  G is_homomorphism U1,U0 by MSUALG_3:13;
then A8: G ** h1 is_homomorphism TermAlg S,U0 by A7, MSUALG_3:10;
 F is "1-1" by A3, MSUALG_3:13;
then A9: F . s is one-to-one by MSUALG_3:1;
 (G ** h1) . s = (G . s) * (h1 . s) by MSUALG_3:2;
then A10: (F . s) * ((G ** h1) . s) = ((F . s) * (G . s)) * (h1 . s) by RELAT_1:36
.= (id ( the Sorts of U1 . s)) * (h1 . s) by A5, A6, A9, FUNCT_2:29
.= h1 . s by FUNCT_2:17 ;
A11: dom ((G ** h1) . s) = the Sorts of (TermAlg S) . s by FUNCT_2:def_1;
hence (h1 . s) . (e `1) = (F . s) . (((G ** h1) . s) . (e `1)) by A10, Th29, FUNCT_1:13
.= (F . s) . (((G ** h1) . s) . (e `2)) by A2, A8, Def5
.= (h1 . s) . (e `2) by A10, A11, Th30, FUNCT_1:13 ;
::_thesis: verum
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
proof
let S be non empty non void ManySortedSign ; ::_thesis: 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
let U0, U1 be non-empty MSAlgebra over S; ::_thesis: for E being EqualSet of S st U0,U1 are_isomorphic & U0 |= E holds
U1 |= E
let E be EqualSet of S; ::_thesis: ( U0,U1 are_isomorphic & U0 |= E implies U1 |= E )
assume that
A1: U0,U1 are_isomorphic and
A2: U0 |= E ; ::_thesis: U1 |= E
let s be SortSymbol of S; :: according to EQUATION:def_6 ::_thesis: for e being Element of (Equations S) . s st e in E . s holds
U1 |= e
let e be Element of (Equations S) . s; ::_thesis: ( e in E . s implies U1 |= e )
assume  e in E . s ; ::_thesis: U1 |= e
then  U0 |= e by A2, Def6;
hence  U1 |= e by A1, Th33; ::_thesis: verum
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
proof
let S be non empty non void ManySortedSign ; ::_thesis: 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
let U0 be non-empty MSAlgebra over S; ::_thesis: 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
let s be SortSymbol of S; ::_thesis: for e being Element of (Equations S) . s
for R being MSCongruence of U0 st U0 |= e holds
QuotMSAlg (U0,R) |= e
let e be Element of (Equations S) . s; ::_thesis: for R being MSCongruence of U0 st U0 |= e holds
QuotMSAlg (U0,R) |= e
let R be MSCongruence of U0; ::_thesis: ( U0 |= e implies QuotMSAlg (U0,R) |= e )
assume A1: U0 |= e ; ::_thesis: QuotMSAlg (U0,R) |= e
set n = (MSNat_Hom (U0,R)) . s;
let h be ManySortedFunction of (TermAlg S),(QuotMSAlg (U0,R)); :: according to EQUATION:def_5 ::_thesis: ( h is_homomorphism TermAlg S, QuotMSAlg (U0,R) implies (h . s) . (e `1) = (h . s) . (e `2) )
assume  h is_homomorphism TermAlg S, QuotMSAlg (U0,R) ; ::_thesis: (h . s) . (e `1) = (h . s) . (e `2)
then consider h0 being ManySortedFunction of (TermAlg S),U0 such that
A2: h0 is_homomorphism TermAlg S,U0 and
A3: h = (MSNat_Hom (U0,R)) ** h0 by Th24, MSUALG_4:3;
A4: dom (h0 . s) = the Sorts of (TermAlg S) . s by FUNCT_2:def_1;
thus (h . s) . (e `1) = (((MSNat_Hom (U0,R)) . s) * (h0 . s)) . (e `1) by A3, MSUALG_3:2
.= ((MSNat_Hom (U0,R)) . s) . ((h0 . s) . (e `1)) by A4, Th29, FUNCT_1:13
.= ((MSNat_Hom (U0,R)) . s) . ((h0 . s) . (e `2)) by A1, A2, Def5
.= (((MSNat_Hom (U0,R)) . s) * (h0 . s)) . (e `2) by A4, Th30, FUNCT_1:13
.= (h . s) . (e `2) by A3, MSUALG_3:2 ; ::_thesis: verum
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
proof
let S be non empty non void ManySortedSign ; ::_thesis: 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
let U0 be non-empty MSAlgebra over S; ::_thesis: for E being EqualSet of S
for R being MSCongruence of U0 st U0 |= E holds
QuotMSAlg (U0,R) |= E
let E be EqualSet of S; ::_thesis: for R being MSCongruence of U0 st U0 |= E holds
QuotMSAlg (U0,R) |= E
let R be MSCongruence of U0; ::_thesis: ( U0 |= E implies QuotMSAlg (U0,R) |= E )
assume A1: U0 |= E ; ::_thesis: QuotMSAlg (U0,R) |= E
let s be SortSymbol of S; :: according to EQUATION:def_6 ::_thesis: for e being Element of (Equations S) . s st e in E . s holds
QuotMSAlg (U0,R) |= e
let e be Element of (Equations S) . s; ::_thesis: ( e in E . s implies QuotMSAlg (U0,R) |= e )
assume  e in E . s ; ::_thesis: QuotMSAlg (U0,R) |= e
then  U0 |= e by A1, Def6;
hence  QuotMSAlg (U0,R) |= e by Th35; ::_thesis: verum
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
let S be non empty non void ManySortedSign ; ::_thesis: 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
let s be SortSymbol of S; ::_thesis: 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
let e be Element of (Equations S) . s; ::_thesis: 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
reconsider e2 = e `2 as Element of the Sorts of (TermAlg S) . s by Th30;
reconsider e1 = e `1 as Element of the Sorts of (TermAlg S) . s by Th29;
let I be non empty set ; ::_thesis: for A being MSAlgebra-Family of I,S st ( for i being Element of I holds A . i |= e ) holds
product A |= e
let A be MSAlgebra-Family of I,S; ::_thesis: ( ( for i being Element of I holds A . i |= e ) implies product A |= e )
assume A1: for i being Element of I holds A . i |= e ; ::_thesis: product A |= e
let h be ManySortedFunction of (TermAlg S),(product A); :: according to EQUATION:def_5 ::_thesis: ( h is_homomorphism TermAlg S, product A implies (h . s) . (e `1) = (h . s) . (e `2) )
assume A2: h is_homomorphism TermAlg S, product A ; ::_thesis: (h . s) . (e `1) = (h . s) . (e `2)
A3: dom (h . s) = the Sorts of (TermAlg S) . s by FUNCT_2:def_1;
A4: now__::_thesis:_for_i_being_Element_of_I_holds_(proj_((Carrier_(A,s)),i))_._((h_._s)_._e1)_=_(proj_((Carrier_(A,s)),i))_._((h_._s)_._e2)
let i be Element of I; ::_thesis: (proj ((Carrier (A,s)),i)) . ((h . s) . e1) = (proj ((Carrier (A,s)),i)) . ((h . s) . e2)
set Z = (proj (A,i)) ** h;
A5: A . i |= e by A1;
 proj (A,i) is_homomorphism product A,A . i by PRALG_3:24;
then A6: (proj (A,i)) ** h is_homomorphism TermAlg S,A . i by A2, MSUALG_3:10;
thus (proj ((Carrier (A,s)),i)) . ((h . s) . e1) = ((proj (A,i)) . s) . ((h . s) . e1) by PRALG_3:def_2
.= (((proj (A,i)) . s) * (h . s)) . e1 by A3, FUNCT_1:13
.= (((proj (A,i)) ** h) . s) . e1 by MSUALG_3:2
.= (((proj (A,i)) ** h) . s) . e2 by A5, A6, Def5
.= (((proj (A,i)) . s) * (h . s)) . e2 by MSUALG_3:2
.= ((proj (A,i)) . s) . ((h . s) . e2) by A3, FUNCT_1:13
.= (proj ((Carrier (A,s)),i)) . ((h . s) . e2) by PRALG_3:def_2 ; ::_thesis: verum
end;
 the Sorts of (product A) . s = product (Carrier (A,s)) by PRALG_2:def_10;
hence  (h . s) . (e `1) = (h . s) . (e `2) by A4, MSUALG_9:14; ::_thesis: verum
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
proof
let I be set ; ::_thesis: 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
let S be non empty non void ManySortedSign ; ::_thesis: 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
let s be SortSymbol of S; ::_thesis: 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
let e be Element of (Equations S) . s; ::_thesis: 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
let F be MSAlgebra-Family of I,S; ::_thesis: ( ( for i being set st i in I holds
ex A being MSAlgebra over S st
( A = F . i & A |= e ) ) implies product F |= e )
assume A1: for i being set st i in I holds
ex A being MSAlgebra over S st
( A = F . i & A |= e ) ; ::_thesis: product F |= e
percases ( I = {} or I <> {} ) ;
suppose I = {} ; ::_thesis: product F |= e
then reconsider J = I as empty set ;
reconsider FJ = F as MSAlgebra-Family of J,S ;
thus  product F |= e ::_thesis: verum
proof
let h be ManySortedFunction of (TermAlg S),(product F); :: according to EQUATION:def_5 ::_thesis: ( h is_homomorphism TermAlg S, product F implies (h . s) . (e `1) = (h . s) . (e `2) )
assume  h is_homomorphism TermAlg S, product F ; ::_thesis: (h . s) . (e `1) = (h . s) . (e `2)
A2: the Sorts of (product FJ) . s = product (Carrier (FJ,s)) by PRALG_2:def_10
.= {{}} by CARD_3:10 ;
A3: (h . s) . (e `2) in the Sorts of (product FJ) . s by Th30, FUNCT_2:5;
 (h . s) . (e `1) in the Sorts of (product FJ) . s by Th29, FUNCT_2:5;
hence (h . s) . (e `1) = {} by A2, TARSKI:def_1
.= (h . s) . (e `2) by A2, A3, TARSKI:def_1 ;
::_thesis: verum
end;
end;
suppose I <> {} ; ::_thesis: product F |= e
then reconsider J = I as non empty set ;
reconsider F1 = F as MSAlgebra-Family of J,S ;
now__::_thesis:_for_i_being_Element_of_J_holds_F1_._i_|=_e
let i be Element of J; ::_thesis: F1 . i |= e
 ex A being MSAlgebra over S st
( A = F1 . i & A |= e ) by A1;
hence  F1 . i |= e ; ::_thesis: verum
end;
hence  product F |= e by Lm1; ::_thesis: verum
end;
end;
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
proof
let I be set ; ::_thesis: 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
let S be non empty non void ManySortedSign ; ::_thesis: 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
let E be EqualSet of S; ::_thesis: 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
let F be MSAlgebra-Family of I,S; ::_thesis: ( ( for i being set st i in I holds
ex A being MSAlgebra over S st
( A = F . i & A |= E ) ) implies product F |= E )
assume A1: for i being set st i in I holds
ex A being MSAlgebra over S st
( A = F . i & A |= E ) ; ::_thesis: product F |= E
let s be SortSymbol of S; :: according to EQUATION:def_6 ::_thesis: for e being Element of (Equations S) . s st e in E . s holds
product F |= e
let e be Element of (Equations S) . s; ::_thesis: ( e in E . s implies product F |= e )
assume A2: e in E . s ; ::_thesis: product F |= e
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
ex_A_being_MSAlgebra_over_S_st_
(_A_=_F_._i_&_A_|=_e_)
let i be set ; ::_thesis: ( i in I implies ex A being MSAlgebra over S st
( A = F . i & A |= e ) )
assume  i in I ; ::_thesis: ex A being MSAlgebra over S st
( A = F . i & A |= e )
then consider A being MSAlgebra over S such that
A3: ( A = F . i & A |= E ) by A1;
take A = A; ::_thesis: ( A = F . i & A |= e )
thus  ( A = F . i & A |= e ) by A2, A3, Def6; ::_thesis: verum
end;
hence  product F |= e by Th37; ::_thesis: verum
end;