:: ALGSPEC1 semantic presentation

begin

theorem Th1: :: ALGSPEC1:1
for f, g, h being Function st (dom f) /\ (dom g) c= dom h holds
(f +* g) +* h = (g +* f) +* h
proof
let f, g, h be Function; ::_thesis: ( (dom f) /\ (dom g) c= dom h implies (f +* g) +* h = (g +* f) +* h )
A1: dom ((g +* f) +* h) = (dom (g +* f)) \/ (dom h) by FUNCT_4:def_1;
A2: dom (f +* g) = (dom f) \/ (dom g) by FUNCT_4:def_1;
assume A3: (dom f) /\ (dom g) c= dom h ; ::_thesis: (f +* g) +* h = (g +* f) +* h
A4: now__::_thesis:_for_x_being_set_st_x_in_((dom_f)_\/_(dom_g))_\/_(dom_h)_holds_
((f_+*_g)_+*_h)_._x_=_((g_+*_f)_+*_h)_._x
let x be set ; ::_thesis: ( x in ((dom f) \/ (dom g)) \/ (dom h) implies ((f +* g) +* h) . b1 = ((g +* f) +* h) . b1 )
assume A5: x in ((dom f) \/ (dom g)) \/ (dom h) ; ::_thesis: ((f +* g) +* h) . b1 = ((g +* f) +* h) . b1
percases ( x in dom h or not x in dom h ) ;
supposeA6: x in dom h ; ::_thesis: ((f +* g) +* h) . b1 = ((g +* f) +* h) . b1
then  ((f +* g) +* h) . x = h . x by FUNCT_4:13;
hence  ((f +* g) +* h) . x = ((g +* f) +* h) . x by A6, FUNCT_4:13; ::_thesis: verum
end;
supposeA7: not x in dom h ; ::_thesis: ((f +* g) +* h) . b1 = ((g +* f) +* h) . b1
then  not x in (dom f) /\ (dom g) by A3;
then A8: ( not x in dom f or not x in dom g ) by XBOOLE_0:def_4;
A9: ((f +* g) +* h) . x = (f +* g) . x by A7, FUNCT_4:11;
 x in (dom g) \/ (dom f) by A5, A7, XBOOLE_0:def_3;
then  ( x in dom f or x in dom g ) by XBOOLE_0:def_3;
then  ( ( (f +* g) . x = f . x & (g +* f) . x = f . x ) or ( (f +* g) . x = g . x & (g +* f) . x = g . x ) ) by A8, FUNCT_4:11, FUNCT_4:13;
hence  ((f +* g) +* h) . x = ((g +* f) +* h) . x by A7, A9, FUNCT_4:11; ::_thesis: verum
end;
end;
end;
A10: dom (g +* f) = (dom g) \/ (dom f) by FUNCT_4:def_1;
 dom ((f +* g) +* h) = (dom (f +* g)) \/ (dom h) by FUNCT_4:def_1;
hence  (f +* g) +* h = (g +* f) +* h by A1, A2, A10, A4, FUNCT_1:2; ::_thesis: verum
end;

theorem Th2: :: ALGSPEC1:2
for f, g, h being Function st f c= g & (rng h) /\ (dom g) c= dom f holds
g * h = f * h
proof
let f, g, h be Function; ::_thesis: ( f c= g & (rng h) /\ (dom g) c= dom f implies g * h = f * h )
assume that
A1: f c= g and
A2: (rng h) /\ (dom g) c= dom f ; ::_thesis: g * h = f * h
A3: dom (f * h) = dom (g * h)
proof
 f * h c= g * h by A1, RELAT_1:29;
hence  dom (f * h) c= dom (g * h) by RELAT_1:11; :: according to XBOOLE_0:def_10 ::_thesis: dom (g * h) c= dom (f * h)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (g * h) or x in dom (f * h) )
assume A4: x in dom (g * h) ; ::_thesis: x in dom (f * h)
then A5: h . x in dom g by FUNCT_1:11;
A6: x in dom h by A4, FUNCT_1:11;
then  h . x in rng h by FUNCT_1:def_3;
then  h . x in (rng h) /\ (dom g) by A5, XBOOLE_0:def_4;
hence  x in dom (f * h) by A2, A6, FUNCT_1:11; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_dom_(f_*_h)_holds_
(g_*_h)_._x_=_(f_*_h)_._x
let x be set ; ::_thesis: ( x in dom (f * h) implies (g * h) . x = (f * h) . x )
assume A7: x in dom (f * h) ; ::_thesis: (g * h) . x = (f * h) . x
then A8: x in dom h by FUNCT_1:11;
then A9: (g * h) . x = g . (h . x) by FUNCT_1:13;
A10: (f * h) . x = f . (h . x) by A8, FUNCT_1:13;
 h . x in dom f by A7, FUNCT_1:11;
hence  (g * h) . x = (f * h) . x by A1, A9, A10, GRFUNC_1:2; ::_thesis: verum
end;
hence  g * h = f * h by A3, FUNCT_1:2; ::_thesis: verum
end;

theorem Th3: :: ALGSPEC1:3
for f, g, h being Function st dom f misses rng h & g .: (dom h) misses dom f holds
f * (g +* h) = f * g
proof
let f, g, h be Function; ::_thesis: ( dom f misses rng h & g .: (dom h) misses dom f implies f * (g +* h) = f * g )
assume that
A1: dom f misses rng h and
A2: g .: (dom h) misses dom f ; ::_thesis: f * (g +* h) = f * g
A3: dom (f * g) = dom (f * (g +* h))
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: dom (f * (g +* h)) c= dom (f * g)
let x be set ; ::_thesis: ( x in dom (f * g) implies x in dom (f * (g +* h)) )
assume A4: x in dom (f * g) ; ::_thesis: x in dom (f * (g +* h))
then A5: x in dom g by FUNCT_1:11;
A6: g . x in dom f by A4, FUNCT_1:11;
now__::_thesis:_not_x_in_dom_h
assume  x in dom h ; ::_thesis: contradiction
then  g . x in g .: (dom h) by A5, FUNCT_1:def_6;
hence  contradiction by A2, A6, XBOOLE_0:3; ::_thesis: verum
end;
then A7: g . x = (g +* h) . x by FUNCT_4:11;
 x in dom (g +* h) by A5, FUNCT_4:12;
hence  x in dom (f * (g +* h)) by A6, A7, FUNCT_1:11; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (f * (g +* h)) or x in dom (f * g) )
assume A8: x in dom (f * (g +* h)) ; ::_thesis: x in dom (f * g)
then  x in dom (g +* h) by FUNCT_1:11;
then  ( ( x in dom g & not x in dom h ) or x in dom h ) by FUNCT_4:12;
then A9: ( ( x in dom g & (g +* h) . x = g . x ) or ( (g +* h) . x = h . x & h . x in rng h ) ) by FUNCT_1:def_3, FUNCT_4:11, FUNCT_4:13;
 (g +* h) . x in dom f by A8, FUNCT_1:11;
hence  x in dom (f * g) by A1, A9, FUNCT_1:11, XBOOLE_0:3; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_dom_(f_*_g)_holds_
(f_*_(g_+*_h))_._x_=_(f_*_g)_._x
let x be set ; ::_thesis: ( x in dom (f * g) implies (f * (g +* h)) . x = (f * g) . x )
assume A10: x in dom (f * g) ; ::_thesis: (f * (g +* h)) . x = (f * g) . x
then A11: x in dom g by FUNCT_1:11;
A12: g . x in dom f by A10, FUNCT_1:11;
now__::_thesis:_not_x_in_dom_h
assume  x in dom h ; ::_thesis: contradiction
then  g . x in g .: (dom h) by A11, FUNCT_1:def_6;
hence  contradiction by A2, A12, XBOOLE_0:3; ::_thesis: verum
end;
then A13: g . x = (g +* h) . x by FUNCT_4:11;
 x in dom (g +* h) by A11, FUNCT_4:12;
hence (f * (g +* h)) . x = f . (g . x) by A13, FUNCT_1:13
.= (f * g) . x by A11, FUNCT_1:13 ;
::_thesis: verum
end;
hence  f * (g +* h) = f * g by A3, FUNCT_1:2; ::_thesis: verum
end;

theorem Th4: :: ALGSPEC1:4
for f1, f2, g1, g2 being Function st f1 tolerates f2 & g1 tolerates g2 holds
f1 * g1 tolerates f2 * g2
proof
let f1, f2, g1, g2 be Function; ::_thesis: ( f1 tolerates f2 & g1 tolerates g2 implies f1 * g1 tolerates f2 * g2 )
assume that
A1: for x being set st x in (dom f1) /\ (dom f2) holds
f1 . x = f2 . x and
A2: for x being set st x in (dom g1) /\ (dom g2) holds
g1 . x = g2 . x ; :: according to PARTFUN1:def_4 ::_thesis: f1 * g1 tolerates f2 * g2
let x be set ; :: according to PARTFUN1:def_4 ::_thesis: ( not x in (dom (f1 * g1)) /\ (dom (f2 * g2)) or (f1 * g1) . x = (f2 * g2) . x )
assume A3: x in (dom (f1 * g1)) /\ (dom (f2 * g2)) ; ::_thesis: (f1 * g1) . x = (f2 * g2) . x
then A4: x in dom (f1 * g1) by XBOOLE_0:def_4;
then A5: x in dom g1 by FUNCT_1:11;
then A6: (f1 * g1) . x = f1 . (g1 . x) by FUNCT_1:13;
A7: x in dom (f2 * g2) by A3, XBOOLE_0:def_4;
then A8: x in dom g2 by FUNCT_1:11;
then A9: (f2 * g2) . x = f2 . (g2 . x) by FUNCT_1:13;
 x in (dom g1) /\ (dom g2) by A5, A8, XBOOLE_0:def_4;
then A10: g1 . x = g2 . x by A2;
A11: g2 . x in dom f2 by A7, FUNCT_1:11;
 g1 . x in dom f1 by A4, FUNCT_1:11;
then  g1 . x in (dom f1) /\ (dom f2) by A11, A10, XBOOLE_0:def_4;
hence  (f1 * g1) . x = (f2 * g2) . x by A1, A10, A6, A9; ::_thesis: verum
end;

theorem Th5: :: ALGSPEC1:5
for X1, Y1, X2, Y2 being non empty set
for f being Function of X1,X2
for g being Function of Y1,Y2 st f c= g holds
f * c= g *
proof
let X1, Y1, X2, Y2 be non empty set ; ::_thesis: for f being Function of X1,X2
for g being Function of Y1,Y2 st f c= g holds
f * c= g *
let f be Function of X1,X2; ::_thesis: for g being Function of Y1,Y2 st f c= g holds
f * c= g *
let g be Function of Y1,Y2; ::_thesis: ( f c= g implies f * c= g * )
A1: dom g = Y1 by FUNCT_2:def_1;
assume A2: f c= g ; ::_thesis: f * c= g *
A3: dom f = X1 by FUNCT_2:def_1;
then A4: X1 * c= Y1 * by A1, A2, FINSEQ_1:62, RELAT_1:11;
A5: now__::_thesis:_for_x_being_set_st_x_in_X1_*_holds_
(f_*)_._x_=_(g_*)_._x
let x be set ; ::_thesis: ( x in X1 * implies (f *) . x = (g *) . x )
assume  x in X1 * ; ::_thesis: (f *) . x = (g *) . x
then reconsider p = x as Element of X1 * ;
A6: (f *) . p = f * p by LANG1:def_13;
 (rng p) /\ Y1 c= X1 ;
then A7: f * p = g * p by A3, A1, A2, Th2;
 p in X1 * ;
hence  (f *) . x = (g *) . x by A4, A6, A7, LANG1:def_13; ::_thesis: verum
end;
A8: dom (g *) = Y1 * by FUNCT_2:def_1;
 dom (f *) = X1 * by FUNCT_2:def_1;
hence  f * c= g * by A8, A4, A5, GRFUNC_1:2; ::_thesis: verum
end;

theorem Th6: :: ALGSPEC1:6
for X1, Y1, X2, Y2 being non empty set
for f being Function of X1,X2
for g being Function of Y1,Y2 st f tolerates g holds
f * tolerates g *
proof
let X1, Y1, X2, Y2 be non empty set ; ::_thesis: for f being Function of X1,X2
for g being Function of Y1,Y2 st f tolerates g holds
f * tolerates g *
let f be Function of X1,X2; ::_thesis: for g being Function of Y1,Y2 st f tolerates g holds
f * tolerates g *
let g be Function of Y1,Y2; ::_thesis: ( f tolerates g implies f * tolerates g * )
A1: dom g = Y1 by FUNCT_2:def_1;
assume A2: for x being set st x in (dom f) /\ (dom g) holds
f . x = g . x ; :: according to PARTFUN1:def_4 ::_thesis: f * tolerates g *
let x be set ; :: according to PARTFUN1:def_4 ::_thesis: ( not x in (dom (f *)) /\ (dom (g *)) or (f *) . x = (g *) . x )
assume A3: x in (dom (f *)) /\ (dom (g *)) ; ::_thesis: (f *) . x = (g *) . x
then reconsider q = x as Element of Y1 * ;
A4: (g *) . x = g * q by LANG1:def_13;
 x in dom (f *) by A3, XBOOLE_0:def_4;
then reconsider p = x as Element of X1 * ;
A5: dom f = X1 by FUNCT_2:def_1;
A6: now__::_thesis:_for_i_being_set_st_i_in_dom_p_holds_
(f_*_p)_._i_=_(g_*_q)_._i
let i be set ; ::_thesis: ( i in dom p implies (f * p) . i = (g * q) . i )
assume A7: i in dom p ; ::_thesis: (f * p) . i = (g * q) . i
then A8: q . i in rng q by FUNCT_1:def_3;
 p . i in rng p by A7, FUNCT_1:def_3;
then  p . i in (dom f) /\ (dom g) by A5, A1, A8, XBOOLE_0:def_4;
then f . (p . i) = g . (q . i) by A2
.= (g * q) . i by A7, FUNCT_1:13 ;
hence  (f * p) . i = (g * q) . i by A7, FUNCT_1:13; ::_thesis: verum
end;
 rng q c= Y1 ;
then A9: dom (g * q) = dom q by A1, RELAT_1:27;
 rng p c= X1 ;
then A10: dom (f * p) = dom p by A5, RELAT_1:27;
 (f *) . x = f * p by LANG1:def_13;
hence  (f *) . x = (g *) . x by A4, A10, A9, A6, FUNCT_1:2; ::_thesis: verum
end;

definition
let X be set ;
let f be Function;
funcX -indexing f ->  ManySortedSet of X equals :: ALGSPEC1:def 1
(id X) +* (f | X);
coherence
 (id X) +* (f | X) is ManySortedSet of X
proof
 dom (id X) = X ;
then  dom ((id X) +* (f | X)) = X \/ (dom (f | X)) by FUNCT_4:def_1;
then  dom ((id X) +* (f | X)) = X by RELAT_1:58, XBOOLE_1:12;
hence  (id X) +* (f | X) is ManySortedSet of X by PARTFUN1:def_2, RELAT_1:def_18; ::_thesis: verum
end;
end;

:: deftheorem  defines -indexing ALGSPEC1:def_1_:_
 for X being set
for f being Function holds X -indexing f = (id X) +* (f | X);

theorem Th7: :: ALGSPEC1:7
for X being set
for f being Function holds rng (X -indexing f) = (X \ (dom f)) \/ (f .: X)
proof
let X be set ; ::_thesis: for f being Function holds rng (X -indexing f) = (X \ (dom f)) \/ (f .: X)
let f be Function; ::_thesis: rng (X -indexing f) = (X \ (dom f)) \/ (f .: X)
 dom (id X) = X ;
hence  rng (X -indexing f) = ((id X) .: (X \ (dom (f | X)))) \/ (rng (f | X)) by FRECHET:12
.= ((id X) .: (X \ (dom (f | X)))) \/ (f .: X) by RELAT_1:115
.= (X \ (dom (f | X))) \/ (f .: X) by FUNCT_1:92
.= (X \ ((dom f) /\ X)) \/ (f .: X) by RELAT_1:61
.= (X \ (dom f)) \/ (f .: X) by XBOOLE_1:47 ;
::_thesis: verum
end;

theorem Th8: :: ALGSPEC1:8
for X being non empty set
for f being Function
for x being Element of X holds (X -indexing f) . x = ((id X) +* f) . x
proof
let X be non empty set ; ::_thesis: for f being Function
for x being Element of X holds (X -indexing f) . x = ((id X) +* f) . x
let f be Function; ::_thesis: for x being Element of X holds (X -indexing f) . x = ((id X) +* f) . x
let x be Element of X; ::_thesis: (X -indexing f) . x = ((id X) +* f) . x
((id X) +* f) | X = ((id X) | X) +* (f | X) by FUNCT_4:71
.= ((id X) | (dom (id X))) +* (f | X)
.= X -indexing f ;
hence  (X -indexing f) . x = ((id X) +* f) . x by FUNCT_1:49; ::_thesis: verum
end;

theorem Th9: :: ALGSPEC1:9
for X, x being set
for f being Function st x in X holds
( ( x in dom f implies (X -indexing f) . x = f . x ) & ( not x in dom f implies (X -indexing f) . x = x ) )
proof
let X, x be set ; ::_thesis: for f being Function st x in X holds
( ( x in dom f implies (X -indexing f) . x = f . x ) & ( not x in dom f implies (X -indexing f) . x = x ) )
let f be Function; ::_thesis: ( x in X implies ( ( x in dom f implies (X -indexing f) . x = f . x ) & ( not x in dom f implies (X -indexing f) . x = x ) ) )
assume A1: x in X ; ::_thesis: ( ( x in dom f implies (X -indexing f) . x = f . x ) & ( not x in dom f implies (X -indexing f) . x = x ) )
then A2: (id X) . x = x by FUNCT_1:18;
 (X -indexing f) . x = ((id X) +* f) . x by A1, Th8;
hence  ( ( x in dom f implies (X -indexing f) . x = f . x ) & ( not x in dom f implies (X -indexing f) . x = x ) ) by A2, FUNCT_4:11, FUNCT_4:13; ::_thesis: verum
end;

theorem Th10: :: ALGSPEC1:10
for X being set
for f being Function st dom f = X holds
X -indexing f = f
proof
let X be set ; ::_thesis: for f being Function st dom f = X holds
X -indexing f = f
let f be Function; ::_thesis: ( dom f = X implies X -indexing f = f )
A1: dom (id X) = X ;
assume A2: dom f = X ; ::_thesis: X -indexing f = f
then  f | X = f by RELAT_1:68;
hence  X -indexing f = f by A2, A1, FUNCT_4:19; ::_thesis: verum
end;

theorem Th11: :: ALGSPEC1:11
for X being set
for f being Function holds X -indexing (X -indexing f) = X -indexing f
proof
let X be set ; ::_thesis: for f being Function holds X -indexing (X -indexing f) = X -indexing f
let f be Function; ::_thesis: X -indexing (X -indexing f) = X -indexing f
 dom (X -indexing f) = X by PARTFUN1:def_2;
then  for x being set st x in X holds
(X -indexing (X -indexing f)) . x = (X -indexing f) . x by Th9;
hence  X -indexing (X -indexing f) = X -indexing f by PBOOLE:3; ::_thesis: verum
end;

