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