theorem Th12: :: ALGSPEC1:12
for X being set
for f being Function holds X -indexing ((id X) +* f) = X -indexing f
proof
let X be set ; ::_thesis: for f being Function holds X -indexing ((id X) +* f) = X -indexing f
let f be Function; ::_thesis: X -indexing ((id X) +* f) = X -indexing f
thus X -indexing ((id X) +* f) = (id X) +* (((id X) | X) +* (f | X)) by FUNCT_4:71
.= (id X) +* ((id X) +* (f | X))
.= ((id X) +* (id X)) +* (f | X) by FUNCT_4:14
.= X -indexing f ; ::_thesis: verum
end;

theorem :: ALGSPEC1:13
for X being set
for f being Function st f c= id X holds
X -indexing f = id X
proof
let X be set ; ::_thesis: for f being Function st f c= id X holds
X -indexing f = id X
let f be Function; ::_thesis: ( f c= id X implies X -indexing f = id X )
assume  f c= id X ; ::_thesis: X -indexing f = id X
then  (id X) +* f = id X by FUNCT_4:98;
hence X -indexing f = X -indexing (id X) by Th12
.= id X ;
::_thesis: verum
end;

theorem :: ALGSPEC1:14
for X being set holds X -indexing {} = id X ;

theorem :: ALGSPEC1:15
for X being set
for f being Function st X c= dom f holds
X -indexing f = f | X
proof
let X be set ; ::_thesis: for f being Function st X c= dom f holds
X -indexing f = f | X
let f be Function; ::_thesis: ( X c= dom f implies X -indexing f = f | X )
assume  X c= dom f ; ::_thesis: X -indexing f = f | X
then A1: dom (f | X) = X by RELAT_1:62;
thus X -indexing f = X -indexing (f | X)
.= f | X by A1, Th10 ; ::_thesis: verum
end;

theorem :: ALGSPEC1:16
for f being Function holds {} -indexing f = {} ;

theorem Th17: :: ALGSPEC1:17
for X, Y being set
for f being Function st X c= Y holds
(Y -indexing f) | X = X -indexing f
proof
let X, Y be set ; ::_thesis: for f being Function st X c= Y holds
(Y -indexing f) | X = X -indexing f
let f be Function; ::_thesis: ( X c= Y implies (Y -indexing f) | X = X -indexing f )
assume A1: X c= Y ; ::_thesis: (Y -indexing f) | X = X -indexing f
then A2: (f | Y) | X = f | X by RELAT_1:74;
 (id Y) | X = id X by A1, FUNCT_3:1;
hence  (Y -indexing f) | X = X -indexing f by A2, FUNCT_4:71; ::_thesis: verum
end;

theorem Th18: :: ALGSPEC1:18
for X, Y being set
for f being Function holds (X \/ Y) -indexing f = (X -indexing f) +* (Y -indexing f)
proof
let X, Y be set ; ::_thesis: for f being Function holds (X \/ Y) -indexing f = (X -indexing f) +* (Y -indexing f)
let f be Function; ::_thesis: (X \/ Y) -indexing f = (X -indexing f) +* (Y -indexing f)
set Z = X \/ Y;
A1: f | Y c= f by RELAT_1:59;
 f | X c= f by RELAT_1:59;
then  f | X tolerates f | Y by A1, PARTFUN1:52;
then A2: (f | X) \/ (f | Y) = (f | X) +* (f | Y) by FUNCT_4:30;
 dom (f | X) = (dom f) /\ X by RELAT_1:61;
then A3: dom (f | X) c= dom f by XBOOLE_1:17;
 dom (f | Y) = (dom f) /\ Y by RELAT_1:61;
then A4: (dom (f | X)) /\ (dom (id Y)) c= dom (f | Y) by A3, XBOOLE_1:27;
thus (X \/ Y) -indexing f = ((id X) +* (id Y)) +* (f | (X \/ Y)) by FUNCT_4:22
.= ((id X) +* (id Y)) +* ((f | X) +* (f | Y)) by A2, RELAT_1:78
.= (id X) +* ((id Y) +* ((f | X) +* (f | Y))) by FUNCT_4:14
.= (id X) +* (((id Y) +* (f | X)) +* (f | Y)) by FUNCT_4:14
.= (id X) +* (((f | X) +* (id Y)) +* (f | Y)) by A4, Th1
.= (id X) +* ((f | X) +* ((id Y) +* (f | Y))) by FUNCT_4:14
.= (X -indexing f) +* (Y -indexing f) by FUNCT_4:14 ; ::_thesis: verum
end;

theorem Th19: :: ALGSPEC1:19
for X, Y being set
for f being Function holds X -indexing f tolerates Y -indexing f
proof
let X, Y be set ; ::_thesis: for f being Function holds X -indexing f tolerates Y -indexing f
let f be Function; ::_thesis: X -indexing f tolerates Y -indexing f
 Y -indexing f = ((X \/ Y) -indexing f) | Y by Th17, XBOOLE_1:7;
then A1: Y -indexing f c= (X \/ Y) -indexing f by RELAT_1:59;
 X -indexing f = ((X \/ Y) -indexing f) | X by Th17, XBOOLE_1:7;
then  X -indexing f c= (X \/ Y) -indexing f by RELAT_1:59;
hence  X -indexing f tolerates Y -indexing f by A1, PARTFUN1:52; ::_thesis: verum
end;

theorem Th20: :: ALGSPEC1:20
for X, Y being set
for f being Function holds (X \/ Y) -indexing f = (X -indexing f) \/ (Y -indexing f)
proof
let X, Y be set ; ::_thesis: for f being Function holds (X \/ Y) -indexing f = (X -indexing f) \/ (Y -indexing f)
let f be Function; ::_thesis: (X \/ Y) -indexing f = (X -indexing f) \/ (Y -indexing f)
A1: X -indexing f tolerates Y -indexing f by Th19;
 (X \/ Y) -indexing f = (X -indexing f) +* (Y -indexing f) by Th18;
hence  (X \/ Y) -indexing f = (X -indexing f) \/ (Y -indexing f) by A1, FUNCT_4:30; ::_thesis: verum
end;

theorem Th21: :: ALGSPEC1:21
for X being non empty set
for f, g being Function st rng g c= X holds
(X -indexing f) * g = ((id X) +* f) * g
proof
let X be non empty set ; ::_thesis: for f, g being Function st rng g c= X holds
(X -indexing f) * g = ((id X) +* f) * g
let f, g be Function; ::_thesis: ( rng g c= X implies (X -indexing f) * g = ((id X) +* f) * g )
assume A1: rng g c= X ; ::_thesis: (X -indexing f) * g = ((id X) +* f) * g
 rng g c= dom (X -indexing f) by A1, PARTFUN1:def_2;
then A2: dom ((X -indexing f) * g) = dom g by RELAT_1:27;
A3: now__::_thesis:_for_x_being_set_st_x_in_dom_g_holds_
((X_-indexing_f)_*_g)_._x_=_(((id_X)_+*_f)_*_g)_._x
let x be set ; ::_thesis: ( x in dom g implies ((X -indexing f) * g) . x = (((id X) +* f) * g) . x )
assume A4: x in dom g ; ::_thesis: ((X -indexing f) * g) . x = (((id X) +* f) * g) . x
then A5: (((id X) +* f) * g) . x = ((id X) +* f) . (g . x) by FUNCT_1:13;
A6: g . x in rng g by A4, FUNCT_1:def_3;
 ((X -indexing f) * g) . x = (X -indexing f) . (g . x) by A4, FUNCT_1:13;
hence  ((X -indexing f) * g) . x = (((id X) +* f) * g) . x by A1, A5, A6, Th8; ::_thesis: verum
end;
 dom (id X) = X ;
then A7: dom ((id X) +* f) = X \/ (dom f) by FUNCT_4:def_1;
 X c= X \/ (dom f) by XBOOLE_1:7;
then  dom (((id X) +* f) * g) = dom g by A1, A7, RELAT_1:27, XBOOLE_1:1;
hence  (X -indexing f) * g = ((id X) +* f) * g by A2, A3, FUNCT_1:2; ::_thesis: verum
end;

theorem :: ALGSPEC1:22
for f, g being Function st dom f misses dom g & rng g misses dom f holds
for X being set holds f * (X -indexing g) = f | X
proof
let f, g be Function; ::_thesis: ( dom f misses dom g & rng g misses dom f implies for X being set holds f * (X -indexing g) = f | X )
assume that
A1: dom f misses dom g and
A2: rng g misses dom f ; ::_thesis: for X being set holds f * (X -indexing g) = f | X
let X be set ; ::_thesis: f * (X -indexing g) = f | X
A3: dom (f | X) c= dom f by RELAT_1:60;
A4: (id X) .: (dom (g | X)) c= dom (g | X)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (id X) .: (dom (g | X)) or x in dom (g | X) )
assume  x in (id X) .: (dom (g | X)) ; ::_thesis: x in dom (g | X)
then  ex y being set st
( y in dom (id X) & y in dom (g | X) & x = (id X) . y ) by FUNCT_1:def_6;
hence  x in dom (g | X) by FUNCT_1:18; ::_thesis: verum
end;
 dom (g | X) c= dom g by RELAT_1:60;
then  dom (f | X) misses dom (g | X) by A1, A3, XBOOLE_1:64;
then A5: (id X) .: (dom (g | X)) misses dom (f | X) by A4, XBOOLE_1:64;
A6: dom (f | X) c= X by RELAT_1:58;
 rng (g | X) c= rng g by RELAT_1:70;
then A7: dom (f | X) misses rng (g | X) by A2, A3, XBOOLE_1:64;
 g .: X c= rng g by RELAT_1:111;
then  g .: X misses dom f by A2, XBOOLE_1:64;
then A8: (g .: X) /\ (dom f) = {} by XBOOLE_0:def_7;
 rng (X -indexing g) = (X \ (dom g)) \/ (g .: X) by Th7;
then (rng (X -indexing g)) /\ (dom f) = ((X \ (dom g)) /\ (dom f)) \/ ((g .: X) /\ (dom f)) by XBOOLE_1:23
.= (X \ (dom g)) /\ (dom f) by A8 ;
then  (rng (X -indexing g)) /\ (dom f) c= X /\ (dom f) by XBOOLE_1:26;
then  (rng (X -indexing g)) /\ (dom f) c= dom (f | X) by RELAT_1:61;
hence f * (X -indexing g) = (f | X) * ((id X) +* (g | X)) by Th2, RELAT_1:59
.= (f | X) * (id X) by A7, A5, Th3
.= f | X by A6, RELAT_1:51 ;
::_thesis: verum
end;

definition
let f be Function;
mode rng-retract of f ->  Function means :Def2: :: ALGSPEC1:def 2
( dom it = rng f & f * it = id (rng f) );
existence
 ex b1 being Function st
( dom b1 = rng f & f * b1 = id (rng f) )
proof
defpred S1[ set , set ] means f . $2 = $1;
A1: dom (id (rng f)) = rng f ;
A2: for o being set st o in rng f holds
ex y being set st
( y in dom f & S1[o,y] ) by FUNCT_1:def_3;
consider g being Function such that
A3: ( dom g = rng f & rng g c= dom f ) and
A4: for o being set st o in rng f holds
S1[o,g . o] from FUNCT_1:sch_5(A2);
A5: now__::_thesis:_for_x_being_set_st_x_in_rng_f_holds_
(f_*_g)_._x_=_(id_(rng_f))_._x
let x be set ; ::_thesis: ( x in rng f implies (f * g) . x = (id (rng f)) . x )
assume A6: x in rng f ; ::_thesis: (f * g) . x = (id (rng f)) . x
then A7: (f * g) . x = f . (g . x) by A3, FUNCT_1:13;
 f . (g . x) = x by A4, A6;
hence  (f * g) . x = (id (rng f)) . x by A6, A7, FUNCT_1:18; ::_thesis: verum
end;
take  g ; ::_thesis: ( dom g = rng f & f * g = id (rng f) )
thus  dom g = rng f by A3; ::_thesis: f * g = id (rng f)
 dom (f * g) = rng f by A3, RELAT_1:27;
hence  f * g = id (rng f) by A1, A5, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines rng-retract ALGSPEC1:def_2_:_
 for f, b2 being Function holds
( b2 is rng-retract of f iff ( dom b2 = rng f & f * b2 = id (rng f) ) );

theorem Th23: :: ALGSPEC1:23
for f being Function
for g being rng-retract of f holds rng g c= dom f
proof
let f, g be Function; ::_thesis: ( g is rng-retract of f implies rng g c= dom f )
assume that
A1: dom g = rng f and
A2: f * g = id (rng f) ; :: according to ALGSPEC1:def_2 ::_thesis: rng g c= dom f
 dom g = dom (f * g) by A1, A2, RELAT_1:45;
hence  rng g c= dom f by FUNCT_1:15; ::_thesis: verum
end;

theorem Th24: :: ALGSPEC1:24
for f being Function
for g being rng-retract of f
for x being set st x in rng f holds
( g . x in dom f & f . (g . x) = x )
proof
let f be Function; ::_thesis: for g being rng-retract of f
for x being set st x in rng f holds
( g . x in dom f & f . (g . x) = x )
let g be rng-retract of f; ::_thesis: for x being set st x in rng f holds
( g . x in dom f & f . (g . x) = x )
let x be set ; ::_thesis: ( x in rng f implies ( g . x in dom f & f . (g . x) = x ) )
assume A1: x in rng f ; ::_thesis: ( g . x in dom f & f . (g . x) = x )
A2: rng g c= dom f by Th23;
A3: dom g = rng f by Def2;
then  g . x in rng g by A1, FUNCT_1:def_3;
hence  g . x in dom f by A2; ::_thesis: f . (g . x) = x
thus f . (g . x) = (f * g) . x by A1, A3, FUNCT_1:13
.= (id (rng f)) . x by Def2
.= x by A1, FUNCT_1:18 ; ::_thesis: verum
end;

theorem :: ALGSPEC1:25
for f being Function st f is one-to-one holds
f " is rng-retract of f
proof
let f be Function; ::_thesis: ( f is one-to-one implies f " is rng-retract of f )
assume  f is one-to-one ; ::_thesis: f " is rng-retract of f
hence  ( dom (f ") = rng f & f * (f ") = id (rng f) ) by FUNCT_1:32, FUNCT_1:39; :: according to ALGSPEC1:def_2 ::_thesis: verum
end;

theorem :: ALGSPEC1:26
for f being Function st f is one-to-one holds
for g being rng-retract of f holds g = f "
proof
let f be Function; ::_thesis: ( f is one-to-one implies for g being rng-retract of f holds g = f " )
assume A1: f is one-to-one ; ::_thesis: for g being rng-retract of f holds g = f "
let g be rng-retract of f; ::_thesis: g = f "
A2: rng f = dom g by Def2;
A3: rng g = dom f
proof
thus  rng g c= dom f by Th23; :: according to XBOOLE_0:def_10 ::_thesis: dom f c= rng g
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom f or x in rng g )
assume A4: x in dom f ; ::_thesis: x in rng g
then A5: f . x in rng f by FUNCT_1:def_3;
then A6: g . (f . x) in dom f by Th24;
 f . (g . (f . x)) = f . x by A5, Th24;
then  x = g . (f . x) by A1, A4, A6, FUNCT_1:def_4;
hence  x in rng g by A2, A5, FUNCT_1:def_3; ::_thesis: verum
end;
now__::_thesis:_for_x,_y_being_set_st_x_in_dom_f_&_y_in_dom_g_holds_
(_f_._x_=_y_iff_g_._y_=_x_)
let x, y be set ; ::_thesis: ( x in dom f & y in dom g implies ( f . x = y iff g . y = x ) )
assume that
A7: x in dom f and
A8: y in dom g ; ::_thesis: ( f . x = y iff g . y = x )
A9: g . y in rng g by A8, FUNCT_1:def_3;
 f . (g . y) = y by A2, A8, Th24;
hence  ( f . x = y iff g . y = x ) by A1, A3, A7, A9, FUNCT_1:def_4; ::_thesis: verum
end;
hence  g = f " by A1, A2, A3, FUNCT_1:38; ::_thesis: verum
end;

theorem Th27: :: ALGSPEC1:27
for f1, f2 being Function st f1 tolerates f2 holds
for g1 being rng-retract of f1
for g2 being rng-retract of f2 holds g1 +* g2 is rng-retract of f1 +* f2
proof
let f1, f2 be Function; ::_thesis: ( f1 tolerates f2 implies for g1 being rng-retract of f1
for g2 being rng-retract of f2 holds g1 +* g2 is rng-retract of f1 +* f2 )
assume A1: f1 tolerates f2 ; ::_thesis: for g1 being rng-retract of f1
for g2 being rng-retract of f2 holds g1 +* g2 is rng-retract of f1 +* f2
then A2: f1 +* f2 = f1 \/ f2 by FUNCT_4:30;
let g1 be rng-retract of f1; ::_thesis: for g2 being rng-retract of f2 holds g1 +* g2 is rng-retract of f1 +* f2
let g2 be rng-retract of f2; ::_thesis: g1 +* g2 is rng-retract of f1 +* f2
A3: dom g1 = rng f1 by Def2;
A4: dom g2 = rng f2 by Def2;
thus  dom (g1 +* g2) = (dom g1) \/ (dom g2) by FUNCT_4:def_1
.= rng (f1 +* f2) by A2, A3, A4, RELAT_1:12 ; :: according to ALGSPEC1:def_2 ::_thesis: (f1 +* f2) * (g1 +* g2) = id (rng (f1 +* f2))
A5: rng g2 c= dom f2 by Th23;
 rng g1 c= dom f1 by Th23;
hence (f1 +* f2) * (g1 +* g2) = (f1 * g1) +* (f2 * g2) by A1, A5, FUNCT_4:69
.= (id (rng f1)) +* (f2 * g2) by Def2
.= (id (rng f1)) +* (id (rng f2)) by Def2
.= id ((rng f1) \/ (rng f2)) by FUNCT_4:22
.= id (rng (f1 +* f2)) by A2, RELAT_1:12 ;
::_thesis: verum
end;

theorem :: ALGSPEC1:28
for f1, f2 being Function st f1 c= f2 holds
for g1 being rng-retract of f1 ex g2 being rng-retract of f2 st g1 c= g2
proof
let f1, f2 be Function; ::_thesis: ( f1 c= f2 implies for g1 being rng-retract of f1 ex g2 being rng-retract of f2 st g1 c= g2 )
assume A1: f1 c= f2 ; ::_thesis: for g1 being rng-retract of f1 ex g2 being rng-retract of f2 st g1 c= g2
A2: f2 +* f1 = f2 by A1, FUNCT_4:98;
set g = the rng-retract of f2;
let g1 be rng-retract of f1; ::_thesis: ex g2 being rng-retract of f2 st g1 c= g2
 f1 tolerates f2 by A1, PARTFUN1:52;
then reconsider g2 = the rng-retract of f2 +* g1 as rng-retract of f2 by A2, Th27;
take  g2 ; ::_thesis: g1 c= g2
thus  g1 c= g2 by FUNCT_4:25; ::_thesis: verum
end;

begin

definition
let S be non empty non void ManySortedSign ;
let f, g be Function;
predf,g form_a_replacement_in S means :Def3: :: ALGSPEC1:def 3
 for o1, o2 being OperSymbol of S st ((id the carrier' of S) +* g) . o1 = ((id the carrier' of S) +* g) . o2 holds
( ((id the carrier of S) +* f) * (the_arity_of o1) = ((id the carrier of S) +* f) * (the_arity_of o2) & ((id the carrier of S) +* f) . (the_result_sort_of o1) = ((id the carrier of S) +* f) . (the_result_sort_of o2) );
end;

:: deftheorem Def3 defines form_a_replacement_in ALGSPEC1:def_3_:_
 for S being non empty non void ManySortedSign
for f, g being Function holds
( f,g form_a_replacement_in S iff for o1, o2 being OperSymbol of S st ((id the carrier' of S) +* g) . o1 = ((id the carrier' of S) +* g) . o2 holds
( ((id the carrier of S) +* f) * (the_arity_of o1) = ((id the carrier of S) +* f) * (the_arity_of o2) & ((id the carrier of S) +* f) . (the_result_sort_of o1) = ((id the carrier of S) +* f) . (the_result_sort_of o2) ) );

theorem Th29: :: ALGSPEC1:29
for S being non empty non void ManySortedSign
for f, g being Function holds
( f,g form_a_replacement_in S iff for o1, o2 being OperSymbol of S st ( the carrier' of S -indexing g) . o1 = ( the carrier' of S -indexing g) . o2 holds
( ( the carrier of S -indexing f) * (the_arity_of o1) = ( the carrier of S -indexing f) * (the_arity_of o2) & ( the carrier of S -indexing f) . (the_result_sort_of o1) = ( the carrier of S -indexing f) . (the_result_sort_of o2) ) )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for f, g being Function holds
( f,g form_a_replacement_in S iff for o1, o2 being OperSymbol of S st ( the carrier' of S -indexing g) . o1 = ( the carrier' of S -indexing g) . o2 holds
( ( the carrier of S -indexing f) * (the_arity_of o1) = ( the carrier of S -indexing f) * (the_arity_of o2) & ( the carrier of S -indexing f) . (the_result_sort_of o1) = ( the carrier of S -indexing f) . (the_result_sort_of o2) ) )
let f, g be Function; ::_thesis: ( f,g form_a_replacement_in S iff for o1, o2 being OperSymbol of S st ( the carrier' of S -indexing g) . o1 = ( the carrier' of S -indexing g) . o2 holds
( ( the carrier of S -indexing f) * (the_arity_of o1) = ( the carrier of S -indexing f) * (the_arity_of o2) & ( the carrier of S -indexing f) . (the_result_sort_of o1) = ( the carrier of S -indexing f) . (the_result_sort_of o2) ) )
hereby  ::_thesis: ( ( for o1, o2 being OperSymbol of S st ( the carrier' of S -indexing g) . o1 = ( the carrier' of S -indexing g) . o2 holds
( ( the carrier of S -indexing f) * (the_arity_of o1) = ( the carrier of S -indexing f) * (the_arity_of o2) & ( the carrier of S -indexing f) . (the_result_sort_of o1) = ( the carrier of S -indexing f) . (the_result_sort_of o2) ) ) implies f,g form_a_replacement_in S )
assume A1: f,g form_a_replacement_in S ; ::_thesis: for o1, o2 being OperSymbol of S st ( the carrier' of S -indexing g) . o1 = ( the carrier' of S -indexing g) . o2 holds
( ( the carrier of S -indexing f) * (the_arity_of o1) = ( the carrier of S -indexing f) * (the_arity_of o2) & ( the carrier of S -indexing f) . (the_result_sort_of o1) = ( the carrier of S -indexing f) . (the_result_sort_of o2) )
let o1, o2 be OperSymbol of S; ::_thesis: ( ( the carrier' of S -indexing g) . o1 = ( the carrier' of S -indexing g) . o2 implies ( ( the carrier of S -indexing f) * (the_arity_of o1) = ( the carrier of S -indexing f) * (the_arity_of o2) & ( the carrier of S -indexing f) . (the_result_sort_of o1) = ( the carrier of S -indexing f) . (the_result_sort_of o2) ) )
A2: rng (the_arity_of o1) c= the carrier of S ;
A3: rng (the_arity_of o2) c= the carrier of S ;
assume  ( the carrier' of S -indexing g) . o1 = ( the carrier' of S -indexing g) . o2 ; ::_thesis: ( ( the carrier of S -indexing f) * (the_arity_of o1) = ( the carrier of S -indexing f) * (the_arity_of o2) & ( the carrier of S -indexing f) . (the_result_sort_of o1) = ( the carrier of S -indexing f) . (the_result_sort_of o2) )
then A4: ((id the carrier' of S) +* g) . o1 = ( the carrier' of S -indexing g) . o2 by Th8
.= ((id the carrier' of S) +* g) . o2 by Th8 ;
then  ((id the carrier of S) +* f) * (the_arity_of o1) = ((id the carrier of S) +* f) * (the_arity_of o2) by A1, Def3;
hence ( the carrier of S -indexing f) * (the_arity_of o1) = ((id the carrier of S) +* f) * (the_arity_of o2) by A2, Th21
.= ( the carrier of S -indexing f) * (the_arity_of o2) by A3, Th21 ;
::_thesis: ( the carrier of S -indexing f) . (the_result_sort_of o1) = ( the carrier of S -indexing f) . (the_result_sort_of o2)
thus ( the carrier of S -indexing f) . (the_result_sort_of o1) = ((id the carrier of S) +* f) . (the_result_sort_of o1) by Th8
.= ((id the carrier of S) +* f) . (the_result_sort_of o2) by A1, A4, Def3
.= ( the carrier of S -indexing f) . (the_result_sort_of o2) by Th8 ; ::_thesis: verum
end;
assume A5: for o1, o2 being OperSymbol of S st ( the carrier' of S -indexing g) . o1 = ( the carrier' of S -indexing g) . o2 holds
( ( the carrier of S -indexing f) * (the_arity_of o1) = ( the carrier of S -indexing f) * (the_arity_of o2) & ( the carrier of S -indexing f) . (the_result_sort_of o1) = ( the carrier of S -indexing f) . (the_result_sort_of o2) ) ; ::_thesis: f,g form_a_replacement_in S
let o1, o2 be OperSymbol of S; :: according to ALGSPEC1:def_3 ::_thesis: ( ((id the carrier' of S) +* g) . o1 = ((id the carrier' of S) +* g) . o2 implies ( ((id the carrier of S) +* f) * (the_arity_of o1) = ((id the carrier of S) +* f) * (the_arity_of o2) & ((id the carrier of S) +* f) . (the_result_sort_of o1) = ((id the carrier of S) +* f) . (the_result_sort_of o2) ) )
A6: rng (the_arity_of o1) c= the carrier of S ;
A7: rng (the_arity_of o2) c= the carrier of S ;
assume  ((id the carrier' of S) +* g) . o1 = ((id the carrier' of S) +* g) . o2 ; ::_thesis: ( ((id the carrier of S) +* f) * (the_arity_of o1) = ((id the carrier of S) +* f) * (the_arity_of o2) & ((id the carrier of S) +* f) . (the_result_sort_of o1) = ((id the carrier of S) +* f) . (the_result_sort_of o2) )
then A8: ( the carrier' of S -indexing g) . o1 = ((id the carrier' of S) +* g) . o2 by Th8
.= ( the carrier' of S -indexing g) . o2 by Th8 ;
then  ( the carrier of S -indexing f) * (the_arity_of o1) = ( the carrier of S -indexing f) * (the_arity_of o2) by A5;
hence ((id the carrier of S) +* f) * (the_arity_of o1) = ( the carrier of S -indexing f) * (the_arity_of o2) by A6, Th21
.= ((id the carrier of S) +* f) * (the_arity_of o2) by A7, Th21 ;
::_thesis: ((id the carrier of S) +* f) . (the_result_sort_of o1) = ((id the carrier of S) +* f) . (the_result_sort_of o2)
thus ((id the carrier of S) +* f) . (the_result_sort_of o1) = ( the carrier of S -indexing f) . (the_result_sort_of o1) by Th8
.= ( the carrier of S -indexing f) . (the_result_sort_of o2) by A5, A8
.= ((id the carrier of S) +* f) . (the_result_sort_of o2) by Th8 ; ::_thesis: verum
end;

theorem Th30: :: ALGSPEC1:30
for S being non empty non void ManySortedSign
for f, g being Function holds
( f,g form_a_replacement_in S iff the carrier of S -indexing f, the carrier' of S -indexing g form_a_replacement_in S )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for f, g being Function holds
( f,g form_a_replacement_in S iff the carrier of S -indexing f, the carrier' of S -indexing g form_a_replacement_in S )
let f, g be Function; ::_thesis: ( f,g form_a_replacement_in S iff the carrier of S -indexing f, the carrier' of S -indexing g form_a_replacement_in S )
 (id the carrier' of S) +* (id the carrier' of S) = id the carrier' of S ;
then A1: (id the carrier' of S) +* ((id the carrier' of S) +* (g | the carrier' of S)) = (id the carrier' of S) +* (g | the carrier' of S) by FUNCT_4:14;
 (id the carrier of S) +* (id the carrier of S) = id the carrier of S ;
then A2: (id the carrier of S) +* ((id the carrier of S) +* (f | the carrier of S)) = (id the carrier of S) +* (f | the carrier of S) by FUNCT_4:14;
 ( f,g form_a_replacement_in S iff for o1, o2 being OperSymbol of S st ( the carrier' of S -indexing g) . o1 = ( the carrier' of S -indexing g) . o2 holds
( ( the carrier of S -indexing f) * (the_arity_of o1) = ( the carrier of S -indexing f) * (the_arity_of o2) & ( the carrier of S -indexing f) . (the_result_sort_of o1) = ( the carrier of S -indexing f) . (the_result_sort_of o2) ) ) by Th29;
hence  ( f,g form_a_replacement_in S iff the carrier of S -indexing f, the carrier' of S -indexing g form_a_replacement_in S ) by A1, A2, Def3; ::_thesis: verum
end;


theorem Th31: :: ALGSPEC1:31
for S, S9 being non void Signature
for f, g being Function st f,g form_morphism_between S,S9 holds
f,g form_a_replacement_in S
proof
let S, S9 be non void Signature; ::_thesis: for f, g being Function st f,g form_morphism_between S,S9 holds
f,g form_a_replacement_in S
let f, g be Function; ::_thesis: ( f,g form_morphism_between S,S9 implies f,g form_a_replacement_in S )
A1: dom (id the carrier of S) = the carrier of S ;
A2: dom (id the carrier' of S) = the carrier' of S ;
assume A3: f,g form_morphism_between S,S9 ; ::_thesis: f,g form_a_replacement_in S
then  dom g = the carrier' of S by PUA2MSS1:def_12;
then A4: (id the carrier' of S) +* g = g by A2, FUNCT_4:19;
let o1, o2 be OperSymbol of S; :: according to ALGSPEC1:def_3 ::_thesis: ( ((id the carrier' of S) +* g) . o1 = ((id the carrier' of S) +* g) . o2 implies ( ((id the carrier of S) +* f) * (the_arity_of o1) = ((id the carrier of S) +* f) * (the_arity_of o2) & ((id the carrier of S) +* f) . (the_result_sort_of o1) = ((id the carrier of S) +* f) . (the_result_sort_of o2) ) )
assume A5: ((id the carrier' of S) +* g) . o1 = ((id the carrier' of S) +* g) . o2 ; ::_thesis: ( ((id the carrier of S) +* f) * (the_arity_of o1) = ((id the carrier of S) +* f) * (the_arity_of o2) & ((id the carrier of S) +* f) . (the_result_sort_of o1) = ((id the carrier of S) +* f) . (the_result_sort_of o2) )
 dom f = the carrier of S by A3, PUA2MSS1:def_12;
then A6: (id the carrier of S) +* f = f by A1, FUNCT_4:19;
hence ((id the carrier of S) +* f) * (the_arity_of o1) = the Arity of S9 . (g . o1) by A3, PUA2MSS1:def_12
.= ((id the carrier of S) +* f) * (the_arity_of o2) by A3, A6, A4, A5, PUA2MSS1:def_12 ;
::_thesis: ((id the carrier of S) +* f) . (the_result_sort_of o1) = ((id the carrier of S) +* f) . (the_result_sort_of o2)
reconsider g9 = g as Function of the carrier' of S, the carrier' of S9 by A3, INSTALG1:9;
thus ((id the carrier of S) +* f) . (the_result_sort_of o1) = (f * the ResultSort of S) . o1 by A6, FUNCT_2:15
.= ( the ResultSort of S9 * g) . o1 by A3, PUA2MSS1:def_12
.= the ResultSort of S9 . (g9 . o1) by FUNCT_2:15
.= ( the ResultSort of S9 * g9) . o2 by A4, A5, FUNCT_2:15
.= (f * the ResultSort of S) . o2 by A3, PUA2MSS1:def_12
.= ((id the carrier of S) +* f) . (the_result_sort_of o2) by A6, FUNCT_2:15 ; ::_thesis: verum
end;

theorem :: ALGSPEC1:32
for S being non void Signature
for f being Function holds f, {} form_a_replacement_in S
proof
let S be non void Signature; ::_thesis: for f being Function holds f, {} form_a_replacement_in S
let f be Function; ::_thesis: f, {} form_a_replacement_in S
let o1, o2 be OperSymbol of S; :: according to ALGSPEC1:def_3 ::_thesis: ( ((id the carrier' of S) +* {}) . o1 = ((id the carrier' of S) +* {}) . o2 implies ( ((id the carrier of S) +* f) * (the_arity_of o1) = ((id the carrier of S) +* f) * (the_arity_of o2) & ((id the carrier of S) +* f) . (the_result_sort_of o1) = ((id the carrier of S) +* f) . (the_result_sort_of o2) ) )
assume  ((id the carrier' of S) +* {}) . o1 = ((id the carrier' of S) +* {}) . o2 ; ::_thesis: ( ((id the carrier of S) +* f) * (the_arity_of o1) = ((id the carrier of S) +* f) * (the_arity_of o2) & ((id the carrier of S) +* f) . (the_result_sort_of o1) = ((id the carrier of S) +* f) . (the_result_sort_of o2) )
then o1 = (id the carrier' of S) . o2 by FUNCT_1:17
.= o2 by FUNCT_1:17 ;
hence  ( ((id the carrier of S) +* f) * (the_arity_of o1) = ((id the carrier of S) +* f) * (the_arity_of o2) & ((id the carrier of S) +* f) . (the_result_sort_of o1) = ((id the carrier of S) +* f) . (the_result_sort_of o2) ) ; ::_thesis: verum
end;

theorem Th33: :: ALGSPEC1:33
for S being non void Signature
for g, f being Function st g is one-to-one & the carrier' of S /\ (rng g) c= dom g holds
f,g form_a_replacement_in S
proof
let S be non void Signature; ::_thesis: for g, f being Function st g is one-to-one & the carrier' of S /\ (rng g) c= dom g holds
f,g form_a_replacement_in S
let g, f be Function; ::_thesis: ( g is one-to-one & the carrier' of S /\ (rng g) c= dom g implies f,g form_a_replacement_in S )
assume that
A1: g is one-to-one and
A2: the carrier' of S /\ (rng g) c= dom g ; ::_thesis: f,g form_a_replacement_in S
let o1, o2 be OperSymbol of S; :: according to ALGSPEC1:def_3 ::_thesis: ( ((id the carrier' of S) +* g) . o1 = ((id the carrier' of S) +* g) . o2 implies ( ((id the carrier of S) +* f) * (the_arity_of o1) = ((id the carrier of S) +* f) * (the_arity_of o2) & ((id the carrier of S) +* f) . (the_result_sort_of o1) = ((id the carrier of S) +* f) . (the_result_sort_of o2) ) )
assume A3: ((id the carrier' of S) +* g) . o1 = ((id the carrier' of S) +* g) . o2 ; ::_thesis: ( ((id the carrier of S) +* f) * (the_arity_of o1) = ((id the carrier of S) +* f) * (the_arity_of o2) & ((id the carrier of S) +* f) . (the_result_sort_of o1) = ((id the carrier of S) +* f) . (the_result_sort_of o2) )
A4: (id the carrier' of S) . o1 = o1 by FUNCT_1:18;
A5: (id the carrier' of S) . o2 = o2 by FUNCT_1:18;
percases ( o1 in dom g or not o1 in dom g ) ;
supposeA6: o1 in dom g ; ::_thesis: ( ((id the carrier of S) +* f) * (the_arity_of o1) = ((id the carrier of S) +* f) * (the_arity_of o2) & ((id the carrier of S) +* f) . (the_result_sort_of o1) = ((id the carrier of S) +* f) . (the_result_sort_of o2) )
then A7: g . o1 in rng g by FUNCT_1:def_3;
A8: ((id the carrier' of S) +* g) . o1 = g . o1 by A6, FUNCT_4:13;
then  ( not o2 in dom g implies g . o1 = o2 ) by A3, A5, FUNCT_4:11;
then A9: ( not o2 in dom g implies o2 in the carrier' of S /\ (rng g) ) by A7, XBOOLE_0:def_4;
then  ((id the carrier' of S) +* g) . o2 = g . o2 by A2, FUNCT_4:13;
hence  ( ((id the carrier of S) +* f) * (the_arity_of o1) = ((id the carrier of S) +* f) * (the_arity_of o2) & ((id the carrier of S) +* f) . (the_result_sort_of o1) = ((id the carrier of S) +* f) . (the_result_sort_of o2) ) by A1, A2, A3, A6, A8, A9, FUNCT_1:def_4; ::_thesis: verum
end;
supposeA10: not o1 in dom g ; ::_thesis: ( ((id the carrier of S) +* f) * (the_arity_of o1) = ((id the carrier of S) +* f) * (the_arity_of o2) & ((id the carrier of S) +* f) . (the_result_sort_of o1) = ((id the carrier of S) +* f) . (the_result_sort_of o2) )
then A11: not o1 in the carrier' of S /\ (rng g) by A2;
A12: ((id the carrier' of S) +* g) . o1 = o1 by A4, A10, FUNCT_4:11;
then  ( o2 in dom g implies ( o1 = g . o2 & g . o2 in rng g ) ) by A3, FUNCT_1:def_3, FUNCT_4:13;
hence  ( ((id the carrier of S) +* f) * (the_arity_of o1) = ((id the carrier of S) +* f) * (the_arity_of o2) & ((id the carrier of S) +* f) . (the_result_sort_of o1) = ((id the carrier of S) +* f) . (the_result_sort_of o2) ) by A3, A5, A12, A11, FUNCT_4:11, XBOOLE_0:def_4; ::_thesis: verum
end;
end;
end;

theorem :: ALGSPEC1:34
for S being non void Signature
for g, f being Function st g is one-to-one & rng g misses the carrier' of S holds
f,g form_a_replacement_in S
proof
let S be non void Signature; ::_thesis: for g, f being Function st g is one-to-one & rng g misses the carrier' of S holds
f,g form_a_replacement_in S
let g, f be Function; ::_thesis: ( g is one-to-one & rng g misses the carrier' of S implies f,g form_a_replacement_in S )
assume A1: g is one-to-one ; ::_thesis: ( not rng g misses the carrier' of S or f,g form_a_replacement_in S )
assume  rng g misses the carrier' of S ; ::_thesis: f,g form_a_replacement_in S
then  the carrier' of S /\ (rng g) = {} by XBOOLE_0:def_7;
then  the carrier' of S /\ (rng g) c= dom g by XBOOLE_1:2;
hence  f,g form_a_replacement_in S by A1, Th33; ::_thesis: verum
end;

registration
let X be set ;
let Y be non empty set ;
let a be Function of Y,(X *);
let r be Function of Y,X;
cluster ManySortedSign(# X,Y,a,r #) ->  non void ;
coherence
 not ManySortedSign(# X,Y,a,r #) is void ;
end;

definition
let S be non empty non void ManySortedSign ;
let f, g be Function;
assume X1: f,g form_a_replacement_in S ;
funcS with-replacement (f,g) ->  non empty non void strict ManySortedSign  means :Def4: :: ALGSPEC1:def 4
( the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,it & the carrier of it = rng ( the carrier of S -indexing f) & the carrier' of it = rng ( the carrier' of S -indexing g) );
uniqueness
 for b1, b2 being non empty non void strict ManySortedSign st the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,b1 & the carrier of b1 = rng ( the carrier of S -indexing f) & the carrier' of b1 = rng ( the carrier' of S -indexing g) & the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,b2 & the carrier of b2 = rng ( the carrier of S -indexing f) & the carrier' of b2 = rng ( the carrier' of S -indexing g) holds
b1 = b2
proof
set g1 = the carrier' of S -indexing g;
set g2 = the carrier' of S -indexing g;
set f1 = the carrier of S -indexing f;
set f2 = the carrier of S -indexing f;
let S1, S2 be non empty non void strict ManySortedSign ; ::_thesis: ( the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,S1 & the carrier of S1 = rng ( the carrier of S -indexing f) & the carrier' of S1 = rng ( the carrier' of S -indexing g) & the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,S2 & the carrier of S2 = rng ( the carrier of S -indexing f) & the carrier' of S2 = rng ( the carrier' of S -indexing g) implies S1 = S2 )
assume that
A1: the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,S1 and
A2: the carrier of S1 = rng ( the carrier of S -indexing f) and
A3: the carrier' of S1 = rng ( the carrier' of S -indexing g) and
A4: the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,S2 and
A5: the carrier of S2 = rng ( the carrier of S -indexing f) and
A6: the carrier' of S2 = rng ( the carrier' of S -indexing g) ; ::_thesis: S1 = S2
A7: the ResultSort of S1 = the ResultSort of S2
proof
thus  the carrier' of S1 = the carrier' of S2 by A3, A6; :: according to FUNCT_2:def_7 ::_thesis: for b1 being Element of the carrier' of S1 holds the ResultSort of S1 . b1 = the ResultSort of S2 . b1
let o be OperSymbol of S1; ::_thesis: the ResultSort of S1 . o = the ResultSort of S2 . o
consider o1 being set  such that
A8: o1 in dom ( the carrier' of S -indexing g) and
A9: o = ( the carrier' of S -indexing g) . o1 by A3, FUNCT_1:def_3;
consider o2 being set  such that
A10: o2 in dom ( the carrier' of S -indexing g) and
A11: o = ( the carrier' of S -indexing g) . o2 by A3, FUNCT_1:def_3;
reconsider o1 = o1, o2 = o2 as OperSymbol of S by A8, A10;
thus  the ResultSort of S1 . o = ( the ResultSort of S1 * ( the carrier' of S -indexing g)) . o1 by A8, A9, FUNCT_1:13
.= (( the carrier of S -indexing f) * the ResultSort of S) . o1 by A1, PUA2MSS1:def_12
.= ( the carrier of S -indexing f) . (the_result_sort_of o1) by FUNCT_2:15
.= ( the carrier of S -indexing f) . (the_result_sort_of o2) by X1, A9, A11, Th29
.= (( the carrier of S -indexing f) * the ResultSort of S) . o2 by FUNCT_2:15
.= ( the ResultSort of S2 * ( the carrier' of S -indexing g)) . o2 by A4, PUA2MSS1:def_12
.= the ResultSort of S2 . o by A10, A11, FUNCT_1:13 ; ::_thesis: verum
end;
 the Arity of S1 = the Arity of S2
proof
thus  the carrier' of S1 = the carrier' of S2 by A3, A6; :: according to FUNCT_2:def_7 ::_thesis: for b1 being Element of the carrier' of S1 holds the Arity of S1 . b1 = the Arity of S2 . b1
let o be OperSymbol of S1; ::_thesis: the Arity of S1 . o = the Arity of S2 . o
consider o2 being set  such that
A12: o2 in dom ( the carrier' of S -indexing g) and
A13: o = ( the carrier' of S -indexing g) . o2 by A3, FUNCT_1:def_3;
reconsider o2 = o2 as OperSymbol of S by A12;
thus  the Arity of S1 . o = ( the carrier of S -indexing f) * (the_arity_of o2) by A1, A13, PUA2MSS1:def_12
.= the Arity of S2 . o by A4, A13, PUA2MSS1:def_12 ; ::_thesis: verum
end;
hence  S1 = S2 by A2, A3, A5, A6, A7; ::_thesis: verum
end;
existence
 ex b1 being non empty non void strict ManySortedSign st
( the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,b1 & the carrier of b1 = rng ( the carrier of S -indexing f) & the carrier' of b1 = rng ( the carrier' of S -indexing g) )
proof
set g9 = the carrier' of S -indexing g;
set gg = the carrier' of S -indexing g;
set f9 = the carrier of S -indexing f;
set ff = the carrier of S -indexing f;
A14: dom ( the carrier' of S -indexing g) = the carrier' of S by PARTFUN1:def_2;
reconsider X = rng ( the carrier of S -indexing f), Y = rng ( the carrier' of S -indexing g) as non empty set ;
reconsider g9 = the carrier' of S -indexing g as Function of the carrier' of S,Y by A14, FUNCT_2:1;
set G = the rng-retract of g9;
A15: rng the rng-retract of g9 c= the carrier' of S by A14, Th23;
 dom the rng-retract of g9 = rng g9 by Def2;
then reconsider G = the rng-retract of g9 as Function of Y, the carrier' of S by A15, FUNCT_2:def_1, RELSET_1:4;
 dom ( the carrier of S -indexing f) = the carrier of S by PARTFUN1:def_2;
then reconsider f9 = the carrier of S -indexing f as Function of the carrier of S,X by FUNCT_2:1;
set r = (f9 * the ResultSort of S) * G;
take R = ManySortedSign(# X,Y,(((f9 *) * the Arity of S) * G),((f9 * the ResultSort of S) * G) #); ::_thesis: ( the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,R & the carrier of R = rng ( the carrier of S -indexing f) & the carrier' of R = rng ( the carrier' of S -indexing g) )
thus  the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,R ::_thesis: ( the carrier of R = rng ( the carrier of S -indexing f) & the carrier' of R = rng ( the carrier' of S -indexing g) )
proof
thus  ( dom ( the carrier of S -indexing f) = the carrier of S & dom ( the carrier' of S -indexing g) = the carrier' of S ) by PARTFUN1:def_2; :: according to PUA2MSS1:def_12 ::_thesis: ( rng ( the carrier of S -indexing f) c= the carrier of R & rng ( the carrier' of S -indexing g) c= the carrier' of R & the ResultSort of S * ( the carrier of S -indexing f) = ( the carrier' of S -indexing g) * the ResultSort of R & ( for b1 being set
for b2 being set holds
( not b1 in the carrier' of S or not b2 = the Arity of S . b1 or b2 * ( the carrier of S -indexing f) = the Arity of R . (( the carrier' of S -indexing g) . b1) ) ) )
thus  ( rng ( the carrier of S -indexing f) c= the carrier of R & rng ( the carrier' of S -indexing g) c= the carrier' of R ) ; ::_thesis: ( the ResultSort of S * ( the carrier of S -indexing f) = ( the carrier' of S -indexing g) * the ResultSort of R & ( for b1 being set
for b2 being set holds
( not b1 in the carrier' of S or not b2 = the Arity of S . b1 or b2 * ( the carrier of S -indexing f) = the Arity of R . (( the carrier' of S -indexing g) . b1) ) ) )
now__::_thesis:_for_x_being_OperSymbol_of_S_holds_(((f9_*_the_ResultSort_of_S)_*_G)_*_g9)_._x_=_(f9_*_the_ResultSort_of_S)_._x
let x be OperSymbol of S; ::_thesis: (((f9 * the ResultSort of S) * G) * g9) . x = (f9 * the ResultSort of S) . x
A16: g9 . (G . (g9 . x)) = g9 . x by Th24;
thus (((f9 * the ResultSort of S) * G) * g9) . x = the ResultSort of R . (g9 . x) by FUNCT_2:15
.= (f9 * the ResultSort of S) . (G . (g9 . x)) by FUNCT_2:15
.= f9 . (the_result_sort_of (G . (g9 . x))) by FUNCT_2:15
.= f9 . (the_result_sort_of x) by X1, A16, Th29
.= (f9 * the ResultSort of S) . x by FUNCT_2:15 ; ::_thesis: verum
end;
hence  ( the carrier of S -indexing f) * the ResultSort of S = the ResultSort of R * ( the carrier' of S -indexing g) by FUNCT_2:63; ::_thesis: for b1 being set
for b2 being set holds
( not b1 in the carrier' of S or not b2 = the Arity of S . b1 or b2 * ( the carrier of S -indexing f) = the Arity of R . (( the carrier' of S -indexing g) . b1) )
let o be set ; ::_thesis: for b1 being set holds
( not o in the carrier' of S or not b1 = the Arity of S . o or b1 * ( the carrier of S -indexing f) = the Arity of R . (( the carrier' of S -indexing g) . o) )
let p be Function; ::_thesis: ( not o in the carrier' of S or not p = the Arity of S . o or p * ( the carrier of S -indexing f) = the Arity of R . (( the carrier' of S -indexing g) . o) )
assume that
A17: o in the carrier' of S and
A18: p = the Arity of S . o ; ::_thesis: p * ( the carrier of S -indexing f) = the Arity of R . (( the carrier' of S -indexing g) . o)
reconsider x = o as OperSymbol of S by A17;
 g9 . (G . (g9 . x)) = g9 . x by Th24;
then  f9 * (the_arity_of x) = f9 * (the_arity_of (G . (g9 . x))) by X1, Th29;
hence ( the carrier of S -indexing f) * p = (f9 *) . (the_arity_of (G . (g9 . x))) by A18, LANG1:def_13
.= ((f9 *) * the Arity of S) . (G . (g9 . x)) by FUNCT_2:15
.= the Arity of R . (( the carrier' of S -indexing g) . o) by FUNCT_2:15 ;
::_thesis: verum
end;
thus  ( the carrier of R = rng ( the carrier of S -indexing f) & the carrier' of R = rng ( the carrier' of S -indexing g) ) ; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines with-replacement ALGSPEC1:def_4_:_
 for S being non empty non void ManySortedSign
for f, g being Function st f,g form_a_replacement_in S holds
for b4 being non empty non void strict ManySortedSign holds
( b4 = S with-replacement (f,g) iff ( the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,b4 & the carrier of b4 = rng ( the carrier of S -indexing f) & the carrier' of b4 = rng ( the carrier' of S -indexing g) ) );

theorem Th35: :: ALGSPEC1:35
for S1, S2 being non void Signature
for f being Function of the carrier of S1, the carrier of S2
for g being Function st f,g form_morphism_between S1,S2 holds
(f *) * the Arity of S1 = the Arity of S2 * g
proof
let S1, S2 be non void Signature; ::_thesis: for f being Function of the carrier of S1, the carrier of S2
for g being Function st f,g form_morphism_between S1,S2 holds
(f *) * the Arity of S1 = the Arity of S2 * g
let f be Function of the carrier of S1, the carrier of S2; ::_thesis: for g being Function st f,g form_morphism_between S1,S2 holds
(f *) * the Arity of S1 = the Arity of S2 * g
let g be Function; ::_thesis: ( f,g form_morphism_between S1,S2 implies (f *) * the Arity of S1 = the Arity of S2 * g )
A1: dom the Arity of S2 = the carrier' of S2 by FUNCT_2:def_1;
A2: dom ((f *) * the Arity of S1) = the carrier' of S1 by FUNCT_2:def_1;
assume A3: f,g form_morphism_between S1,S2 ; ::_thesis: (f *) * the Arity of S1 = the Arity of S2 * g
then A4: dom g = the carrier' of S1 by PUA2MSS1:def_12;
A5: dom the Arity of S1 = the carrier' of S1 by FUNCT_2:def_1;
A6: now__::_thesis:_for_c_being_set_st_c_in_the_carrier'_of_S1_holds_
((f_*)_*_the_Arity_of_S1)_._c_=_(_the_Arity_of_S2_*_g)_._c
let c be set ; ::_thesis: ( c in the carrier' of S1 implies ((f *) * the Arity of S1) . c = ( the Arity of S2 * g) . c )
assume A7: c in the carrier' of S1 ; ::_thesis: ((f *) * the Arity of S1) . c = ( the Arity of S2 * g) . c
then A8: the Arity of S1 . c in rng the Arity of S1 by A5, FUNCT_1:def_3;
then reconsider p = the Arity of S1 . c as FinSequence of the carrier of S1 by FINSEQ_1:def_11;
thus ((f *) * the Arity of S1) . c = (f *) . p by A5, A7, FUNCT_1:13
.= f * p by A8, LANG1:def_13
.= the Arity of S2 . (g . c) by A3, A7, PUA2MSS1:def_12
.= ( the Arity of S2 * g) . c by A4, A7, FUNCT_1:13 ; ::_thesis: verum
end;
 rng g c= the carrier' of S2 by A3, PUA2MSS1:def_12;
then  dom ( the Arity of S2 * g) = the carrier' of S1 by A4, A1, RELAT_1:27;
hence  (f *) * the Arity of S1 = the Arity of S2 * g by A2, A6, FUNCT_1:2; ::_thesis: verum
end;

theorem Th36: :: ALGSPEC1:36
for S being non void Signature
for f, g being Function st f,g form_a_replacement_in S holds
the carrier of S -indexing f is Function of the carrier of S, the carrier of (S with-replacement (f,g))
proof
let S be non void Signature; ::_thesis: for f, g being Function st f,g form_a_replacement_in S holds
the carrier of S -indexing f is Function of the carrier of S, the carrier of (S with-replacement (f,g))
let f, g be Function; ::_thesis: ( f,g form_a_replacement_in S implies the carrier of S -indexing f is Function of the carrier of S, the carrier of (S with-replacement (f,g)) )
assume  f,g form_a_replacement_in S ; ::_thesis: the carrier of S -indexing f is Function of the carrier of S, the carrier of (S with-replacement (f,g))
then  the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,S with-replacement (f,g) by Def4;
hence  the carrier of S -indexing f is Function of the carrier of S, the carrier of (S with-replacement (f,g)) by INSTALG1:9; ::_thesis: verum
end;

theorem Th37: :: ALGSPEC1:37
for S being non void Signature
for f, g being Function st f,g form_a_replacement_in S holds
for f9 being Function of the carrier of S, the carrier of (S with-replacement (f,g)) st f9 = the carrier of S -indexing f holds
for g9 being rng-retract of the carrier' of S -indexing g holds the Arity of (S with-replacement (f,g)) = ((f9 *) * the Arity of S) * g9
proof
let S be non void Signature; ::_thesis: for f, g being Function st f,g form_a_replacement_in S holds
for f9 being Function of the carrier of S, the carrier of (S with-replacement (f,g)) st f9 = the carrier of S -indexing f holds
for g9 being rng-retract of the carrier' of S -indexing g holds the Arity of (S with-replacement (f,g)) = ((f9 *) * the Arity of S) * g9
let f, g be Function; ::_thesis: ( f,g form_a_replacement_in S implies for f9 being Function of the carrier of S, the carrier of (S with-replacement (f,g)) st f9 = the carrier of S -indexing f holds
for g9 being rng-retract of the carrier' of S -indexing g holds the Arity of (S with-replacement (f,g)) = ((f9 *) * the Arity of S) * g9 )
set ff = the carrier of S -indexing f;
set gg = the carrier' of S -indexing g;
set T = S with-replacement (f,g);
assume A1: f,g form_a_replacement_in S ; ::_thesis: for f9 being Function of the carrier of S, the carrier of (S with-replacement (f,g)) st f9 = the carrier of S -indexing f holds
for g9 being rng-retract of the carrier' of S -indexing g holds the Arity of (S with-replacement (f,g)) = ((f9 *) * the Arity of S) * g9
then A2: the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,S with-replacement (f,g) by Def4;
let f9 be Function of the carrier of S, the carrier of (S with-replacement (f,g)); ::_thesis: ( f9 = the carrier of S -indexing f implies for g9 being rng-retract of the carrier' of S -indexing g holds the Arity of (S with-replacement (f,g)) = ((f9 *) * the Arity of S) * g9 )
assume A3: f9 = the carrier of S -indexing f ; ::_thesis: for g9 being rng-retract of the carrier' of S -indexing g holds the Arity of (S with-replacement (f,g)) = ((f9 *) * the Arity of S) * g9
let g9 be rng-retract of the carrier' of S -indexing g; ::_thesis: the Arity of (S with-replacement (f,g)) = ((f9 *) * the Arity of S) * g9
 the carrier' of (S with-replacement (f,g)) = rng ( the carrier' of S -indexing g) by A1, Def4;
hence  the Arity of (S with-replacement (f,g)) = the Arity of (S with-replacement (f,g)) * (id (rng ( the carrier' of S -indexing g))) by FUNCT_2:17
.= the Arity of (S with-replacement (f,g)) * (( the carrier' of S -indexing g) * g9) by Def2
.= ( the Arity of (S with-replacement (f,g)) * ( the carrier' of S -indexing g)) * g9 by RELAT_1:36
.= ((f9 *) * the Arity of S) * g9 by A2, A3, Th35 ;
::_thesis: verum
end;

theorem Th38: :: ALGSPEC1:38
for S being non void Signature
for f, g being Function st f,g form_a_replacement_in S holds
for g9 being rng-retract of the carrier' of S -indexing g holds the ResultSort of (S with-replacement (f,g)) = (( the carrier of S -indexing f) * the ResultSort of S) * g9
proof
let S be non void Signature; ::_thesis: for f, g being Function st f,g form_a_replacement_in S holds
for g9 being rng-retract of the carrier' of S -indexing g holds the ResultSort of (S with-replacement (f,g)) = (( the carrier of S -indexing f) * the ResultSort of S) * g9
let f, g be Function; ::_thesis: ( f,g form_a_replacement_in S implies for g9 being rng-retract of the carrier' of S -indexing g holds the ResultSort of (S with-replacement (f,g)) = (( the carrier of S -indexing f) * the ResultSort of S) * g9 )
set ff = the carrier of S -indexing f;
set gg = the carrier' of S -indexing g;
set T = S with-replacement (f,g);
assume A1: f,g form_a_replacement_in S ; ::_thesis: for g9 being rng-retract of the carrier' of S -indexing g holds the ResultSort of (S with-replacement (f,g)) = (( the carrier of S -indexing f) * the ResultSort of S) * g9
then A2: the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,S with-replacement (f,g) by Def4;
let g9 be rng-retract of the carrier' of S -indexing g; ::_thesis: the ResultSort of (S with-replacement (f,g)) = (( the carrier of S -indexing f) * the ResultSort of S) * g9
 the carrier' of (S with-replacement (f,g)) = rng ( the carrier' of S -indexing g) by A1, Def4;
hence  the ResultSort of (S with-replacement (f,g)) = the ResultSort of (S with-replacement (f,g)) * (id (rng ( the carrier' of S -indexing g))) by FUNCT_2:17
.= the ResultSort of (S with-replacement (f,g)) * (( the carrier' of S -indexing g) * g9) by Def2
.= ( the ResultSort of (S with-replacement (f,g)) * ( the carrier' of S -indexing g)) * g9 by RELAT_1:36
.= (( the carrier of S -indexing f) * the ResultSort of S) * g9 by A2, PUA2MSS1:def_12 ;
::_thesis: verum
end;

theorem Th39: :: ALGSPEC1:39
for S, S9 being non void Signature
for f, g being Function st f,g form_morphism_between S,S9 holds
S with-replacement (f,g) is Subsignature of S9
proof
let S, S9 be non void Signature; ::_thesis: for f, g being Function st f,g form_morphism_between S,S9 holds
S with-replacement (f,g) is Subsignature of S9
let f, g be Function; ::_thesis: ( f,g form_morphism_between S,S9 implies S with-replacement (f,g) is Subsignature of S9 )
set R = S with-replacement (f,g);
set F = id the carrier of (S with-replacement (f,g));
set G = id the carrier' of (S with-replacement (f,g));
set f9 = the carrier of S -indexing f;
set g9 = the carrier' of S -indexing g;
A1: dom the ResultSort of S9 = the carrier' of S9 by FUNCT_2:def_1;
A2: dom the ResultSort of (S with-replacement (f,g)) = the carrier' of (S with-replacement (f,g)) by FUNCT_2:def_1;
assume A3: f,g form_morphism_between S,S9 ; ::_thesis: S with-replacement (f,g) is Subsignature of S9
then  dom f = the carrier of S by PUA2MSS1:def_12;
then A4: the carrier of S -indexing f = f by Th10;
A5: f,g form_a_replacement_in S by A3, Th31;
then A6: the carrier' of (S with-replacement (f,g)) = rng ( the carrier' of S -indexing g) by Def4;
thus  ( dom (id the carrier of (S with-replacement (f,g))) = the carrier of (S with-replacement (f,g)) & dom (id the carrier' of (S with-replacement (f,g))) = the carrier' of (S with-replacement (f,g)) ) ; :: according to PUA2MSS1:def_12,INSTALG1:def_2 ::_thesis: ( rng (id the carrier of (S with-replacement (f,g))) c= the carrier of S9 & rng (id the carrier' of (S with-replacement (f,g))) c= the carrier' of S9 & the ResultSort of (S with-replacement (f,g)) * (id the carrier of (S with-replacement (f,g))) = (id the carrier' of (S with-replacement (f,g))) * the ResultSort of S9 & ( for b1 being set
for b2 being set holds
( not b1 in the carrier' of (S with-replacement (f,g)) or not b2 = the Arity of (S with-replacement (f,g)) . b1 or b2 * (id the carrier of (S with-replacement (f,g))) = the Arity of S9 . ((id the carrier' of (S with-replacement (f,g))) . b1) ) ) )
 dom g = the carrier' of S by A3, PUA2MSS1:def_12;
then A7: the carrier' of S -indexing g = g by Th10;
A8: the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,S with-replacement (f,g) by A5, Def4;
A9: now__::_thesis:_for_x_being_set_st_x_in_the_carrier'_of_(S_with-replacement_(f,g))_holds_
the_ResultSort_of_(S_with-replacement_(f,g))_._x_=_(_the_ResultSort_of_S9_|_the_carrier'_of_(S_with-replacement_(f,g)))_._x
let x be set ; ::_thesis: ( x in the carrier' of (S with-replacement (f,g)) implies the ResultSort of (S with-replacement (f,g)) . x = ( the ResultSort of S9 | the carrier' of (S with-replacement (f,g))) . x )
assume A10: x in the carrier' of (S with-replacement (f,g)) ; ::_thesis: the ResultSort of (S with-replacement (f,g)) . x = ( the ResultSort of S9 | the carrier' of (S with-replacement (f,g))) . x
then consider a being set  such that
A11: a in dom g and
A12: x = g . a by A6, A7, FUNCT_1:def_3;
reconsider a = a as OperSymbol of S by A3, A11, PUA2MSS1:def_12;
 the ResultSort of (S with-replacement (f,g)) * g = f * the ResultSort of S by A8, A4, A7, PUA2MSS1:def_12;
then A13: the ResultSort of (S with-replacement (f,g)) . x = (f * the ResultSort of S) . a by A11, A12, FUNCT_1:13;
 the ResultSort of S9 * g = f * the ResultSort of S by A3, PUA2MSS1:def_12;
then  the ResultSort of S9 . x = (f * the ResultSort of S) . a by A11, A12, FUNCT_1:13;
hence  the ResultSort of (S with-replacement (f,g)) . x = ( the ResultSort of S9 | the carrier' of (S with-replacement (f,g))) . x by A10, A13, FUNCT_1:49; ::_thesis: verum
end;
 rng g c= the carrier' of S9 by A3, PUA2MSS1:def_12;
then  dom ( the ResultSort of S9 | the carrier' of (S with-replacement (f,g))) = the carrier' of (S with-replacement (f,g)) by A6, A7, A1, RELAT_1:62;
then A14: the ResultSort of (S with-replacement (f,g)) = the ResultSort of S9 | the carrier' of (S with-replacement (f,g)) by A2, A9, FUNCT_1:2;
 the carrier of (S with-replacement (f,g)) = rng ( the carrier of S -indexing f) by A5, Def4;
hence  ( rng (id the carrier of (S with-replacement (f,g))) c= the carrier of S9 & rng (id the carrier' of (S with-replacement (f,g))) c= the carrier' of S9 ) by A3, A6, A4, A7, PUA2MSS1:def_12; ::_thesis: ( the ResultSort of (S with-replacement (f,g)) * (id the carrier of (S with-replacement (f,g))) = (id the carrier' of (S with-replacement (f,g))) * the ResultSort of S9 & ( for b1 being set
for b2 being set holds
( not b1 in the carrier' of (S with-replacement (f,g)) or not b2 = the Arity of (S with-replacement (f,g)) . b1 or b2 * (id the carrier of (S with-replacement (f,g))) = the Arity of S9 . ((id the carrier' of (S with-replacement (f,g))) . b1) ) ) )
 rng the ResultSort of (S with-replacement (f,g)) c= the carrier of (S with-replacement (f,g)) ;
hence (id the carrier of (S with-replacement (f,g))) * the ResultSort of (S with-replacement (f,g)) = the ResultSort of (S with-replacement (f,g)) by RELAT_1:53
.= the ResultSort of S9 * (id the carrier' of (S with-replacement (f,g))) by A14, RELAT_1:65 ;
::_thesis: for b1 being set
for b2 being set holds
( not b1 in the carrier' of (S with-replacement (f,g)) or not b2 = the Arity of (S with-replacement (f,g)) . b1 or b2 * (id the carrier of (S with-replacement (f,g))) = the Arity of S9 . ((id the carrier' of (S with-replacement (f,g))) . b1) )
let o be set ; ::_thesis: for b1 being set holds
( not o in the carrier' of (S with-replacement (f,g)) or not b1 = the Arity of (S with-replacement (f,g)) . o or b1 * (id the carrier of (S with-replacement (f,g))) = the Arity of S9 . ((id the carrier' of (S with-replacement (f,g))) . o) )
let p be Function; ::_thesis: ( not o in the carrier' of (S with-replacement (f,g)) or not p = the Arity of (S with-replacement (f,g)) . o or p * (id the carrier of (S with-replacement (f,g))) = the Arity of S9 . ((id the carrier' of (S with-replacement (f,g))) . o) )
assume that
A15: o in the carrier' of (S with-replacement (f,g)) and
A16: p = the Arity of (S with-replacement (f,g)) . o ; ::_thesis: p * (id the carrier of (S with-replacement (f,g))) = the Arity of S9 . ((id the carrier' of (S with-replacement (f,g))) . o)
consider a being set  such that
A17: a in dom g and
A18: o = g . a by A6, A7, A15, FUNCT_1:def_3;
reconsider a = a as OperSymbol of S by A3, A17, PUA2MSS1:def_12;
A19: f * (the_arity_of a) = the Arity of S9 . o by A3, A18, PUA2MSS1:def_12;
 p in the carrier of (S with-replacement (f,g)) * by A15, A16, FUNCT_2:5;
then  p is FinSequence of the carrier of (S with-replacement (f,g)) by FINSEQ_1:def_11;
then A20: rng p c= the carrier of (S with-replacement (f,g)) by FINSEQ_1:def_4;
 f * (the_arity_of a) = p by A8, A4, A7, A16, A18, PUA2MSS1:def_12;
hence (id the carrier of (S with-replacement (f,g))) * p = the Arity of S9 . o by A20, A19, RELAT_1:53
.= the Arity of S9 . ((id the carrier' of (S with-replacement (f,g))) . o) by A15, FUNCT_1:18 ;
::_thesis: verum
end;

theorem Th40: :: ALGSPEC1:40
for S being non void Signature
for f, g being Function holds
( f,g form_a_replacement_in S iff the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,S with-replacement (f,g) )
proof
let S be non void Signature; ::_thesis: for f, g being Function holds
( f,g form_a_replacement_in S iff the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,S with-replacement (f,g) )
let f, g be Function; ::_thesis: ( f,g form_a_replacement_in S iff the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,S with-replacement (f,g) )
set ff = the carrier of S -indexing f;
set gg = the carrier' of S -indexing g;
set S9 = S with-replacement (f,g);
thus  ( f,g form_a_replacement_in S implies the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,S with-replacement (f,g) ) by Def4; ::_thesis: ( the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,S with-replacement (f,g) implies f,g form_a_replacement_in S )
assume  the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,S with-replacement (f,g) ; ::_thesis: f,g form_a_replacement_in S
then  the carrier of S -indexing f, the carrier' of S -indexing g form_a_replacement_in S by Th31;
hence  f,g form_a_replacement_in S by Th30; ::_thesis: verum
end;

theorem Th41: :: ALGSPEC1:41
for S being non void Signature
for f, g being Function st dom f c= the carrier of S & dom g c= the carrier' of S & f,g form_a_replacement_in S holds
(id the carrier of S) +* f,(id the carrier' of S) +* g form_morphism_between S,S with-replacement (f,g)
proof
let S be non void Signature; ::_thesis: for f, g being Function st dom f c= the carrier of S & dom g c= the carrier' of S & f,g form_a_replacement_in S holds
(id the carrier of S) +* f,(id the carrier' of S) +* g form_morphism_between S,S with-replacement (f,g)
let f, g be Function; ::_thesis: ( dom f c= the carrier of S & dom g c= the carrier' of S & f,g form_a_replacement_in S implies (id the carrier of S) +* f,(id the carrier' of S) +* g form_morphism_between S,S with-replacement (f,g) )
assume that
A1: dom f c= the carrier of S and
A2: dom g c= the carrier' of S ; ::_thesis: ( not f,g form_a_replacement_in S or (id the carrier of S) +* f,(id the carrier' of S) +* g form_morphism_between S,S with-replacement (f,g) )
A3: the carrier' of S -indexing g = (id the carrier' of S) +* g by A2, RELAT_1:68;
 the carrier of S -indexing f = (id the carrier of S) +* f by A1, RELAT_1:68;
hence  ( not f,g form_a_replacement_in S or (id the carrier of S) +* f,(id the carrier' of S) +* g form_morphism_between S,S with-replacement (f,g) ) by A3, Th40; ::_thesis: verum
end;

theorem :: ALGSPEC1:42
for S being non void Signature
for f, g being Function st dom f = the carrier of S & dom g = the carrier' of S & f,g form_a_replacement_in S holds
f,g form_morphism_between S,S with-replacement (f,g)
proof
let S be non void Signature; ::_thesis: for f, g being Function st dom f = the carrier of S & dom g = the carrier' of S & f,g form_a_replacement_in S holds
f,g form_morphism_between S,S with-replacement (f,g)
let f, g be Function; ::_thesis: ( dom f = the carrier of S & dom g = the carrier' of S & f,g form_a_replacement_in S implies f,g form_morphism_between S,S with-replacement (f,g) )
assume that
A1: dom f = the carrier of S and
A2: dom g = the carrier' of S ; ::_thesis: ( not f,g form_a_replacement_in S or f,g form_morphism_between S,S with-replacement (f,g) )
 dom g = dom (id the carrier' of S) by A2;
then A3: (id the carrier' of S) +* g = g by FUNCT_4:19;
 dom f = dom (id the carrier of S) by A1;
then  (id the carrier of S) +* f = f by FUNCT_4:19;
hence  ( not f,g form_a_replacement_in S or f,g form_morphism_between S,S with-replacement (f,g) ) by A1, A2, A3, Th41; ::_thesis: verum
end;

theorem Th43: :: ALGSPEC1:43
for S being non void Signature
for f, g being Function st f,g form_a_replacement_in S holds
S with-replacement (( the carrier of S -indexing f),g) = S with-replacement (f,g)
proof
let S be non void Signature; ::_thesis: for f, g being Function st f,g form_a_replacement_in S holds
S with-replacement (( the carrier of S -indexing f),g) = S with-replacement (f,g)
let f, g be Function; ::_thesis: ( f,g form_a_replacement_in S implies S with-replacement (( the carrier of S -indexing f),g) = S with-replacement (f,g) )
set X = the carrier of S;
set Y = the carrier' of S;
set S2 = S with-replacement (( the carrier of S -indexing f),g);
A1: the carrier of S -indexing ( the carrier of S -indexing f) = the carrier of S -indexing f by Th11;
assume A2: f,g form_a_replacement_in S ; ::_thesis: S with-replacement (( the carrier of S -indexing f),g) = S with-replacement (f,g)
then  the carrier of S -indexing f, the carrier' of S -indexing g form_a_replacement_in S by Th30;
then A3: the carrier of S -indexing f,g form_a_replacement_in S by A1, Th30;
then A4: the carrier of (S with-replacement (( the carrier of S -indexing f),g)) = rng ( the carrier of S -indexing f) by A1, Def4;
A5: the carrier' of (S with-replacement (( the carrier of S -indexing f),g)) = rng ( the carrier' of S -indexing g) by A3, Def4;
 the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,S with-replacement (( the carrier of S -indexing f),g) by A1, A3, Def4;
hence  S with-replacement (( the carrier of S -indexing f),g) = S with-replacement (f,g) by A2, A4, A5, Def4; ::_thesis: verum
end;

theorem Th44: :: ALGSPEC1:44
for S being non void Signature
for f, g being Function st f,g form_a_replacement_in S holds
S with-replacement (f,( the carrier' of S -indexing g)) = S with-replacement (f,g)
proof
let S be non void Signature; ::_thesis: for f, g being Function st f,g form_a_replacement_in S holds
S with-replacement (f,( the carrier' of S -indexing g)) = S with-replacement (f,g)
let f, g be Function; ::_thesis: ( f,g form_a_replacement_in S implies S with-replacement (f,( the carrier' of S -indexing g)) = S with-replacement (f,g) )
set X = the carrier of S;
set Y = the carrier' of S;
set S2 = S with-replacement (f,( the carrier' of S -indexing g));
A1: the carrier' of S -indexing ( the carrier' of S -indexing g) = the carrier' of S -indexing g by Th11;
assume A2: f,g form_a_replacement_in S ; ::_thesis: S with-replacement (f,( the carrier' of S -indexing g)) = S with-replacement (f,g)
then  the carrier of S -indexing f, the carrier' of S -indexing g form_a_replacement_in S by Th30;
then A3: f, the carrier' of S -indexing g form_a_replacement_in S by A1, Th30;
then A4: the carrier' of (S with-replacement (f,( the carrier' of S -indexing g))) = rng ( the carrier' of S -indexing g) by A1, Def4;
A5: the carrier of (S with-replacement (f,( the carrier' of S -indexing g))) = rng ( the carrier of S -indexing f) by A3, Def4;
 the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,S with-replacement (f,( the carrier' of S -indexing g)) by A1, A3, Def4;
hence  S with-replacement (f,( the carrier' of S -indexing g)) = S with-replacement (f,g) by A2, A5, A4, Def4; ::_thesis: verum
end;

begin

definition
let S be Signature;
mode Extension of S ->  Signature means :Def5: :: ALGSPEC1:def 5
S is Subsignature of it;
existence
 ex b1 being Signature st S is Subsignature of b1
proof
take  S ; ::_thesis: S is Subsignature of S
thus  S is Subsignature of S by INSTALG1:15; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines Extension ALGSPEC1:def_5_:_
 for S, b2 being Signature holds
( b2 is Extension of S iff S is Subsignature of b2 );

theorem Th45: :: ALGSPEC1:45
for S being Signature holds S is Extension of S
proof
let S be Signature; ::_thesis: S is Extension of S
thus  S is Subsignature of S by INSTALG1:15; :: according to ALGSPEC1:def_5 ::_thesis: verum
end;

theorem Th46: :: ALGSPEC1:46
for S1 being Signature
for S2 being Extension of S1
for S3 being Extension of S2 holds S3 is Extension of S1
proof
let S1 be Signature; ::_thesis: for S2 being Extension of S1
for S3 being Extension of S2 holds S3 is Extension of S1
let S2 be Extension of S1; ::_thesis: for S3 being Extension of S2 holds S3 is Extension of S1
let S3 be Extension of S2; ::_thesis: S3 is Extension of S1
A1: S2 is Subsignature of S3 by Def5;
 S1 is Subsignature of S2 by Def5;
then  S1 is Subsignature of S3 by A1, INSTALG1:16;
hence  S3 is Extension of S1 by Def5; ::_thesis: verum
end;

theorem Th47: :: ALGSPEC1:47
for S1, S2 being non empty Signature st S1 tolerates S2 holds
S1 +* S2 is Extension of S1
proof
let S1, S2 be non empty Signature; ::_thesis: ( S1 tolerates S2 implies S1 +* S2 is Extension of S1 )
assume that
A1: the Arity of S1 tolerates the Arity of S2 and
A2: the ResultSort of S1 tolerates the ResultSort of S2 ; :: according to CIRCCOMB:def_1 ::_thesis: S1 +* S2 is Extension of S1
set S = S1 +* S2;
 the ResultSort of (S1 +* S2) = the ResultSort of S1 +* the ResultSort of S2 by CIRCCOMB:def_2;
then A3: the ResultSort of S1 c= the ResultSort of (S1 +* S2) by A2, FUNCT_4:28;
set f1 = id the carrier of S1;
set g1 = id the carrier' of S1;
thus  ( dom (id the carrier of S1) = the carrier of S1 & dom (id the carrier' of S1) = the carrier' of S1 ) ; :: according to PUA2MSS1:def_12,INSTALG1:def_2,ALGSPEC1:def_5 ::_thesis: ( rng (id the carrier of S1) c= the carrier of (S1 +* S2) & rng (id the carrier' of S1) c= the carrier' of (S1 +* S2) & the ResultSort of S1 * (id the carrier of S1) = (id the carrier' of S1) * the ResultSort of (S1 +* S2) & ( for b1 being set
for b2 being set holds
( not b1 in the carrier' of S1 or not b2 = the Arity of S1 . b1 or b2 * (id the carrier of S1) = the Arity of (S1 +* S2) . ((id the carrier' of S1) . b1) ) ) )
 dom the ResultSort of S1 = the carrier' of S1 by FUNCT_2:def_1;
then  the ResultSort of S1 = the ResultSort of (S1 +* S2) | the carrier' of S1 by A3, GRFUNC_1:23;
then A4: the ResultSort of S1 = the ResultSort of (S1 +* S2) * (id the carrier' of S1) by RELAT_1:65;
A5: the carrier' of (S1 +* S2) = the carrier' of S1 \/ the carrier' of S2 by CIRCCOMB:def_2;
A6: the carrier of (S1 +* S2) = the carrier of S1 \/ the carrier of S2 by CIRCCOMB:def_2;
thus  ( rng (id the carrier of S1) c= the carrier of (S1 +* S2) & rng (id the carrier' of S1) c= the carrier' of (S1 +* S2) ) by A6, A5, XBOOLE_1:7; ::_thesis: ( the ResultSort of S1 * (id the carrier of S1) = (id the carrier' of S1) * the ResultSort of (S1 +* S2) & ( for b1 being set
for b2 being set holds
( not b1 in the carrier' of S1 or not b2 = the Arity of S1 . b1 or b2 * (id the carrier of S1) = the Arity of (S1 +* S2) . ((id the carrier' of S1) . b1) ) ) )
 rng the ResultSort of S1 c= the carrier of S1 ;
hence  (id the carrier of S1) * the ResultSort of S1 = the ResultSort of (S1 +* S2) * (id the carrier' of S1) by A4, RELAT_1:53; ::_thesis: for b1 being set
for b2 being set holds
( not b1 in the carrier' of S1 or not b2 = the Arity of S1 . b1 or b2 * (id the carrier of S1) = the Arity of (S1 +* S2) . ((id the carrier' of S1) . b1) )
let o be set ; ::_thesis: for b1 being set holds
( not o in the carrier' of S1 or not b1 = the Arity of S1 . o or b1 * (id the carrier of S1) = the Arity of (S1 +* S2) . ((id the carrier' of S1) . o) )
let p be Function; ::_thesis: ( not o in the carrier' of S1 or not p = the Arity of S1 . o or p * (id the carrier of S1) = the Arity of (S1 +* S2) . ((id the carrier' of S1) . o) )
assume that
A7: o in the carrier' of S1 and
A8: p = the Arity of S1 . o ; ::_thesis: p * (id the carrier of S1) = the Arity of (S1 +* S2) . ((id the carrier' of S1) . o)
A9: dom the Arity of S1 = the carrier' of S1 by FUNCT_2:def_1;
then  p in rng the Arity of S1 by A7, A8, FUNCT_1:def_3;
then  p is FinSequence of the carrier of S1 by FINSEQ_1:def_11;
then  rng p c= the carrier of S1 by FINSEQ_1:def_4;
hence (id the carrier of S1) * p = p by RELAT_1:53
.= ( the Arity of S1 +* the Arity of S2) . o by A1, A7, A8, A9, FUNCT_4:15
.= the Arity of (S1 +* S2) . o by CIRCCOMB:def_2
.= the Arity of (S1 +* S2) . ((id the carrier' of S1) . o) by A7, FUNCT_1:18 ;
::_thesis: verum
end;

theorem Th48: :: ALGSPEC1:48
for S1, S2 being non empty Signature holds S1 +* S2 is Extension of S2
proof
let S1, S2 be non empty Signature; ::_thesis: S1 +* S2 is Extension of S2
set S = S1 +* S2;
set f1 = id the carrier of S2;
set g1 = id the carrier' of S2;
thus  ( dom (id the carrier of S2) = the carrier of S2 & dom (id the carrier' of S2) = the carrier' of S2 ) ; :: according to PUA2MSS1:def_12,INSTALG1:def_2,ALGSPEC1:def_5 ::_thesis: ( rng (id the carrier of S2) c= the carrier of (S1 +* S2) & rng (id the carrier' of S2) c= the carrier' of (S1 +* S2) & the ResultSort of S2 * (id the carrier of S2) = (id the carrier' of S2) * the ResultSort of (S1 +* S2) & ( for b1 being set
for b2 being set holds
( not b1 in the carrier' of S2 or not b2 = the Arity of S2 . b1 or b2 * (id the carrier of S2) = the Arity of (S1 +* S2) . ((id the carrier' of S2) . b1) ) ) )
A1: the carrier of (S1 +* S2) = the carrier of S1 \/ the carrier of S2 by CIRCCOMB:def_2;
A2: the carrier' of (S1 +* S2) = the carrier' of S1 \/ the carrier' of S2 by CIRCCOMB:def_2;
thus  ( rng (id the carrier of S2) c= the carrier of (S1 +* S2) & rng (id the carrier' of S2) c= the carrier' of (S1 +* S2) ) by A1, A2, XBOOLE_1:7; ::_thesis: ( the ResultSort of S2 * (id the carrier of S2) = (id the carrier' of S2) * the ResultSort of (S1 +* S2) & ( for b1 being set
for b2 being set holds
( not b1 in the carrier' of S2 or not b2 = the Arity of S2 . b1 or b2 * (id the carrier of S2) = the Arity of (S1 +* S2) . ((id the carrier' of S2) . b1) ) ) )
A3: the ResultSort of (S1 +* S2) = the ResultSort of S1 +* the ResultSort of S2 by CIRCCOMB:def_2;
 dom the ResultSort of S2 = the carrier' of S2 by FUNCT_2:def_1;
then  the ResultSort of S2 = the ResultSort of (S1 +* S2) | the carrier' of S2 by A3, FUNCT_4:25, GRFUNC_1:23;
then A4: the ResultSort of S2 = the ResultSort of (S1 +* S2) * (id the carrier' of S2) by RELAT_1:65;
 rng the ResultSort of S2 c= the carrier of S2 ;
hence  (id the carrier of S2) * the ResultSort of S2 = the ResultSort of (S1 +* S2) * (id the carrier' of S2) by A4, RELAT_1:53; ::_thesis: for b1 being set
for b2 being set holds
( not b1 in the carrier' of S2 or not b2 = the Arity of S2 . b1 or b2 * (id the carrier of S2) = the Arity of (S1 +* S2) . ((id the carrier' of S2) . b1) )
let o be set ; ::_thesis: for b1 being set holds
( not o in the carrier' of S2 or not b1 = the Arity of S2 . o or b1 * (id the carrier of S2) = the Arity of (S1 +* S2) . ((id the carrier' of S2) . o) )
let p be Function; ::_thesis: ( not o in the carrier' of S2 or not p = the Arity of S2 . o or p * (id the carrier of S2) = the Arity of (S1 +* S2) . ((id the carrier' of S2) . o) )
assume that
A5: o in the carrier' of S2 and
A6: p = the Arity of S2 . o ; ::_thesis: p * (id the carrier of S2) = the Arity of (S1 +* S2) . ((id the carrier' of S2) . o)
A7: dom the Arity of S2 = the carrier' of S2 by FUNCT_2:def_1;
then  p in rng the Arity of S2 by A5, A6, FUNCT_1:def_3;
then  p is FinSequence of the carrier of S2 by FINSEQ_1:def_11;
then  rng p c= the carrier of S2 by FINSEQ_1:def_4;
hence (id the carrier of S2) * p = p by RELAT_1:53
.= ( the Arity of S1 +* the Arity of S2) . o by A5, A6, A7, FUNCT_4:13
.= the Arity of (S1 +* S2) . o by CIRCCOMB:def_2
.= the Arity of (S1 +* S2) . ((id the carrier' of S2) . o) by A5, FUNCT_1:18 ;
::_thesis: verum
end;

theorem Th49: :: ALGSPEC1:49
for S1, S2, S being non empty ManySortedSign
for f1, g1, f2, g2 being Function st f1 tolerates f2 & f1,g1 form_morphism_between S1,S & f2,g2 form_morphism_between S2,S holds
f1 +* f2,g1 +* g2 form_morphism_between S1 +* S2,S
proof
let S1, S2, E be non empty ManySortedSign ; ::_thesis: for f1, g1, f2, g2 being Function st f1 tolerates f2 & f1,g1 form_morphism_between S1,E & f2,g2 form_morphism_between S2,E holds
f1 +* f2,g1 +* g2 form_morphism_between S1 +* S2,E
let f1, g1, f2, g2 be Function; ::_thesis: ( f1 tolerates f2 & f1,g1 form_morphism_between S1,E & f2,g2 form_morphism_between S2,E implies f1 +* f2,g1 +* g2 form_morphism_between S1 +* S2,E )
assume that
A1: f1 tolerates f2 and
A2: dom f1 = the carrier of S1 and
A3: dom g1 = the carrier' of S1 and
A4: rng f1 c= the carrier of E and
A5: rng g1 c= the carrier' of E and
A6: f1 * the ResultSort of S1 = the ResultSort of E * g1 and
A7: for o being set
for p being Function st o in the carrier' of S1 & p = the Arity of S1 . o holds
f1 * p = the Arity of E . (g1 . o) and
A8: dom f2 = the carrier of S2 and
A9: dom g2 = the carrier' of S2 and
A10: rng f2 c= the carrier of E and
A11: rng g2 c= the carrier' of E and
A12: f2 * the ResultSort of S2 = the ResultSort of E * g2 and
A13: for o being set
for p being Function st o in the carrier' of S2 & p = the Arity of S2 . o holds
f2 * p = the Arity of E . (g2 . o) ; :: according to PUA2MSS1:def_12 ::_thesis: f1 +* f2,g1 +* g2 form_morphism_between S1 +* S2,E
set f = f1 +* f2;
set g = g1 +* g2;
set S = S1 +* S2;
 the carrier of (S1 +* S2) = the carrier of S1 \/ the carrier of S2 by CIRCCOMB:def_2;
hence  dom (f1 +* f2) = the carrier of (S1 +* S2) by A2, A8, FUNCT_4:def_1; :: according to PUA2MSS1:def_12 ::_thesis: ( dom (g1 +* g2) = the carrier' of (S1 +* S2) & rng (f1 +* f2) c= the carrier of E & rng (g1 +* g2) c= the carrier' of E & the ResultSort of (S1 +* S2) * (f1 +* f2) = (g1 +* g2) * the ResultSort of E & ( for b1 being set
for b2 being set holds
( not b1 in the carrier' of (S1 +* S2) or not b2 = the Arity of (S1 +* S2) . b1 or b2 * (f1 +* f2) = the Arity of E . ((g1 +* g2) . b1) ) ) )
A14: the carrier' of (S1 +* S2) = the carrier' of S1 \/ the carrier' of S2 by CIRCCOMB:def_2;
hence  dom (g1 +* g2) = the carrier' of (S1 +* S2) by A3, A9, FUNCT_4:def_1; ::_thesis: ( rng (f1 +* f2) c= the carrier of E & rng (g1 +* g2) c= the carrier' of E & the ResultSort of (S1 +* S2) * (f1 +* f2) = (g1 +* g2) * the ResultSort of E & ( for b1 being set
for b2 being set holds
( not b1 in the carrier' of (S1 +* S2) or not b2 = the Arity of (S1 +* S2) . b1 or b2 * (f1 +* f2) = the Arity of E . ((g1 +* g2) . b1) ) ) )
A15: rng (f1 +* f2) c= (rng f1) \/ (rng f2) by FUNCT_4:17;
 (rng f1) \/ (rng f2) c= the carrier of E by A4, A10, XBOOLE_1:8;
hence  rng (f1 +* f2) c= the carrier of E by A15, XBOOLE_1:1; ::_thesis: ( rng (g1 +* g2) c= the carrier' of E & the ResultSort of (S1 +* S2) * (f1 +* f2) = (g1 +* g2) * the ResultSort of E & ( for b1 being set
for b2 being set holds
( not b1 in the carrier' of (S1 +* S2) or not b2 = the Arity of (S1 +* S2) . b1 or b2 * (f1 +* f2) = the Arity of E . ((g1 +* g2) . b1) ) ) )
A16: rng (g1 +* g2) c= (rng g1) \/ (rng g2) by FUNCT_4:17;
 (rng g1) \/ (rng g2) c= the carrier' of E by A5, A11, XBOOLE_1:8;
hence  rng (g1 +* g2) c= the carrier' of E by A16, XBOOLE_1:1; ::_thesis: ( the ResultSort of (S1 +* S2) * (f1 +* f2) = (g1 +* g2) * the ResultSort of E & ( for b1 being set
for b2 being set holds
( not b1 in the carrier' of (S1 +* S2) or not b2 = the Arity of (S1 +* S2) . b1 or b2 * (f1 +* f2) = the Arity of E . ((g1 +* g2) . b1) ) ) )
A17: rng the ResultSort of S1 c= the carrier of S1 ;
A18: rng the ResultSort of S2 c= the carrier of S2 ;
A19: dom the ResultSort of E = the carrier' of E by FUNCT_2:def_1;
 the ResultSort of S1 +* the ResultSort of S2 = the ResultSort of (S1 +* S2) by CIRCCOMB:def_2;
hence (f1 +* f2) * the ResultSort of (S1 +* S2) = (f1 * the ResultSort of S1) +* (f2 * the ResultSort of S2) by A1, A2, A8, A17, A18, FUNCT_4:69
.= the ResultSort of E * (g1 +* g2) by A6, A11, A12, A19, FUNCT_7:9 ;
::_thesis: for b1 being set
for b2 being set holds
( not b1 in the carrier' of (S1 +* S2) or not b2 = the Arity of (S1 +* S2) . b1 or b2 * (f1 +* f2) = the Arity of E . ((g1 +* g2) . b1) )
let o be set ; ::_thesis: for b1 being set holds
( not o in the carrier' of (S1 +* S2) or not b1 = the Arity of (S1 +* S2) . o or b1 * (f1 +* f2) = the Arity of E . ((g1 +* g2) . o) )
let p be Function; ::_thesis: ( not o in the carrier' of (S1 +* S2) or not p = the Arity of (S1 +* S2) . o or p * (f1 +* f2) = the Arity of E . ((g1 +* g2) . o) )
assume that
A20: o in the carrier' of (S1 +* S2) and
A21: p = the Arity of (S1 +* S2) . o ; ::_thesis: p * (f1 +* f2) = the Arity of E . ((g1 +* g2) . o)
A22: the Arity of S1 +* the Arity of S2 = the Arity of (S1 +* S2) by CIRCCOMB:def_2;
A23: dom the Arity of S1 = the carrier' of S1 by FUNCT_2:def_1;
A24: dom the Arity of S2 = the carrier' of S2 by FUNCT_2:def_1;
percases ( o in the carrier' of S2 or not o in the carrier' of S2 ) ;
supposeA25: o in the carrier' of S2 ; ::_thesis: p * (f1 +* f2) = the Arity of E . ((g1 +* g2) . o)
then A26: p = the Arity of S2 . o by A21, A22, A24, FUNCT_4:13;
then  p in rng the Arity of S2 by A24, A25, FUNCT_1:def_3;
then  p is FinSequence of the carrier of S2 by FINSEQ_1:def_11;
then  rng p c= dom f2 by A8, FINSEQ_1:def_4;
then A27: dom (f2 * p) = dom p by RELAT_1:27;
A28: dom (f1 * p) c= dom p by RELAT_1:25;
thus (f1 +* f2) * p = (f1 * p) +* (f2 * p) by FUNCT_7:10
.= f2 * p by A28, A27, FUNCT_4:19
.= the Arity of E . (g2 . o) by A13, A25, A26
.= the Arity of E . ((g1 +* g2) . o) by A9, A25, FUNCT_4:13 ; ::_thesis: verum
end;
supposeA29: not o in the carrier' of S2 ; ::_thesis: p * (f1 +* f2) = the Arity of E . ((g1 +* g2) . o)
A30: dom (f2 * p) c= dom p by RELAT_1:25;
A31: o in the carrier' of S1 by A14, A20, A29, XBOOLE_0:def_3;
A32: p = the Arity of S1 . o by A21, A22, A24, A29, FUNCT_4:11;
then  p in rng the Arity of S1 by A23, A31, FUNCT_1:def_3;
then  p is FinSequence of the carrier of S1 by FINSEQ_1:def_11;
then  rng p c= dom f1 by A2, FINSEQ_1:def_4;
then A33: dom (f1 * p) = dom p by RELAT_1:27;
thus (f1 +* f2) * p = (f2 +* f1) * p by A1, FUNCT_4:34
.= (f2 * p) +* (f1 * p) by FUNCT_7:10
.= f1 * p by A33, A30, FUNCT_4:19
.= the Arity of E . (g1 . o) by A7, A31, A32
.= the Arity of E . ((g1 +* g2) . o) by A9, A29, FUNCT_4:11 ; ::_thesis: verum
end;
end;
end;

theorem :: ALGSPEC1:50
for S1, S2, E being non empty Signature holds
( E is Extension of S1 & E is Extension of S2 iff ( S1 tolerates S2 & E is Extension of S1 +* S2 ) )
proof
let S1, S2, E be non empty Signature; ::_thesis: ( E is Extension of S1 & E is Extension of S2 iff ( S1 tolerates S2 & E is Extension of S1 +* S2 ) )
set f1 = id the carrier of S1;
set g1 = id the carrier' of S1;
set f2 = id the carrier of S2;
set g2 = id the carrier' of S2;
A1: ( E is Extension of S1 & E is Extension of S2 implies S1 tolerates S2 )
proof
assume that
A2: S1 is Subsignature of E and
A3: S2 is Subsignature of E ; :: according to ALGSPEC1:def_5 ::_thesis: S1 tolerates S2
A4: the Arity of S2 c= the Arity of E by A3, INSTALG1:11;
 the Arity of S1 c= the Arity of E by A2, INSTALG1:11;
hence  the Arity of S1 tolerates the Arity of S2 by A4, PARTFUN1:52; :: according to CIRCCOMB:def_1 ::_thesis: the ResultSort of S1 tolerates the ResultSort of S2
A5: the ResultSort of S2 c= the ResultSort of E by A3, INSTALG1:11;
 the ResultSort of S1 c= the ResultSort of E by A2, INSTALG1:11;
hence  the ResultSort of S1 tolerates the ResultSort of S2 by A5, PARTFUN1:52; ::_thesis: verum
end;
A6: the carrier of (S1 +* S2) = the carrier of S1 \/ the carrier of S2 by CIRCCOMB:def_2;
 the carrier of S2 c= the carrier of S1 \/ the carrier of S2 by XBOOLE_1:7;
then A7: id the carrier of S2 c= id ( the carrier of S1 \/ the carrier of S2) by FUNCT_4:3;
A8: the carrier' of (S1 +* S2) = the carrier' of S1 \/ the carrier' of S2 by CIRCCOMB:def_2;
 the carrier of S1 c= the carrier of S1 \/ the carrier of S2 by XBOOLE_1:7;
then  id the carrier of S1 c= id ( the carrier of S1 \/ the carrier of S2) by FUNCT_4:3;
then A9: id the carrier of S1 tolerates id the carrier of S2 by A7, PARTFUN1:52;
 ( E is Extension of S1 & E is Extension of S2 implies E is Extension of S1 +* S2 )
proof
assume that
A10: id the carrier of S1, id the carrier' of S1 form_morphism_between S1,E and
A11: id the carrier of S2, id the carrier' of S2 form_morphism_between S2,E ; :: according to INSTALG1:def_2,ALGSPEC1:def_5 ::_thesis: E is Extension of S1 +* S2
 (id the carrier of S1) +* (id the carrier of S2),(id the carrier' of S1) +* (id the carrier' of S2) form_morphism_between S1 +* S2,E by A9, A10, A11, Th49;
then  id the carrier of (S1 +* S2),(id the carrier' of S1) +* (id the carrier' of S2) form_morphism_between S1 +* S2,E by A6, FUNCT_4:22;
hence  id the carrier of (S1 +* S2), id the carrier' of (S1 +* S2) form_morphism_between S1 +* S2,E by A8, FUNCT_4:22; :: according to INSTALG1:def_2,ALGSPEC1:def_5 ::_thesis: verum
end;
hence  ( E is Extension of S1 & E is Extension of S2 implies ( S1 tolerates S2 & E is Extension of S1 +* S2 ) ) by A1; ::_thesis: ( S1 tolerates S2 & E is Extension of S1 +* S2 implies ( E is Extension of S1 & E is Extension of S2 ) )
assume  S1 tolerates S2 ; ::_thesis: ( not E is Extension of S1 +* S2 or ( E is Extension of S1 & E is Extension of S2 ) )
then A12: S1 +* S2 is Extension of S1 by Th47;
 S1 +* S2 is Extension of S2 by Th48;
hence  ( not E is Extension of S1 +* S2 or ( E is Extension of S1 & E is Extension of S2 ) ) by A12, Th46; ::_thesis: verum
end;

registration
let S be non empty Signature;
cluster  ->  non empty for Extension of S;
coherence
 for b1 being Extension of S holds not b1 is empty
proof
set x = the Element of S;
let E be Extension of S; ::_thesis: not E is empty
 S is Subsignature of E by Def5;
then A1: the carrier of S c= the carrier of E by INSTALG1:10;
 the Element of S in the carrier of S ;
hence  not the carrier of E is empty by A1; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;

registration
let S be non void Signature;
cluster  ->  non void for Extension of S;
coherence
 for b1 being Extension of S holds not b1 is void
proof
set x = the OperSymbol of S;
let E be Extension of S; ::_thesis: not E is void
 S is Subsignature of E by Def5;
then A1: the carrier' of S c= the carrier' of E by INSTALG1:10;
 the OperSymbol of S in the carrier' of S ;
hence  not the carrier' of E is empty by A1; :: according to STRUCT_0:def_13 ::_thesis: verum
end;
end;

theorem Th51: :: ALGSPEC1:51
for S, T being Signature st S is empty holds
T is Extension of S
proof
let S, T be Signature; ::_thesis: ( S is empty implies T is Extension of S )
assume A1: the carrier of S is empty ; :: according to STRUCT_0:def_1 ::_thesis: T is Extension of S
then  the carrier' of S = {} by INSTALG1:def_1;
then  the Arity of S = {} ;
then A2: the Arity of S c= the Arity of T by XBOOLE_1:2;
 the ResultSort of S = {} by A1;
then  the ResultSort of S c= the ResultSort of T by XBOOLE_1:2;
hence  S is Subsignature of T by A1, A2, INSTALG1:13, XBOOLE_1:2; :: according to ALGSPEC1:def_5 ::_thesis: verum
end;

registration
let S be Signature;
cluster non empty non void strict feasible for Extension of S;
existence
 ex b1 being Extension of S st
( not b1 is empty & not b1 is void & b1 is strict )
proof
set S9 = the non void strict Signature;
percases ( S is empty or not S is empty ) ;
suppose S is empty ; ::_thesis: ex b1 being Extension of S st
( not b1 is empty & not b1 is void & b1 is strict )
then  the non void strict Signature is Extension of S by Th51;
hence  ex b1 being Extension of S st
( not b1 is empty & not b1 is void & b1 is strict ) ; ::_thesis: verum
end;
suppose not S is empty ; ::_thesis: ex b1 being Extension of S st
( not b1 is empty & not b1 is void & b1 is strict )
then reconsider S1 = S as non empty Signature ;
reconsider E = the non void strict Signature +* S1 as Extension of S by Th48;
take  E ; ::_thesis: ( not E is empty & not E is void & E is strict )
thus  not the carrier of E is empty ; :: according to STRUCT_0:def_1 ::_thesis: ( not E is void & E is strict )
thus  not the carrier' of E is empty ; :: according to STRUCT_0:def_13 ::_thesis: E is strict
thus  E is strict ; ::_thesis: verum
end;
end;
end;
end;

theorem Th52: :: ALGSPEC1:52
for f, g being Function
for S being non void Signature
for E being Extension of S st f,g form_a_replacement_in E holds
f,g form_a_replacement_in S
proof
let f, g be Function; ::_thesis: for S being non void Signature
for E being Extension of S st f,g form_a_replacement_in E holds
f,g form_a_replacement_in S
let S be non void Signature; ::_thesis: for E being Extension of S st f,g form_a_replacement_in E holds
f,g form_a_replacement_in S
let E be Extension of S; ::_thesis: ( f,g form_a_replacement_in E implies f,g form_a_replacement_in S )
set f9 = the carrier of E -indexing f;
set g9 = the carrier' of E -indexing g;
set T = E with-replacement (f,g);
A1: S is Subsignature of E by Def5;
then A2: ( the carrier of E -indexing f) | the carrier of S = the carrier of S -indexing f by Th17, INSTALG1:10;
A3: ( the carrier' of E -indexing g) | the carrier' of S = the carrier' of S -indexing g by A1, Th17, INSTALG1:10;
assume  f,g form_a_replacement_in E ; ::_thesis: f,g form_a_replacement_in S
then  the carrier of E -indexing f, the carrier' of E -indexing g form_morphism_between E,E with-replacement (f,g) by Th40;
then  ( the carrier of E -indexing f) | the carrier of S,( the carrier' of E -indexing g) | the carrier' of S form_a_replacement_in S by A1, Th31, INSTALG1:18;
hence  f,g form_a_replacement_in S by A2, A3, Th30; ::_thesis: verum
end;

theorem :: ALGSPEC1:53
for f, g being Function
for S being non void Signature
for E being Extension of S st f,g form_a_replacement_in E holds
E with-replacement (f,g) is Extension of S with-replacement (f,g)
proof
let f, g be Function; ::_thesis: for S being non void Signature
for E being Extension of S st f,g form_a_replacement_in E holds
E with-replacement (f,g) is Extension of S with-replacement (f,g)
let S be non void Signature; ::_thesis: for E being Extension of S st f,g form_a_replacement_in E holds
E with-replacement (f,g) is Extension of S with-replacement (f,g)
let E be Extension of S; ::_thesis: ( f,g form_a_replacement_in E implies E with-replacement (f,g) is Extension of S with-replacement (f,g) )
set f9 = the carrier of E -indexing f;
set g9 = the carrier' of E -indexing g;
set gg = the carrier' of S -indexing g;
set T = E with-replacement (f,g);
A1: the carrier' of S -indexing ( the carrier' of S -indexing g) = the carrier' of S -indexing g by Th11;
assume A2: f,g form_a_replacement_in E ; ::_thesis: E with-replacement (f,g) is Extension of S with-replacement (f,g)
then  f,g form_a_replacement_in S by Th52;
then  the carrier of S -indexing f, the carrier' of S -indexing g form_a_replacement_in S by Th30;
then A3: f, the carrier' of S -indexing g form_a_replacement_in S by A1, Th30;
A4: S is Subsignature of E by Def5;
then A5: ( the carrier' of E -indexing g) | the carrier' of S = the carrier' of S -indexing g by Th17, INSTALG1:10;
 the carrier of E -indexing f, the carrier' of E -indexing g form_morphism_between E,E with-replacement (f,g) by A2, Th40;
then A6: S with-replacement ((( the carrier of E -indexing f) | the carrier of S),(( the carrier' of E -indexing g) | the carrier' of S)) is Subsignature of E with-replacement (f,g) by A4, Th39, INSTALG1:18;
 ( the carrier of E -indexing f) | the carrier of S = the carrier of S -indexing f by A4, Th17, INSTALG1:10;
then  S with-replacement ((( the carrier of E -indexing f) | the carrier of S),(( the carrier' of E -indexing g) | the carrier' of S)) = S with-replacement (f,( the carrier' of S -indexing g)) by A3, A5, Th43;
hence  S with-replacement (f,g) is Subsignature of E with-replacement (f,g) by A2, A6, Th44, Th52; :: according to ALGSPEC1:def_5 ::_thesis: verum
end;

theorem :: ALGSPEC1:54
for S1, S2 being non void Signature st S1 tolerates S2 holds
for f, g being Function st f,g form_a_replacement_in S1 +* S2 holds
(S1 +* S2) with-replacement (f,g) = (S1 with-replacement (f,g)) +* (S2 with-replacement (f,g))
proof
let S1, S2 be non void Signature; ::_thesis: ( S1 tolerates S2 implies for f, g being Function st f,g form_a_replacement_in S1 +* S2 holds
(S1 +* S2) with-replacement (f,g) = (S1 with-replacement (f,g)) +* (S2 with-replacement (f,g)) )
assume A1: S1 tolerates S2 ; ::_thesis: for f, g being Function st f,g form_a_replacement_in S1 +* S2 holds
(S1 +* S2) with-replacement (f,g) = (S1 with-replacement (f,g)) +* (S2 with-replacement (f,g))
A2: the ResultSort of S1 tolerates the ResultSort of S2 by A1, CIRCCOMB:def_1;
A3: rng the Arity of S2 c= the carrier of S2 * ;
A4: rng the ResultSort of S2 c= the carrier of S2 ;
A5: rng the ResultSort of S1 c= the carrier of S1 ;
set S = S1 +* S2;
let f, g be Function; ::_thesis: ( f,g form_a_replacement_in S1 +* S2 implies (S1 +* S2) with-replacement (f,g) = (S1 with-replacement (f,g)) +* (S2 with-replacement (f,g)) )
assume A6: f,g form_a_replacement_in S1 +* S2 ; ::_thesis: (S1 +* S2) with-replacement (f,g) = (S1 with-replacement (f,g)) +* (S2 with-replacement (f,g))
deffunc H1( non void Signature) ->  ManySortedSet of the carrier of $1 = the carrier of $1 -indexing f;
deffunc H2( non void Signature) ->  non empty non void strict ManySortedSign = $1 with-replacement (f,g);
A7: dom H1(S2) = the carrier of S2 by PARTFUN1:def_2;
A8: H1(S1) tolerates H1(S2) by Th19;
A9: S1 +* S2 is Extension of S1 by A1, Th47;
then reconsider F1 = H1(S1) as Function of the carrier of S1, the carrier of H2(S1) by A6, Th36, Th52;
A10: dom (H1(S1) * the ResultSort of S1) = the carrier' of S1 by PARTFUN1:def_2;
deffunc H3( non void Signature) ->  ManySortedSet of the carrier' of $1 = the carrier' of $1 -indexing g;
A11: dom H1(S1) = the carrier of S1 by PARTFUN1:def_2;
A12: dom H3(S1) = the carrier' of S1 by PARTFUN1:def_2;
set g1 = the rng-retract of H3(S1);
set g2 = the rng-retract of H3(S2);
A13: the ResultSort of (S1 +* S2) = the ResultSort of S1 +* the ResultSort of S2 by CIRCCOMB:def_2;
A14: rng the rng-retract of H3(S2) c= dom H3(S2) by Th23;
A15: the carrier' of (S1 +* S2) = the carrier' of S1 \/ the carrier' of S2 by CIRCCOMB:def_2;
then  H3(S1 +* S2) = H3(S1) \/ H3(S2) by Th20;
then A16: rng H3(S1 +* S2) = (rng H3(S1)) \/ (rng H3(S2)) by RELAT_1:12;
A17: dom H3(S2) = the carrier' of S2 by PARTFUN1:def_2;
A18: S1 +* S2 is Extension of S2 by Th48;
then reconsider F2 = H1(S2) as Function of the carrier of S2, the carrier of H2(S2) by A6, Th36, Th52;
A19: dom (H1(S2) * the ResultSort of S2) = the carrier' of S2 by PARTFUN1:def_2;
A20: the carrier of (S1 +* S2) = the carrier of S1 \/ the carrier of S2 by CIRCCOMB:def_2;
then A21: H1(S1 +* S2) = H1(S1) +* H1(S2) by Th18;
 H1(S1 +* S2) = H1(S1) \/ H1(S2) by A20, Th20;
then A22: rng H1(S1 +* S2) = (rng H1(S1)) \/ (rng H1(S2)) by RELAT_1:12;
A23: dom ((F2 *) * the Arity of S2) = the carrier' of S2 by FUNCT_2:def_1;
A24: dom (F2 *) = the carrier of S2 * by FUNCT_2:def_1;
 H3(S1 +* S2) = H3(S1) +* H3(S2) by A15, Th18;
then reconsider gg = the rng-retract of H3(S1) +* the rng-retract of H3(S2) as rng-retract of H3(S1 +* S2) by Th19, Th27;
A25: rng the rng-retract of H3(S1) c= dom H3(S1) by Th23;
A26: the ResultSort of H2(S1 +* S2) = (H1(S1 +* S2) * the ResultSort of (S1 +* S2)) * gg by A6, Th38
.= ((H1(S1) * the ResultSort of S1) +* (H1(S2) * the ResultSort of S2)) * gg by A13, A21, A5, A4, A11, A7, Th19, FUNCT_4:69
.= ((H1(S1) * the ResultSort of S1) * the rng-retract of H3(S1)) +* ((H1(S2) * the ResultSort of S2) * the rng-retract of H3(S2)) by A8, A25, A14, A12, A17, A10, A19, A2, Th4, FUNCT_4:69
.= the ResultSort of H2(S1) +* ((H1(S2) * the ResultSort of S2) * the rng-retract of H3(S2)) by A6, A9, Th38, Th52
.= the ResultSort of H2(S1) +* the ResultSort of H2(S2) by A6, A18, Th38, Th52 ;
A27: the carrier of H2(S1 +* S2) = rng H1(S1 +* S2) by A6, Def4;
A28: dom ((F1 *) * the Arity of S1) = the carrier' of S1 by FUNCT_2:def_1;
reconsider FS = H1(S1 +* S2) as Function of the carrier of (S1 +* S2), the carrier of H2(S1 +* S2) by A6, Th36;
A29: (rng the Arity of (S1 +* S2)) /\ (dom (FS *)) c= rng the Arity of (S1 +* S2) by XBOOLE_1:17;
A30: the Arity of (S1 +* S2) = the Arity of S1 +* the Arity of S2 by CIRCCOMB:def_2;
A31: f,g form_a_replacement_in S1 by A6, A9, Th52;
then A32: the carrier of H2(S1) = rng H1(S1) by Def4;
A33: the carrier' of H2(S1) = rng H3(S1) by A31, Def4;
A34: the carrier' of H2(S1 +* S2) = rng H3(S1 +* S2) by A6, Def4;
A35: dom (F1 *) = the carrier of S1 * by FUNCT_2:def_1;
 the Arity of S1 tolerates the Arity of S2 by A1, CIRCCOMB:def_1;
then  the Arity of (S1 +* S2) = the Arity of S1 \/ the Arity of S2 by A30, FUNCT_4:30;
then  rng the Arity of (S1 +* S2) = (rng the Arity of S1) \/ (rng the Arity of S2) by RELAT_1:12;
then  rng the Arity of (S1 +* S2) c= ( the carrier of S1 *) \/ ( the carrier of S2 *) by XBOOLE_1:13;
then  rng the Arity of (S1 +* S2) c= dom ((F1 *) +* (F2 *)) by A35, A24, FUNCT_4:def_1;
then A36: (rng the Arity of (S1 +* S2)) /\ (dom (FS *)) c= dom ((F1 *) +* (F2 *)) by A29, XBOOLE_1:1;
A37: f,g form_a_replacement_in S2 by A6, A18, Th52;
then A38: the carrier of H2(S2) = rng H1(S2) by Def4;
A39: the carrier' of H2(S2) = rng H3(S2) by A37, Def4;
A40: F1 * tolerates F2 * by Th6, Th19;
A41: (F1 *) +* (F2 *) c= (F1 *) \/ (F2 *) by FUNCT_4:29;
 F2 = FS | the carrier of S2 by A20, Th17, XBOOLE_1:7;
then A42: F2 * c= FS * by Th5, RELAT_1:59;
 F1 = FS | the carrier of S1 by A20, Th17, XBOOLE_1:7;
then  F1 * c= FS * by Th5, RELAT_1:59;
then  (F1 *) \/ (F2 *) c= FS * by A42, XBOOLE_1:8;
then A43: (F1 *) +* (F2 *) c= FS * by A41, XBOOLE_1:1;
A44: the Arity of S1 tolerates the Arity of S2 by A1, CIRCCOMB:def_1;
A45: rng the Arity of S1 c= the carrier of S1 * ;
the Arity of H2(S1 +* S2) = ((FS *) * the Arity of (S1 +* S2)) * gg by A6, Th37
.= (((F1 *) +* (F2 *)) * the Arity of (S1 +* S2)) * gg by A43, A36, Th2
.= (((F1 *) * the Arity of S1) +* ((F2 *) * the Arity of S2)) * gg by A30, A8, A45, A3, A35, A24, Th6, FUNCT_4:69
.= (((F1 *) * the Arity of S1) * the rng-retract of H3(S1)) +* (((F2 *) * the Arity of S2) * the rng-retract of H3(S2)) by A25, A14, A12, A17, A40, A44, A28, A23, Th4, FUNCT_4:69
.= the Arity of H2(S1) +* (((F2 *) * the Arity of S2) * the rng-retract of H3(S2)) by A6, A9, Th37, Th52
.= the Arity of H2(S1) +* the Arity of H2(S2) by A6, A18, Th37, Th52 ;
hence  (S1 +* S2) with-replacement (f,g) = (S1 with-replacement (f,g)) +* (S2 with-replacement (f,g)) by A22, A27, A32, A38, A16, A34, A33, A39, A26, CIRCCOMB:def_2; ::_thesis: verum
end;

begin

definition
mode Algebra  ->  set  means :Def6: :: ALGSPEC1:def 6
 ex S being non void Signature st it is feasible MSAlgebra over S;
existence
 ex b1 being set ex S being non void Signature st b1 is feasible MSAlgebra over S
proof
set S = the non void Signature;
set A = the feasible MSAlgebra over the non void Signature;
take  the feasible MSAlgebra over the non void Signature ; ::_thesis: ex S being non void Signature st the feasible MSAlgebra over the non void Signature is feasible MSAlgebra over S
take  the non void Signature ; ::_thesis: the feasible MSAlgebra over the non void Signature is feasible MSAlgebra over the non void Signature
thus  the feasible MSAlgebra over the non void Signature is feasible MSAlgebra over the non void Signature ; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines Algebra ALGSPEC1:def_6_:_
 for b1 being set holds
( b1 is Algebra iff ex S being non void Signature st b1 is feasible MSAlgebra over S );

definition
let S be Signature;
mode Algebra of S ->  Algebra  means :Def7: :: ALGSPEC1:def 7
 ex E being non void Extension of S st it is feasible MSAlgebra over E;
existence
 ex b1 being Algebra ex E being non void Extension of S st b1 is feasible MSAlgebra over E
proof
set E = the non void Extension of S;
set A = the feasible MSAlgebra over the non void Extension of S;
 the feasible MSAlgebra over the non void Extension of S is Algebra by Def6;
hence  ex b1 being Algebra ex E being non void Extension of S st b1 is feasible MSAlgebra over E ; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines Algebra ALGSPEC1:def_7_:_
 for S being Signature
for b2 being Algebra holds
( b2 is Algebra of S iff ex E being non void Extension of S st b2 is feasible MSAlgebra over E );

theorem :: ALGSPEC1:55
for S being non void Signature
for A being feasible MSAlgebra over S holds A is Algebra of S
proof
let S be non void Signature; ::_thesis: for A being feasible MSAlgebra over S holds A is Algebra of S
let A be feasible MSAlgebra over S; ::_thesis: A is Algebra of S
A1: S is Extension of S by Th45;
 A is Algebra by Def6;
hence  A is Algebra of S by A1, Def7; ::_thesis: verum
end;

theorem :: ALGSPEC1:56
for S being Signature
for E being Extension of S
for A being Algebra of E holds A is Algebra of S
proof
let S be Signature; ::_thesis: for E being Extension of S
for A being Algebra of E holds A is Algebra of S
let E be Extension of S; ::_thesis: for A being Algebra of E holds A is Algebra of S
let A be Algebra of E; ::_thesis: A is Algebra of S
consider E9 being non void Extension of E such that
A1: A is feasible MSAlgebra over E9 by Def7;
 E9 is Extension of S by Th46;
hence  A is Algebra of S by A1, Def7; ::_thesis: verum
end;

theorem Th57: :: ALGSPEC1:57
for S being Signature
for E being non empty Signature
for A being MSAlgebra over E st A is Algebra of S holds
( the carrier of S c= the carrier of E & the carrier' of S c= the carrier' of E )
proof
let S be Signature; ::_thesis: for E being non empty Signature
for A being MSAlgebra over E st A is Algebra of S holds
( the carrier of S c= the carrier of E & the carrier' of S c= the carrier' of E )
let E be non empty Signature; ::_thesis: for A being MSAlgebra over E st A is Algebra of S holds
( the carrier of S c= the carrier of E & the carrier' of S c= the carrier' of E )
let A be MSAlgebra over E; ::_thesis: ( A is Algebra of S implies ( the carrier of S c= the carrier of E & the carrier' of S c= the carrier' of E ) )
A1: dom the Charact of A = the carrier' of E by PARTFUN1:def_2;
assume  A is Algebra of S ; ::_thesis: ( the carrier of S c= the carrier of E & the carrier' of S c= the carrier' of E )
then consider ES being non void Extension of S such that
A2: A is feasible MSAlgebra over ES by Def7;
reconsider B = A as MSAlgebra over ES by A2;
A3: dom the Sorts of A = the carrier of E by PARTFUN1:def_2;
A4: S is Subsignature of ES by Def5;
 dom the Sorts of B = the carrier of ES by PARTFUN1:def_2;
hence  the carrier of S c= the carrier of E by A4, A3, INSTALG1:10; ::_thesis: the carrier' of S c= the carrier' of E
 dom the Charact of B = the carrier' of ES by PARTFUN1:def_2;
hence  the carrier' of S c= the carrier' of E by A4, A1, INSTALG1:10; ::_thesis: verum
end;

theorem Th58: :: ALGSPEC1:58
for S being non void Signature
for E being non empty Signature
for A being MSAlgebra over E st A is Algebra of S holds
for o being OperSymbol of S holds the Charact of A . o is Function of (( the Sorts of A #) . (the_arity_of o)),( the Sorts of A . (the_result_sort_of o))
proof
let S be non void Signature; ::_thesis: for E being non empty Signature
for A being MSAlgebra over E st A is Algebra of S holds
for o being OperSymbol of S holds the Charact of A . o is Function of (( the Sorts of A #) . (the_arity_of o)),( the Sorts of A . (the_result_sort_of o))
let E be non empty Signature; ::_thesis: for A being MSAlgebra over E st A is Algebra of S holds
for o being OperSymbol of S holds the Charact of A . o is Function of (( the Sorts of A #) . (the_arity_of o)),( the Sorts of A . (the_result_sort_of o))
let A be MSAlgebra over E; ::_thesis: ( A is Algebra of S implies for o being OperSymbol of S holds the Charact of A . o is Function of (( the Sorts of A #) . (the_arity_of o)),( the Sorts of A . (the_result_sort_of o)) )
A1: dom the Sorts of A = the carrier of E by PARTFUN1:def_2;
assume  A is Algebra of S ; ::_thesis: for o being OperSymbol of S holds the Charact of A . o is Function of (( the Sorts of A #) . (the_arity_of o)),( the Sorts of A . (the_result_sort_of o))
then consider ES being non void Extension of S such that
A2: A is feasible MSAlgebra over ES by Def7;
reconsider B = A as MSAlgebra over ES by A2;
let o be OperSymbol of S; ::_thesis: the Charact of A . o is Function of (( the Sorts of A #) . (the_arity_of o)),( the Sorts of A . (the_result_sort_of o))
A3: dom the Sorts of B = the carrier of ES by PARTFUN1:def_2;
A4: S is Subsignature of ES by Def5;
then A5: the carrier' of S c= the carrier' of ES by INSTALG1:10;
 the ResultSort of S = the ResultSort of ES | the carrier' of S by A4, INSTALG1:12;
then A6: the_result_sort_of o = the ResultSort of ES . o by FUNCT_1:49;
 the Arity of S = the Arity of ES | the carrier' of S by A4, INSTALG1:12;
then A7: the_arity_of o = the Arity of ES . o by FUNCT_1:49;
A8: o in the carrier' of S ;
then A9: the Charact of B . o is Function of ((( the Sorts of B #) * the Arity of ES) . o),(( the Sorts of B * the ResultSort of ES) . o) by A5, PBOOLE:def_15;
 the carrier' of ES = dom the ResultSort of ES by FUNCT_2:def_1;
then A10: ( the Sorts of B * the ResultSort of ES) . o = the Sorts of A . (the_result_sort_of o) by A8, A5, A6, FUNCT_1:13;
 the carrier' of ES = dom the Arity of ES by FUNCT_2:def_1;
then  (( the Sorts of B #) * the Arity of ES) . o = ( the Sorts of A #) . (the_arity_of o) by A8, A5, A3, A1, A7, FUNCT_1:13;
hence  the Charact of A . o is Function of (( the Sorts of A #) . (the_arity_of o)),( the Sorts of A . (the_result_sort_of o)) by A10, A9; ::_thesis: verum
end;

theorem :: ALGSPEC1:59
for S being non empty Signature
for A being Algebra of S
for E being non empty ManySortedSign st A is MSAlgebra over E holds
A is MSAlgebra over E +* S
proof
let S be non empty Signature; ::_thesis: for A being Algebra of S
for E being non empty ManySortedSign st A is MSAlgebra over E holds
A is MSAlgebra over E +* S
let A be Algebra of S; ::_thesis: for E being non empty ManySortedSign st A is MSAlgebra over E holds
A is MSAlgebra over E +* S
let E be non empty ManySortedSign ; ::_thesis: ( A is MSAlgebra over E implies A is MSAlgebra over E +* S )
set T = E +* S;
A1: dom the ResultSort of S = the carrier' of S by FUNCT_2:def_1;
A2: the ResultSort of (E +* S) = the ResultSort of E +* the ResultSort of S by CIRCCOMB:def_2;
assume  A is MSAlgebra over E ; ::_thesis: A is MSAlgebra over E +* S
then reconsider B = A as MSAlgebra over E ;
A3: the Arity of (E +* S) = the Arity of E +* the Arity of S by CIRCCOMB:def_2;
 B is Algebra of S ;
then A4: the carrier of S c= the carrier of E by Th57;
 the carrier of (E +* S) = the carrier of E \/ the carrier of S by CIRCCOMB:def_2;
then A5: the carrier of (E +* S) = the carrier of E by A4, XBOOLE_1:12;
then reconsider Ss = the Sorts of B as ManySortedSet of the carrier of (E +* S) ;
 B is Algebra of S ;
then A6: the carrier' of S c= the carrier' of E by Th57;
 the carrier' of (E +* S) = the carrier' of E \/ the carrier' of S by CIRCCOMB:def_2;
then A7: the carrier' of (E +* S) = the carrier' of E by A6, XBOOLE_1:12;
A8: dom the Arity of S = the carrier' of S by FUNCT_2:def_1;
now__::_thesis:_for_i_being_set_st_i_in_the_carrier'_of_(E_+*_S)_holds_
the_Charact_of_B_._i_is_Function_of_(((Ss_#)_*_the_Arity_of_(E_+*_S))_._i),((Ss_*_the_ResultSort_of_(E_+*_S))_._i)
let i be set ; ::_thesis: ( i in the carrier' of (E +* S) implies the Charact of B . i is Function of (((Ss #) * the Arity of (E +* S)) . i),((Ss * the ResultSort of (E +* S)) . i) )
assume A9: i in the carrier' of (E +* S) ; ::_thesis: the Charact of B . i is Function of (((Ss #) * the Arity of (E +* S)) . i),((Ss * the ResultSort of (E +* S)) . i)
then A10: (Ss * the ResultSort of (E +* S)) . i = Ss . ( the ResultSort of (E +* S) . i) by FUNCT_2:15;
A11: now__::_thesis:_(_i_in_the_carrier'_of_S_implies_the_Charact_of_B_._i_is_Function_of_((_the_Sorts_of_B_#)_._(_the_Arity_of_(E_+*_S)_._i)),(_the_Sorts_of_B_._(_the_ResultSort_of_(E_+*_S)_._i))_)
assume A12: i in the carrier' of S ; ::_thesis: the Charact of B . i is Function of (( the Sorts of B #) . ( the Arity of (E +* S) . i)),( the Sorts of B . ( the ResultSort of (E +* S) . i))
then reconsider S9 = S as non void Signature ;
reconsider o = i as OperSymbol of S9 by A12;
A13: the Arity of (E +* S) . o = the_arity_of o by A8, A3, FUNCT_4:13;
 the ResultSort of (E +* S) . o = the_result_sort_of o by A1, A2, FUNCT_4:13;
hence  the Charact of B . i is Function of (( the Sorts of B #) . ( the Arity of (E +* S) . i)),( the Sorts of B . ( the ResultSort of (E +* S) . i)) by A13, Th58; ::_thesis: verum
end;
A14: ( not i in the carrier' of S implies ( the Arity of (E +* S) . i = the Arity of E . i & the ResultSort of (E +* S) . i = the ResultSort of E . i ) ) by A8, A1, A3, A2, FUNCT_4:11;
A15: ((Ss #) * the Arity of E) . i = (Ss #) . ( the Arity of E . i) by A7, A9, FUNCT_2:15;
A16: ((Ss #) * the Arity of (E +* S)) . i = (Ss #) . ( the Arity of (E +* S) . i) by A9, FUNCT_2:15;
 (Ss * the ResultSort of E) . i = Ss . ( the ResultSort of E . i) by A7, A9, FUNCT_2:15;
hence  the Charact of B . i is Function of (((Ss #) * the Arity of (E +* S)) . i),((Ss * the ResultSort of (E +* S)) . i) by A5, A7, A9, A15, A10, A16, A11, A14, PBOOLE:def_15; ::_thesis: verum
end;
then reconsider C = the Charact of B as ManySortedFunction of (Ss #) * the Arity of (E +* S),Ss * the ResultSort of (E +* S) by A7, PBOOLE:def_15;
set B9 = MSAlgebra(# Ss,C #);
 the Sorts of MSAlgebra(# Ss,C #) = the Sorts of B ;
then  B is MSAlgebra over E +* S ;
hence  A is MSAlgebra over E +* S ; ::_thesis: verum
end;

theorem Th60: :: ALGSPEC1:60
for S1, S2 being non empty Signature
for A being MSAlgebra over S1 st A is MSAlgebra over S2 holds
( the carrier of S1 = the carrier of S2 & the carrier' of S1 = the carrier' of S2 )
proof
let S1, S2 be non empty Signature; ::_thesis: for A being MSAlgebra over S1 st A is MSAlgebra over S2 holds
( the carrier of S1 = the carrier of S2 & the carrier' of S1 = the carrier' of S2 )
let A be MSAlgebra over S1; ::_thesis: ( A is MSAlgebra over S2 implies ( the carrier of S1 = the carrier of S2 & the carrier' of S1 = the carrier' of S2 ) )
assume  A is MSAlgebra over S2 ; ::_thesis: ( the carrier of S1 = the carrier of S2 & the carrier' of S1 = the carrier' of S2 )
then reconsider B = A as MSAlgebra over S2 ;
 the Sorts of A = the Sorts of B ;
then  dom the Sorts of A = the carrier of S2 by PARTFUN1:def_2;
hence  the carrier of S1 = the carrier of S2 by PARTFUN1:def_2; ::_thesis: the carrier' of S1 = the carrier' of S2
 the Charact of A = the Charact of B ;
then  dom the Charact of A = the carrier' of S2 by PARTFUN1:def_2;
hence  the carrier' of S1 = the carrier' of S2 by PARTFUN1:def_2; ::_thesis: verum
end;

registration
let S be non void Signature;
let A be non-empty disjoint_valued MSAlgebra over S;
cluster the Sorts of A ->  one-to-one ;
coherence
 the Sorts of A is one-to-one
proof
let x, y be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x in dom the Sorts of A or not y in dom the Sorts of A or not the Sorts of A . x = the Sorts of A . y or x = y )
assume that
A1: x in dom the Sorts of A and
A2: y in dom the Sorts of A ; ::_thesis: ( not the Sorts of A . x = the Sorts of A . y or x = y )
reconsider a = x, b = y as SortSymbol of S by A1, A2;
assume that
A3: the Sorts of A . x = the Sorts of A . y and
A4: x <> y ; ::_thesis: contradiction
 the Sorts of A is disjoint_valued by MSAFREE1:def_2;
then  the Sorts of A . a misses the Sorts of A . b by A4, PROB_2:def_2;
hence  contradiction by A3; ::_thesis: verum
end;
end;

theorem Th61: :: ALGSPEC1:61
for S being non void Signature
for A being disjoint_valued MSAlgebra over S
for C1, C2 being Component of the Sorts of A holds
( C1 = C2 or C1 misses C2 )
proof
let S be non void Signature; ::_thesis: for A being disjoint_valued MSAlgebra over S
for C1, C2 being Component of the Sorts of A holds
( C1 = C2 or C1 misses C2 )
let A be disjoint_valued MSAlgebra over S; ::_thesis: for C1, C2 being Component of the Sorts of A holds
( C1 = C2 or C1 misses C2 )
let C1, C2 be Component of the Sorts of A; ::_thesis: ( C1 = C2 or C1 misses C2 )
A1: ex y being set st
( y in dom the Sorts of A & C2 = the Sorts of A . y ) by FUNCT_1:def_3;
A2: the Sorts of A is disjoint_valued by MSAFREE1:def_2;
 ex x being set st
( x in dom the Sorts of A & C1 = the Sorts of A . x ) by FUNCT_1:def_3;
hence  ( C1 = C2 or C1 misses C2 ) by A1, A2, PROB_2:def_2; ::_thesis: verum
end;

theorem Th62: :: ALGSPEC1:62
for S, S9 being non void Signature
for A being non-empty disjoint_valued MSAlgebra over S st A is MSAlgebra over S9 holds
ManySortedSign(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S #) = ManySortedSign(# the carrier of S9, the carrier' of S9, the Arity of S9, the ResultSort of S9 #)
proof
let S, E be non void Signature; ::_thesis: for A being non-empty disjoint_valued MSAlgebra over S st A is MSAlgebra over E holds
ManySortedSign(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S #) = ManySortedSign(# the carrier of E, the carrier' of E, the Arity of E, the ResultSort of E #)
let A be non-empty disjoint_valued MSAlgebra over S; ::_thesis: ( A is MSAlgebra over E implies ManySortedSign(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S #) = ManySortedSign(# the carrier of E, the carrier' of E, the Arity of E, the ResultSort of E #) )
A1: dom the Sorts of A = the carrier of S by PARTFUN1:def_2;
assume A2: A is MSAlgebra over E ; ::_thesis: ManySortedSign(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S #) = ManySortedSign(# the carrier of E, the carrier' of E, the Arity of E, the ResultSort of E #)
then reconsider B = A as MSAlgebra over E ;
A3: the carrier of S = the carrier of E by A2, Th60;
A4: now__::_thesis:_for_x_being_set_st_x_in_the_carrier'_of_S_holds_
the_ResultSort_of_S_._x_=_the_ResultSort_of_E_._x
let x be set ; ::_thesis: ( x in the carrier' of S implies the ResultSort of S . x = the ResultSort of E . x )
assume  x in the carrier' of S ; ::_thesis: the ResultSort of S . x = the ResultSort of E . x
then reconsider o = x as OperSymbol of S ;
reconsider e = o as OperSymbol of E by A2, Th60;
set p = the Element of Args (o,A);
 Den (e,B) = the Charact of B . e ;
then A5: rng (Den (o,A)) c= Result (e,B) by RELAT_1:def_19;
 (Den (o,A)) . the Element of Args (o,A) in rng (Den (o,A)) by FUNCT_2:4;
then  Result (o,A) meets Result (e,B) by A5, XBOOLE_0:3;
then  Result (o,A) = ( the Sorts of B * the ResultSort of E) . x by Th61
.= the Sorts of B . ( the ResultSort of E . e) by FUNCT_2:15 ;
then  the Sorts of A . ( the ResultSort of E . e) = the Sorts of A . ( the ResultSort of S . o) by FUNCT_2:15;
hence  the ResultSort of S . x = the ResultSort of E . x by A3, A1, FUNCT_1:def_4; ::_thesis: verum
end;
A6: now__::_thesis:_for_x_being_set_st_x_in_the_carrier'_of_S_holds_
the_Arity_of_S_._x_=_the_Arity_of_E_._x
let x be set ; ::_thesis: ( x in the carrier' of S implies the Arity of S . x = the Arity of E . x )
assume  x in the carrier' of S ; ::_thesis: the Arity of S . x = the Arity of E . x
then reconsider o = x as OperSymbol of S ;
reconsider e = o as OperSymbol of E by A2, Th60;
reconsider p = the Arity of E . e as Element of the carrier of E * ;
reconsider q = the Arity of S . o as Element of the carrier of S * ;
 Den (e,B) = the Charact of B . e ;
then A7: dom (Den (o,A)) = Args (e,B) by FUNCT_2:def_1;
 dom (Den (o,A)) = Args (o,A) by FUNCT_2:def_1;
then  Args (o,A) = ( the Sorts of B #) . p by A7, FUNCT_2:15
.= product ( the Sorts of B * p) by FINSEQ_2:def_5 ;
then  product ( the Sorts of A * p) = ( the Sorts of A #) . q by FUNCT_2:15
.= product ( the Sorts of A * q) by FINSEQ_2:def_5 ;
then A8: the Sorts of B * p = the Sorts of A * q by PUA2MSS1:2;
A9: rng q c= the carrier of S ;
then A10: dom ( the Sorts of A * q) = dom q by A1, RELAT_1:27;
A11: rng p c= the carrier of E ;
then  dom ( the Sorts of B * p) = dom p by A3, A1, RELAT_1:27;
hence  the Arity of S . x = the Arity of E . x by A3, A1, A8, A11, A9, A10, FUNCT_1:27; ::_thesis: verum
end;
A12: dom the Arity of E = the carrier' of E by FUNCT_2:def_1;
A13: dom the Arity of S = the carrier' of S by FUNCT_2:def_1;
A14: dom the ResultSort of E = the carrier' of E by FUNCT_2:def_1;
A15: the carrier' of S = the carrier' of E by A2, Th60;
 dom the ResultSort of S = the carrier' of S by FUNCT_2:def_1;
then  the ResultSort of S = the ResultSort of E by A2, A14, A4, Th60, FUNCT_1:2;
hence  ManySortedSign(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S #) = ManySortedSign(# the carrier of E, the carrier' of E, the Arity of E, the ResultSort of E #) by A3, A15, A13, A12, A6, FUNCT_1:2; ::_thesis: verum
end;

theorem :: ALGSPEC1:63
for S, S9 being non void Signature
for A being non-empty disjoint_valued MSAlgebra over S st A is Algebra of S9 holds
S is Extension of S9
proof
let S, S9 be non void Signature; ::_thesis: for A being non-empty disjoint_valued MSAlgebra over S st A is Algebra of S9 holds
S is Extension of S9
let A be non-empty disjoint_valued MSAlgebra over S; ::_thesis: ( A is Algebra of S9 implies S is Extension of S9 )
assume  A is Algebra of S9 ; ::_thesis: S is Extension of S9
then consider E being non void Extension of S9 such that
A1: A is feasible MSAlgebra over E by Def7;
A2: S9 is Subsignature of E by Def5;
A3: ManySortedSign(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S #) = ManySortedSign(# the carrier of E, the carrier' of E, the Arity of E, the ResultSort of E #) by A1, Th62;
then A4: the ResultSort of S9 c= the ResultSort of S by A2, INSTALG1:11;
 the Arity of S9 c= the Arity of S by A2, A3, INSTALG1:11;
hence  S9 is Subsignature of S by A2, A3, A4, INSTALG1:10, INSTALG1:13; :: according to ALGSPEC1:def_5 ::_thesis: verum
end;