:: EXTENS_1 semantic presentation begin Lm1: for I being set for A, B, C being ManySortedSet of I for F being ManySortedFunction of A,B for G being ManySortedFunction of B,C holds G ** F is ManySortedSet of I proof let I be set ; ::_thesis: for A, B, C being ManySortedSet of I for F being ManySortedFunction of A,B for G being ManySortedFunction of B,C holds G ** F is ManySortedSet of I let A, B, C be ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,B for G being ManySortedFunction of B,C holds G ** F is ManySortedSet of I let F be ManySortedFunction of A,B; ::_thesis: for G being ManySortedFunction of B,C holds G ** F is ManySortedSet of I let G be ManySortedFunction of B,C; ::_thesis: G ** F is ManySortedSet of I dom (G ** F) = (dom F) /\ (dom G) by PBOOLE:def_19 .= I /\ (dom G) by PARTFUN1:def_2 .= I /\ I by PARTFUN1:def_2 .= I ; hence G ** F is ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18; ::_thesis: verum end; begin theorem :: EXTENS_1:1 for I being set for A being ManySortedSet of I for B being V2() ManySortedSet of I for F being ManySortedFunction of A,B for X being ManySortedSubset of A st A c= X holds F || X = F proof let I be set ; ::_thesis: for A being ManySortedSet of I for B being V2() ManySortedSet of I for F being ManySortedFunction of A,B for X being ManySortedSubset of A st A c= X holds F || X = F let A be ManySortedSet of I; ::_thesis: for B being V2() ManySortedSet of I for F being ManySortedFunction of A,B for X being ManySortedSubset of A st A c= X holds F || X = F let B be V2() ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,B for X being ManySortedSubset of A st A c= X holds F || X = F let F be ManySortedFunction of A,B; ::_thesis: for X being ManySortedSubset of A st A c= X holds F || X = F let X be ManySortedSubset of A; ::_thesis: ( A c= X implies F || X = F ) assume A1: A c= X ; ::_thesis: F || X = F now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (F_||_X)_._i_=_F_._i let i be set ; ::_thesis: ( i in I implies (F || X) . i = F . i ) assume A2: i in I ; ::_thesis: (F || X) . i = F . i then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def_15; A3: A . i c= X . i by A1, A2, PBOOLE:def_2; thus (F || X) . i = f | (X . i) by A2, MSAFREE:def_1 .= F . i by A3, RELSET_1:19 ; ::_thesis: verum end; hence F || X = F by PBOOLE:3; ::_thesis: verum end; theorem :: EXTENS_1:2 for I being set for A, B being ManySortedSet of I for M being ManySortedSubset of A for F being ManySortedFunction of A,B holds F .:.: M c= F .:.: A proof let I be set ; ::_thesis: for A, B being ManySortedSet of I for M being ManySortedSubset of A for F being ManySortedFunction of A,B holds F .:.: M c= F .:.: A let A, B be ManySortedSet of I; ::_thesis: for M being ManySortedSubset of A for F being ManySortedFunction of A,B holds F .:.: M c= F .:.: A let M be ManySortedSubset of A; ::_thesis: for F being ManySortedFunction of A,B holds F .:.: M c= F .:.: A let F be ManySortedFunction of A,B; ::_thesis: F .:.: M c= F .:.: A let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (F .:.: M) . i c= (F .:.: A) . i ) assume A1: i in I ; ::_thesis: (F .:.: M) . i c= (F .:.: A) . i reconsider f = F . i as Function of (A . i),(B . i) by A1, PBOOLE:def_15; A2: (F .:.: M) . i = f .: (M . i) by A1, PBOOLE:def_20; M c= A by PBOOLE:def_18; then M . i c= A . i by A1, PBOOLE:def_2; then A3: f .: (M . i) c= f .: (A . i) by RELAT_1:123; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (F .:.: M) . i or x in (F .:.: A) . i ) assume x in (F .:.: M) . i ; ::_thesis: x in (F .:.: A) . i then x in f .: (A . i) by A2, A3; hence x in (F .:.: A) . i by A1, PBOOLE:def_20; ::_thesis: verum end; theorem :: EXTENS_1:3 for I being set for A being ManySortedSet of I for B being V2() ManySortedSet of I for F being ManySortedFunction of A,B for M1, M2 being ManySortedSubset of A st M1 c= M2 holds (F || M2) .:.: M1 = F .:.: M1 proof let I be set ; ::_thesis: for A being ManySortedSet of I for B being V2() ManySortedSet of I for F being ManySortedFunction of A,B for M1, M2 being ManySortedSubset of A st M1 c= M2 holds (F || M2) .:.: M1 = F .:.: M1 let A be ManySortedSet of I; ::_thesis: for B being V2() ManySortedSet of I for F being ManySortedFunction of A,B for M1, M2 being ManySortedSubset of A st M1 c= M2 holds (F || M2) .:.: M1 = F .:.: M1 let B be V2() ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,B for M1, M2 being ManySortedSubset of A st M1 c= M2 holds (F || M2) .:.: M1 = F .:.: M1 let F be ManySortedFunction of A,B; ::_thesis: for M1, M2 being ManySortedSubset of A st M1 c= M2 holds (F || M2) .:.: M1 = F .:.: M1 let M1, M2 be ManySortedSubset of A; ::_thesis: ( M1 c= M2 implies (F || M2) .:.: M1 = F .:.: M1 ) assume A1: M1 c= M2 ; ::_thesis: (F || M2) .:.: M1 = F .:.: M1 now__::_thesis:_for_i_being_set_st_i_in_I_holds_ ((F_||_M2)_.:.:_M1)_._i_=_(F_.:.:_M1)_._i let i be set ; ::_thesis: ( i in I implies ((F || M2) .:.: M1) . i = (F .:.: M1) . i ) assume A2: i in I ; ::_thesis: ((F || M2) .:.: M1) . i = (F .:.: M1) . i then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def_15; reconsider fm = (F || M2) . i as Function of (M2 . i),(B . i) by A2, PBOOLE:def_15; A3: M1 . i c= M2 . i by A1, A2, PBOOLE:def_2; fm = f | (M2 . i) by A2, MSAFREE:def_1; hence ((F || M2) .:.: M1) . i = (f | (M2 . i)) .: (M1 . i) by A2, PBOOLE:def_20 .= f .: (M1 . i) by A3, RELAT_1:129 .= (F .:.: M1) . i by A2, PBOOLE:def_20 ; ::_thesis: verum end; hence (F || M2) .:.: M1 = F .:.: M1 by PBOOLE:3; ::_thesis: verum end; theorem Th4: :: EXTENS_1:4 for I being set for A being ManySortedSet of I for B, C being V2() ManySortedSet of I for F being ManySortedFunction of A,B for G being ManySortedFunction of B,C for X being ManySortedSubset of A holds (G ** F) || X = G ** (F || X) proof let I be set ; ::_thesis: for A being ManySortedSet of I for B, C being V2() ManySortedSet of I for F being ManySortedFunction of A,B for G being ManySortedFunction of B,C for X being ManySortedSubset of A holds (G ** F) || X = G ** (F || X) let A be ManySortedSet of I; ::_thesis: for B, C being V2() ManySortedSet of I for F being ManySortedFunction of A,B for G being ManySortedFunction of B,C for X being ManySortedSubset of A holds (G ** F) || X = G ** (F || X) let B, C be V2() ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,B for G being ManySortedFunction of B,C for X being ManySortedSubset of A holds (G ** F) || X = G ** (F || X) let F be ManySortedFunction of A,B; ::_thesis: for G being ManySortedFunction of B,C for X being ManySortedSubset of A holds (G ** F) || X = G ** (F || X) let G be ManySortedFunction of B,C; ::_thesis: for X being ManySortedSubset of A holds (G ** F) || X = G ** (F || X) let X be ManySortedSubset of A; ::_thesis: (G ** F) || X = G ** (F || X) now__::_thesis:_for_i_being_set_st_i_in_I_holds_ ((G_**_F)_||_X)_._i_=_(G_**_(F_||_X))_._i let i be set ; ::_thesis: ( i in I implies ((G ** F) || X) . i = (G ** (F || X)) . i ) assume A1: i in I ; ::_thesis: ((G ** F) || X) . i = (G ** (F || X)) . i then reconsider gf = (G ** F) . i as Function of (A . i),(C . i) by PBOOLE:def_15; reconsider fx = (F || X) . i as Function of (X . i),(B . i) by A1, PBOOLE:def_15; reconsider g = G . i as Function of (B . i),(C . i) by A1, PBOOLE:def_15; reconsider f = F . i as Function of (A . i),(B . i) by A1, PBOOLE:def_15; thus ((G ** F) || X) . i = gf | (X . i) by A1, MSAFREE:def_1 .= (g * f) | (X . i) by A1, MSUALG_3:2 .= g * (f | (X . i)) by RELAT_1:83 .= g * fx by A1, MSAFREE:def_1 .= (G ** (F || X)) . i by A1, MSUALG_3:2 ; ::_thesis: verum end; hence (G ** F) || X = G ** (F || X) by PBOOLE:3; ::_thesis: verum end; theorem :: EXTENS_1:5 for I being set for A, B being ManySortedSet of I st A is_transformable_to B holds for F being ManySortedFunction of A,B for C being ManySortedSet of I st B is ManySortedSubset of C holds F is ManySortedFunction of A,C proof let I be set ; ::_thesis: for A, B being ManySortedSet of I st A is_transformable_to B holds for F being ManySortedFunction of A,B for C being ManySortedSet of I st B is ManySortedSubset of C holds F is ManySortedFunction of A,C let A, B be ManySortedSet of I; ::_thesis: ( A is_transformable_to B implies for F being ManySortedFunction of A,B for C being ManySortedSet of I st B is ManySortedSubset of C holds F is ManySortedFunction of A,C ) assume A1: A is_transformable_to B ; ::_thesis: for F being ManySortedFunction of A,B for C being ManySortedSet of I st B is ManySortedSubset of C holds F is ManySortedFunction of A,C let F be ManySortedFunction of A,B; ::_thesis: for C being ManySortedSet of I st B is ManySortedSubset of C holds F is ManySortedFunction of A,C let C be ManySortedSet of I; ::_thesis: ( B is ManySortedSubset of C implies F is ManySortedFunction of A,C ) assume B is ManySortedSubset of C ; ::_thesis: F is ManySortedFunction of A,C then A2: B c= C by PBOOLE:def_18; let i be set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in I or F . i is Element of K19(K20((A . i),(C . i))) ) assume A3: i in I ; ::_thesis: F . i is Element of K19(K20((A . i),(C . i))) A4: ( B . i = {} implies A . i = {} ) by A1, A3, PZFMISC1:def_3; A5: F . i is Function of (A . i),(B . i) by A3, PBOOLE:def_15; B . i c= C . i by A3, A2, PBOOLE:def_2; hence F . i is Element of K19(K20((A . i),(C . i))) by A4, A5, FUNCT_2:7; ::_thesis: verum end; theorem :: EXTENS_1:6 for I being set for A being ManySortedSet of I for B being V2() ManySortedSet of I for F being ManySortedFunction of A,B for X being ManySortedSubset of A st F is "1-1" holds F || X is "1-1" proof let I be set ; ::_thesis: for A being ManySortedSet of I for B being V2() ManySortedSet of I for F being ManySortedFunction of A,B for X being ManySortedSubset of A st F is "1-1" holds F || X is "1-1" let A be ManySortedSet of I; ::_thesis: for B being V2() ManySortedSet of I for F being ManySortedFunction of A,B for X being ManySortedSubset of A st F is "1-1" holds F || X is "1-1" let B be V2() ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,B for X being ManySortedSubset of A st F is "1-1" holds F || X is "1-1" let F be ManySortedFunction of A,B; ::_thesis: for X being ManySortedSubset of A st F is "1-1" holds F || X is "1-1" let X be ManySortedSubset of A; ::_thesis: ( F is "1-1" implies F || X is "1-1" ) assume A1: F is "1-1" ; ::_thesis: F || X is "1-1" now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (F_||_X)_._i_is_one-to-one let i be set ; ::_thesis: ( i in I implies (F || X) . i is one-to-one ) assume A2: i in I ; ::_thesis: (F || X) . i is one-to-one then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def_15; f is one-to-one by A1, A2, MSUALG_3:1; then f | (X . i) is one-to-one by FUNCT_1:52; hence (F || X) . i is one-to-one by A2, MSAFREE:def_1; ::_thesis: verum end; hence F || X is "1-1" by MSUALG_3:1; ::_thesis: verum end; begin theorem :: EXTENS_1:7 for I being set for A being ManySortedSet of I for B being V2() ManySortedSet of I for F being ManySortedFunction of A,B for X being ManySortedSubset of A holds doms (F || X) c= doms F proof let I be set ; ::_thesis: for A being ManySortedSet of I for B being V2() ManySortedSet of I for F being ManySortedFunction of A,B for X being ManySortedSubset of A holds doms (F || X) c= doms F let A be ManySortedSet of I; ::_thesis: for B being V2() ManySortedSet of I for F being ManySortedFunction of A,B for X being ManySortedSubset of A holds doms (F || X) c= doms F let B be V2() ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,B for X being ManySortedSubset of A holds doms (F || X) c= doms F let F be ManySortedFunction of A,B; ::_thesis: for X being ManySortedSubset of A holds doms (F || X) c= doms F let X be ManySortedSubset of A; ::_thesis: doms (F || X) c= doms F let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (doms (F || X)) . i c= (doms F) . i ) A1: dom (F || X) = I by PARTFUN1:def_2; assume A2: i in I ; ::_thesis: (doms (F || X)) . i c= (doms F) . i then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def_15; dom F = I by PARTFUN1:def_2; then A3: (doms F) . i = dom f by A2, FUNCT_6:22; (F || X) . i = f | (X . i) by A2, MSAFREE:def_1; then (doms (F || X)) . i = dom (f | (X . i)) by A2, A1, FUNCT_6:22; hence (doms (F || X)) . i c= (doms F) . i by A3, RELAT_1:60; ::_thesis: verum end; theorem :: EXTENS_1:8 for I being set for A being ManySortedSet of I for B being V2() ManySortedSet of I for F being ManySortedFunction of A,B for X being ManySortedSubset of A holds rngs (F || X) c= rngs F proof let I be set ; ::_thesis: for A being ManySortedSet of I for B being V2() ManySortedSet of I for F being ManySortedFunction of A,B for X being ManySortedSubset of A holds rngs (F || X) c= rngs F let A be ManySortedSet of I; ::_thesis: for B being V2() ManySortedSet of I for F being ManySortedFunction of A,B for X being ManySortedSubset of A holds rngs (F || X) c= rngs F let B be V2() ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,B for X being ManySortedSubset of A holds rngs (F || X) c= rngs F let F be ManySortedFunction of A,B; ::_thesis: for X being ManySortedSubset of A holds rngs (F || X) c= rngs F let X be ManySortedSubset of A; ::_thesis: rngs (F || X) c= rngs F let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (rngs (F || X)) . i c= (rngs F) . i ) A1: dom (F || X) = I by PARTFUN1:def_2; assume A2: i in I ; ::_thesis: (rngs (F || X)) . i c= (rngs F) . i then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def_15; dom F = I by PARTFUN1:def_2; then A3: (rngs F) . i = rng f by A2, FUNCT_6:22; (F || X) . i = f | (X . i) by A2, MSAFREE:def_1; then (rngs (F || X)) . i = rng (f | (X . i)) by A2, A1, FUNCT_6:22; hence (rngs (F || X)) . i c= (rngs F) . i by A3, RELAT_1:70; ::_thesis: verum end; theorem :: EXTENS_1:9 for I being set for A, B being ManySortedSet of I for F being ManySortedFunction of A,B holds ( F is "onto" iff rngs F = B ) proof let I be set ; ::_thesis: for A, B being ManySortedSet of I for F being ManySortedFunction of A,B holds ( F is "onto" iff rngs F = B ) let A, B be ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,B holds ( F is "onto" iff rngs F = B ) let F be ManySortedFunction of A,B; ::_thesis: ( F is "onto" iff rngs F = B ) A1: dom F = I by PARTFUN1:def_2; thus ( F is "onto" implies rngs F = B ) ::_thesis: ( rngs F = B implies F is "onto" ) proof assume A2: F is "onto" ; ::_thesis: rngs F = B now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (rngs_F)_._i_=_B_._i let i be set ; ::_thesis: ( i in I implies (rngs F) . i = B . i ) assume A3: i in I ; ::_thesis: (rngs F) . i = B . i then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def_15; rng f = B . i by A2, A3, MSUALG_3:def_3; hence (rngs F) . i = B . i by A1, A3, FUNCT_6:22; ::_thesis: verum end; hence rngs F = B by PBOOLE:3; ::_thesis: verum end; assume A4: rngs F = B ; ::_thesis: F is "onto" let i be set ; :: according to MSUALG_3:def_3 ::_thesis: ( not i in I or rng (F . i) = B . i ) assume i in I ; ::_thesis: rng (F . i) = B . i hence rng (F . i) = B . i by A1, A4, FUNCT_6:22; ::_thesis: verum end; theorem :: EXTENS_1:10 for S being non empty non void ManySortedSign for X being V2() ManySortedSet of the carrier of S holds rngs (Reverse X) = X proof let S be non empty non void ManySortedSign ; ::_thesis: for X being V2() ManySortedSet of the carrier of S holds rngs (Reverse X) = X let X be V2() ManySortedSet of the carrier of S; ::_thesis: rngs (Reverse X) = X set I = the carrier of S; set R = Reverse X; now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_ (rngs_(Reverse_X))_._i_=_X_._i let i be set ; ::_thesis: ( i in the carrier of S implies (rngs (Reverse X)) . i = X . i ) assume A1: i in the carrier of S ; ::_thesis: (rngs (Reverse X)) . i = X . i reconsider r = (Reverse X) . i as Function of ((FreeGen X) . i),(X . i) by A1, PBOOLE:def_15; A2: dom (Reverse X) = the carrier of S by PARTFUN1:def_2; thus (rngs (Reverse X)) . i = X . i ::_thesis: verum proof reconsider s0 = i as SortSymbol of S by A1; set D = DTConMSA X; thus (rngs (Reverse X)) . i c= X . i :: according to XBOOLE_0:def_10 ::_thesis: X . i c= (rngs (Reverse X)) . i proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (rngs (Reverse X)) . i or x in X . i ) assume x in (rngs (Reverse X)) . i ; ::_thesis: x in X . i then A3: x in rng r by A1, A2, FUNCT_6:22; rng r c= X . i by RELAT_1:def_19; hence x in X . i by A3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X . i or x in (rngs (Reverse X)) . i ) assume x in X . i ; ::_thesis: x in (rngs (Reverse X)) . i then A4: [x,s0] in Terminals (DTConMSA X) by MSAFREE:7; then reconsider t = [x,s0] as Symbol of (DTConMSA X) ; t `2 = s0 by MCART_1:7; then root-tree t in { (root-tree tt) where tt is Symbol of (DTConMSA X) : ( tt in Terminals (DTConMSA X) & tt `2 = s0 ) } by A4; then A5: root-tree t in FreeGen (s0,X) by MSAFREE:13; A6: (Reverse X) . s0 = Reverse (s0,X) by MSAFREE:def_18; then A7: ((Reverse X) . s0) . (root-tree t) = t `1 by A5, MSAFREE:def_17 .= x by MCART_1:7 ; dom ((Reverse X) . s0) = FreeGen (s0,X) by A6, FUNCT_2:def_1; then ((Reverse X) . s0) . (root-tree t) in rng ((Reverse X) . s0) by A5, FUNCT_1:def_3; hence x in (rngs (Reverse X)) . i by A2, A7, FUNCT_6:22; ::_thesis: verum end; end; hence rngs (Reverse X) = X by PBOOLE:3; ::_thesis: verum end; theorem :: EXTENS_1:11 for I being set for A being ManySortedSet of I for B, C being V2() ManySortedSet of I for F being ManySortedFunction of A,B for G being ManySortedFunction of B,C for X being V2() ManySortedSubset of B st rngs F c= X holds (G || X) ** F = G ** F proof let I be set ; ::_thesis: for A being ManySortedSet of I for B, C being V2() ManySortedSet of I for F being ManySortedFunction of A,B for G being ManySortedFunction of B,C for X being V2() ManySortedSubset of B st rngs F c= X holds (G || X) ** F = G ** F let A be ManySortedSet of I; ::_thesis: for B, C being V2() ManySortedSet of I for F being ManySortedFunction of A,B for G being ManySortedFunction of B,C for X being V2() ManySortedSubset of B st rngs F c= X holds (G || X) ** F = G ** F let B, C be V2() ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,B for G being ManySortedFunction of B,C for X being V2() ManySortedSubset of B st rngs F c= X holds (G || X) ** F = G ** F let F be ManySortedFunction of A,B; ::_thesis: for G being ManySortedFunction of B,C for X being V2() ManySortedSubset of B st rngs F c= X holds (G || X) ** F = G ** F let G be ManySortedFunction of B,C; ::_thesis: for X being V2() ManySortedSubset of B st rngs F c= X holds (G || X) ** F = G ** F let X be V2() ManySortedSubset of B; ::_thesis: ( rngs F c= X implies (G || X) ** F = G ** F ) assume A1: rngs F c= X ; ::_thesis: (G || X) ** F = G ** F A2: dom F = I by PARTFUN1:def_2; A3: F is ManySortedFunction of A,X proof let i be set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in I or F . i is Element of K19(K20((A . i),(X . i))) ) assume A4: i in I ; ::_thesis: F . i is Element of K19(K20((A . i),(X . i))) then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def_15; A5: (rngs F) . i c= X . i by A1, A4, PBOOLE:def_2; ( dom f = A . i & (rngs F) . i = rng f ) by A2, A4, FUNCT_2:def_1, FUNCT_6:22; hence F . i is Element of K19(K20((A . i),(X . i))) by A4, A5, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum end; A6: now__::_thesis:_for_i_being_set_st_i_in_I_holds_ ((G_||_X)_**_F)_._i_=_(G_**_F)_._i let i be set ; ::_thesis: ( i in I implies ((G || X) ** F) . i = (G ** F) . i ) assume A7: i in I ; ::_thesis: ((G || X) ** F) . i = (G ** F) . i then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def_15; (rngs F) . i = rng f by A2, A7, FUNCT_6:22; then A8: rng f c= X . i by A1, A7, PBOOLE:def_2; dom f = A . i by A7, FUNCT_2:def_1; then reconsider f9 = f as Function of (A . i),(X . i) by A7, A8, FUNCT_2:def_1, RELSET_1:4; reconsider g = G . i as Function of (B . i),(C . i) by A7, PBOOLE:def_15; A9: rng f9 c= X . i by RELAT_1:def_19; reconsider gx = (G || X) . i as Function of (X . i),(C . i) by A7, PBOOLE:def_15; thus ((G || X) ** F) . i = gx * f9 by A3, A7, MSUALG_3:2 .= (g | (X . i)) * f by A7, MSAFREE:def_1 .= g * f9 by A9, MSUHOM_1:1 .= (G ** F) . i by A7, MSUALG_3:2 ; ::_thesis: verum end; (G || X) ** F is ManySortedSet of I by A3, Lm1; hence (G || X) ** F = G ** F by A6, PBOOLE:3; ::_thesis: verum end; begin theorem Th12: :: EXTENS_1:12 for I being set for A being ManySortedSet of I for B being V2() ManySortedSet of I for F being ManySortedFunction of A,B holds ( F is "onto" iff for C being V2() ManySortedSet of I for G, H being ManySortedFunction of B,C st G ** F = H ** F holds G = H ) proof let I be set ; ::_thesis: for A being ManySortedSet of I for B being V2() ManySortedSet of I for F being ManySortedFunction of A,B holds ( F is "onto" iff for C being V2() ManySortedSet of I for G, H being ManySortedFunction of B,C st G ** F = H ** F holds G = H ) let A be ManySortedSet of I; ::_thesis: for B being V2() ManySortedSet of I for F being ManySortedFunction of A,B holds ( F is "onto" iff for C being V2() ManySortedSet of I for G, H being ManySortedFunction of B,C st G ** F = H ** F holds G = H ) let B be V2() ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,B holds ( F is "onto" iff for C being V2() ManySortedSet of I for G, H being ManySortedFunction of B,C st G ** F = H ** F holds G = H ) let F be ManySortedFunction of A,B; ::_thesis: ( F is "onto" iff for C being V2() ManySortedSet of I for G, H being ManySortedFunction of B,C st G ** F = H ** F holds G = H ) thus ( F is "onto" implies for C being V2() ManySortedSet of I for G, H being ManySortedFunction of B,C st G ** F = H ** F holds G = H ) ::_thesis: ( ( for C being V2() ManySortedSet of I for G, H being ManySortedFunction of B,C st G ** F = H ** F holds G = H ) implies F is "onto" ) proof assume A1: F is "onto" ; ::_thesis: for C being V2() ManySortedSet of I for G, H being ManySortedFunction of B,C st G ** F = H ** F holds G = H let C be V2() ManySortedSet of I; ::_thesis: for G, H being ManySortedFunction of B,C st G ** F = H ** F holds G = H let G, H be ManySortedFunction of B,C; ::_thesis: ( G ** F = H ** F implies G = H ) assume A2: G ** F = H ** F ; ::_thesis: G = H now__::_thesis:_for_i_being_set_st_i_in_I_holds_ G_._i_=_H_._i let i be set ; ::_thesis: ( i in I implies G . i = H . i ) assume A3: i in I ; ::_thesis: G . i = H . i then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def_15; reconsider h = H . i as Function of (B . i),(C . i) by A3, PBOOLE:def_15; reconsider g = G . i as Function of (B . i),(C . i) by A3, PBOOLE:def_15; A4: rng f = B . i by A1, A3, MSUALG_3:def_3; g * f = (H ** F) . i by A2, A3, MSUALG_3:2 .= h * f by A3, MSUALG_3:2 ; hence G . i = H . i by A3, A4, FUNCT_2:16; ::_thesis: verum end; hence G = H by PBOOLE:3; ::_thesis: verum end; assume that A5: for C being V2() ManySortedSet of I for G, H being ManySortedFunction of B,C st G ** F = H ** F holds G = H and A6: not F is "onto" ; ::_thesis: contradiction consider j being set such that A7: j in I and A8: rng (F . j) <> B . j by A6, MSUALG_3:def_3; reconsider I = I as non empty set by A7; reconsider j = j as Element of I by A7; reconsider A = A, B = B as ManySortedSet of I ; reconsider F = F as ManySortedFunction of A,B ; reconsider f = F . j as Function of (A . j),(B . j) ; consider Z being set such that A9: Z <> {} and A10: ex g, h being Function of (B . j),Z st ( g * f = h * f & g <> h ) by A8, FUNCT_2:16; consider g, h being Function of (B . j),Z such that A11: g * (F . j) = h * (F . j) and A12: g <> h by A10; ex C being ManySortedSet of I st ( C is V2() & ex G, H being ManySortedFunction of B,C st ( G ** F = H ** F & G <> H ) ) proof deffunc H1( set ) -> set = IFEQ (\$1,j,Z,(B . \$1)); consider C being ManySortedSet of I such that A13: for i being set st i in I holds C . i = H1(i) from PBOOLE:sch_4(); take C ; ::_thesis: ( C is V2() & ex G, H being ManySortedFunction of B,C st ( G ** F = H ** F & G <> H ) ) thus C is V2() ::_thesis: ex G, H being ManySortedFunction of B,C st ( G ** F = H ** F & G <> H ) proof let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in I or not C . i is empty ) assume A14: i in I ; ::_thesis: not C . i is empty now__::_thesis:_(_(_i_=_j_&_not_C_._i_is_empty_)_or_(_i_<>_j_&_not_C_._i_is_empty_)_) percases ( i = j or i <> j ) ; case i = j ; ::_thesis: not C . i is empty then IFEQ (i,j,Z,(B . i)) = Z by FUNCOP_1:def_8; hence not C . i is empty by A9, A13, A14; ::_thesis: verum end; case i <> j ; ::_thesis: not C . i is empty then IFEQ (i,j,Z,(B . i)) = B . i by FUNCOP_1:def_8; hence not C . i is empty by A13, A14; ::_thesis: verum end; end; end; hence not C . i is empty ; ::_thesis: verum end; deffunc H2( set ) -> set = IFEQ (\$1,j,g,((id B) . \$1)); consider G being ManySortedSet of I such that A15: for i being set st i in I holds G . i = H2(i) from PBOOLE:sch_4(); deffunc H3( set ) -> set = IFEQ (\$1,j,h,((id B) . \$1)); consider H being ManySortedSet of I such that A16: for i being set st i in I holds H . i = H3(i) from PBOOLE:sch_4(); now__::_thesis:_for_G_being_ManySortedSet_of_I for_g,_h_being_Function_of_(B_._j),Z_st_g_*_(F_._j)_=_h_*_(F_._j)_&_g_<>_h_&_(_for_i_being_set_st_i_in_I_holds_ G_._i_=_IFEQ_(i,j,g,((id_B)_._i))_)_holds_ G_is_Function-yielding let G be ManySortedSet of I; ::_thesis: for g, h being Function of (B . j),Z st g * (F . j) = h * (F . j) & g <> h & ( for i being set st i in I holds G . i = IFEQ (i,j,g,((id B) . i)) ) holds G is Function-yielding let g, h be Function of (B . j),Z; ::_thesis: ( g * (F . j) = h * (F . j) & g <> h & ( for i being set st i in I holds G . i = IFEQ (i,j,g,((id B) . i)) ) implies G is Function-yielding ) assume that g * (F . j) = h * (F . j) and g <> h and A17: for i being set st i in I holds G . i = IFEQ (i,j,g,((id B) . i)) ; ::_thesis: G is Function-yielding thus G is Function-yielding ::_thesis: verum proof let i be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( not i in dom G or G . i is set ) assume i in dom G ; ::_thesis: G . i is set then A18: i in I ; now__::_thesis:_(_(_i_=_j_&_G_._i_is_set_)_or_(_i_<>_j_&_G_._i_is_set_)_) percases ( i = j or i <> j ) ; case i = j ; ::_thesis: G . i is set then IFEQ (i,j,g,((id B) . i)) = g by FUNCOP_1:def_8; hence G . i is set by A17, A18; ::_thesis: verum end; case i <> j ; ::_thesis: G . i is set then IFEQ (i,j,g,((id B) . i)) = (id B) . i by FUNCOP_1:def_8; hence G . i is set by A17, A18; ::_thesis: verum end; end; end; hence G . i is set ; ::_thesis: verum end; end; then reconsider G = G, H = H as ManySortedFunction of I by A11, A12, A15, A16; now__::_thesis:_for_G_being_ManySortedFunction_of_I for_g,_h_being_Function_of_(B_._j),Z_st_g_*_(F_._j)_=_h_*_(F_._j)_&_g_<>_h_&_(_for_i_being_set_st_i_in_I_holds_ G_._i_=_IFEQ_(i,j,g,((id_B)_._i))_)_holds_ G_is_ManySortedFunction_of_B,C let G be ManySortedFunction of I; ::_thesis: for g, h being Function of (B . j),Z st g * (F . j) = h * (F . j) & g <> h & ( for i being set st i in I holds G . i = IFEQ (i,j,g,((id B) . i)) ) holds G is ManySortedFunction of B,C let g, h be Function of (B . j),Z; ::_thesis: ( g * (F . j) = h * (F . j) & g <> h & ( for i being set st i in I holds G . i = IFEQ (i,j,g,((id B) . i)) ) implies G is ManySortedFunction of B,C ) assume that g * (F . j) = h * (F . j) and g <> h and A19: for i being set st i in I holds G . i = IFEQ (i,j,g,((id B) . i)) ; ::_thesis: G is ManySortedFunction of B,C thus G is ManySortedFunction of B,C ::_thesis: verum proof let i be set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in I or G . i is Element of K19(K20((B . i),(C . i))) ) assume A20: i in I ; ::_thesis: G . i is Element of K19(K20((B . i),(C . i))) now__::_thesis:_(_(_i_=_j_&_G_._i_is_Element_of_K19(K20((B_._i),(C_._i)))_)_or_(_i_<>_j_&_G_._i_is_Element_of_K19(K20((B_._i),(C_._i)))_)_) percases ( i = j or i <> j ) ; caseA21: i = j ; ::_thesis: G . i is Element of K19(K20((B . i),(C . i))) then A22: IFEQ (i,j,Z,(B . i)) = Z by FUNCOP_1:def_8; ( IFEQ (i,j,g,((id B) . i)) = g & C . i = IFEQ (i,j,Z,(B . i)) ) by A13, A21, FUNCOP_1:def_8; hence G . i is Element of K19(K20((B . i),(C . i))) by A19, A21, A22; ::_thesis: verum end; caseA23: i <> j ; ::_thesis: G . i is Element of K19(K20((B . i),(C . i))) then IFEQ (i,j,Z,(B . i)) = B . i by FUNCOP_1:def_8; then A24: B . i = C . i by A13, A20; IFEQ (i,j,g,((id B) . i)) = (id B) . i by A23, FUNCOP_1:def_8; then G . i = (id B) . i by A19, A20; hence G . i is Element of K19(K20((B . i),(C . i))) by A20, A24, PBOOLE:def_15; ::_thesis: verum end; end; end; hence G . i is Element of K19(K20((B . i),(C . i))) ; ::_thesis: verum end; end; then reconsider G = G, H = H as ManySortedFunction of B,C by A11, A12, A15, A16; A25: now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (G_**_F)_._i_=_(H_**_F)_._i let i be set ; ::_thesis: ( i in I implies (G ** F) . i = (H ** F) . i ) assume A26: i in I ; ::_thesis: (G ** F) . i = (H ** F) . i now__::_thesis:_(_(_i_=_j_&_(G_**_F)_._i_=_(H_**_F)_._i_)_or_(_i_<>_j_&_(G_**_F)_._i_=_(H_**_F)_._i_)_) percases ( i = j or i <> j ) ; caseA27: i = j ; ::_thesis: (G ** F) . i = (H ** F) . i then IFEQ (i,j,h,((id B) . i)) = h by FUNCOP_1:def_8; then A28: h = H . i by A16, A26; IFEQ (i,j,g,((id B) . i)) = g by A27, FUNCOP_1:def_8; then g = G . i by A15, A26; hence (G ** F) . i = h * (F . j) by A11, A27, MSUALG_3:2 .= (H ** F) . i by A27, A28, MSUALG_3:2 ; ::_thesis: verum end; caseA29: i <> j ; ::_thesis: (G ** F) . i = (H ** F) . i reconsider g9 = G . i as Function of (B . i),(C . i) by A26, PBOOLE:def_15; reconsider f9 = F . i as Function of (A . i),(B . i) by A26, PBOOLE:def_15; reconsider h9 = H . i as Function of (B . i),(C . i) by A26, PBOOLE:def_15; A30: IFEQ (i,j,h,((id B) . i)) = (id B) . i by A29, FUNCOP_1:def_8; IFEQ (i,j,g,((id B) . i)) = (id B) . i by A29, FUNCOP_1:def_8; then g9 = (id B) . i by A15, A26 .= h9 by A16, A26, A30 ; hence (G ** F) . i = h9 * f9 by A26, MSUALG_3:2 .= (H ** F) . i by A26, MSUALG_3:2 ; ::_thesis: verum end; end; end; hence (G ** F) . i = (H ** F) . i ; ::_thesis: verum end; take G ; ::_thesis: ex H being ManySortedFunction of B,C st ( G ** F = H ** F & G <> H ) take H ; ::_thesis: ( G ** F = H ** F & G <> H ) ( G ** F is ManySortedSet of I & H ** F is ManySortedSet of I ) by Lm1; hence G ** F = H ** F by A25, PBOOLE:3; ::_thesis: G <> H ex i being set st ( i in I & G . i <> H . i ) proof take i = j; ::_thesis: ( i in I & G . i <> H . i ) thus i in I ; ::_thesis: G . i <> H . i A31: h = IFEQ (i,j,h,((id B) . i)) by FUNCOP_1:def_8 .= H . i by A16 ; g = IFEQ (i,j,g,((id B) . i)) by FUNCOP_1:def_8 .= G . i by A15 ; hence G . i <> H . i by A12, A31; ::_thesis: verum end; hence G <> H ; ::_thesis: verum end; hence contradiction by A5; ::_thesis: verum end; theorem Th13: :: EXTENS_1:13 for I being set for A being ManySortedSet of I for B being V2() ManySortedSet of I for F being ManySortedFunction of A,B st A is V2() holds ( F is "1-1" iff for C being ManySortedSet of I for G, H being ManySortedFunction of C,A st F ** G = F ** H holds G = H ) proof let I be set ; ::_thesis: for A being ManySortedSet of I for B being V2() ManySortedSet of I for F being ManySortedFunction of A,B st A is V2() holds ( F is "1-1" iff for C being ManySortedSet of I for G, H being ManySortedFunction of C,A st F ** G = F ** H holds G = H ) let A be ManySortedSet of I; ::_thesis: for B being V2() ManySortedSet of I for F being ManySortedFunction of A,B st A is V2() holds ( F is "1-1" iff for C being ManySortedSet of I for G, H being ManySortedFunction of C,A st F ** G = F ** H holds G = H ) let B be V2() ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,B st A is V2() holds ( F is "1-1" iff for C being ManySortedSet of I for G, H being ManySortedFunction of C,A st F ** G = F ** H holds G = H ) let F be ManySortedFunction of A,B; ::_thesis: ( A is V2() implies ( F is "1-1" iff for C being ManySortedSet of I for G, H being ManySortedFunction of C,A st F ** G = F ** H holds G = H ) ) assume A1: A is V2() ; ::_thesis: ( F is "1-1" iff for C being ManySortedSet of I for G, H being ManySortedFunction of C,A st F ** G = F ** H holds G = H ) thus ( F is "1-1" implies for C being ManySortedSet of I for G, H being ManySortedFunction of C,A st F ** G = F ** H holds G = H ) ::_thesis: ( ( for C being ManySortedSet of I for G, H being ManySortedFunction of C,A st F ** G = F ** H holds G = H ) implies F is "1-1" ) proof assume A2: F is "1-1" ; ::_thesis: for C being ManySortedSet of I for G, H being ManySortedFunction of C,A st F ** G = F ** H holds G = H let C be ManySortedSet of I; ::_thesis: for G, H being ManySortedFunction of C,A st F ** G = F ** H holds G = H let G, H be ManySortedFunction of C,A; ::_thesis: ( F ** G = F ** H implies G = H ) assume A3: F ** G = F ** H ; ::_thesis: G = H now__::_thesis:_for_i_being_set_st_i_in_I_holds_ G_._i_=_H_._i let i be set ; ::_thesis: ( i in I implies G . i = H . i ) assume A4: i in I ; ::_thesis: G . i = H . i then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def_15; reconsider h = H . i as Function of (C . i),(A . i) by A4, PBOOLE:def_15; reconsider g = G . i as Function of (C . i),(A . i) by A4, PBOOLE:def_15; A5: f is one-to-one by A2, A4, MSUALG_3:1; f * g = (F ** H) . i by A3, A4, MSUALG_3:2 .= f * h by A4, MSUALG_3:2 ; hence G . i = H . i by A1, A4, A5, FUNCT_2:21; ::_thesis: verum end; hence G = H by PBOOLE:3; ::_thesis: verum end; assume that A6: for C being ManySortedSet of I for G, H being ManySortedFunction of C,A st F ** G = F ** H holds G = H and A7: not F is "1-1" ; ::_thesis: contradiction consider j being set such that A8: j in I and A9: not F . j is one-to-one by A7, MSUALG_3:1; F . j is Function of (A . j),(B . j) by A8, PBOOLE:def_15; then consider Z being set such that A10: ex g, h being Function of Z,(A . j) st ( (F . j) * g = (F . j) * h & g <> h ) by A1, A8, A9, FUNCT_2:21; consider g, h being Function of Z,(A . j) such that A11: (F . j) * g = (F . j) * h and A12: g <> h by A10; ex C being ManySortedSet of I ex G, H being ManySortedFunction of C,A st ( F ** G = F ** H & G <> H ) proof deffunc H1( set ) -> set = IFEQ (\$1,j,Z,(A . \$1)); consider C being ManySortedSet of I such that A13: for i being set st i in I holds C . i = H1(i) from PBOOLE:sch_4(); take C ; ::_thesis: ex G, H being ManySortedFunction of C,A st ( F ** G = F ** H & G <> H ) deffunc H2( set ) -> set = IFEQ (\$1,j,g,((id C) . \$1)); consider G being ManySortedSet of I such that A14: for i being set st i in I holds G . i = H2(i) from PBOOLE:sch_4(); deffunc H3( set ) -> set = IFEQ (\$1,j,h,((id C) . \$1)); consider H being ManySortedSet of I such that A15: for i being set st i in I holds H . i = H3(i) from PBOOLE:sch_4(); now__::_thesis:_for_G_being_ManySortedSet_of_I for_g,_h_being_Function_of_Z,(A_._j)_st_(F_._j)_*_g_=_(F_._j)_*_h_&_g_<>_h_&_(_for_i_being_set_st_i_in_I_holds_ G_._i_=_IFEQ_(i,j,g,((id_C)_._i))_)_holds_ G_is_Function-yielding let G be ManySortedSet of I; ::_thesis: for g, h being Function of Z,(A . j) st (F . j) * g = (F . j) * h & g <> h & ( for i being set st i in I holds G . i = IFEQ (i,j,g,((id C) . i)) ) holds G is Function-yielding let g, h be Function of Z,(A . j); ::_thesis: ( (F . j) * g = (F . j) * h & g <> h & ( for i being set st i in I holds G . i = IFEQ (i,j,g,((id C) . i)) ) implies G is Function-yielding ) assume that (F . j) * g = (F . j) * h and g <> h and A16: for i being set st i in I holds G . i = IFEQ (i,j,g,((id C) . i)) ; ::_thesis: G is Function-yielding thus G is Function-yielding ::_thesis: verum proof let i be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( not i in dom G or G . i is set ) assume i in dom G ; ::_thesis: G . i is set then A17: i in I ; now__::_thesis:_(_(_i_=_j_&_G_._i_is_set_)_or_(_i_<>_j_&_G_._i_is_set_)_) percases ( i = j or i <> j ) ; case i = j ; ::_thesis: G . i is set then IFEQ (i,j,g,((id C) . i)) = g by FUNCOP_1:def_8; hence G . i is set by A16, A17; ::_thesis: verum end; case i <> j ; ::_thesis: G . i is set then IFEQ (i,j,g,((id C) . i)) = (id C) . i by FUNCOP_1:def_8; hence G . i is set by A16, A17; ::_thesis: verum end; end; end; hence G . i is set ; ::_thesis: verum end; end; then reconsider G = G, H = H as ManySortedFunction of I by A11, A12, A14, A15; now__::_thesis:_for_G_being_ManySortedFunction_of_I for_g,_h_being_Function_of_Z,(A_._j)_st_(F_._j)_*_g_=_(F_._j)_*_h_&_g_<>_h_&_(_for_i_being_set_st_i_in_I_holds_ G_._i_=_IFEQ_(i,j,g,((id_C)_._i))_)_holds_ G_is_ManySortedFunction_of_C,A let G be ManySortedFunction of I; ::_thesis: for g, h being Function of Z,(A . j) st (F . j) * g = (F . j) * h & g <> h & ( for i being set st i in I holds G . i = IFEQ (i,j,g,((id C) . i)) ) holds G is ManySortedFunction of C,A let g, h be Function of Z,(A . j); ::_thesis: ( (F . j) * g = (F . j) * h & g <> h & ( for i being set st i in I holds G . i = IFEQ (i,j,g,((id C) . i)) ) implies G is ManySortedFunction of C,A ) assume that (F . j) * g = (F . j) * h and g <> h and A18: for i being set st i in I holds G . i = IFEQ (i,j,g,((id C) . i)) ; ::_thesis: G is ManySortedFunction of C,A thus G is ManySortedFunction of C,A ::_thesis: verum proof let i be set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in I or G . i is Element of K19(K20((C . i),(A . i))) ) assume A19: i in I ; ::_thesis: G . i is Element of K19(K20((C . i),(A . i))) now__::_thesis:_(_(_i_=_j_&_G_._i_is_Element_of_K19(K20((C_._i),(A_._i)))_)_or_(_i_<>_j_&_G_._i_is_Element_of_K19(K20((C_._i),(A_._i)))_)_) percases ( i = j or i <> j ) ; caseA20: i = j ; ::_thesis: G . i is Element of K19(K20((C . i),(A . i))) then A21: ( IFEQ (i,j,g,((id C) . i)) = g & IFEQ (i,j,Z,(A . i)) = Z ) by FUNCOP_1:def_8; C . i = IFEQ (i,j,Z,(A . i)) by A13, A19; hence G . i is Element of K19(K20((C . i),(A . i))) by A18, A19, A20, A21; ::_thesis: verum end; caseA22: i <> j ; ::_thesis: G . i is Element of K19(K20((C . i),(A . i))) then IFEQ (i,j,Z,(A . i)) = A . i by FUNCOP_1:def_8; then A23: C . i = A . i by A13, A19; IFEQ (i,j,g,((id C) . i)) = (id C) . i by A22, FUNCOP_1:def_8; then G . i = (id C) . i by A18, A19; hence G . i is Element of K19(K20((C . i),(A . i))) by A19, A23, PBOOLE:def_15; ::_thesis: verum end; end; end; hence G . i is Element of K19(K20((C . i),(A . i))) ; ::_thesis: verum end; end; then reconsider G = G, H = H as ManySortedFunction of C,A by A11, A12, A14, A15; A24: now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (F_**_G)_._i_=_(F_**_H)_._i let i be set ; ::_thesis: ( i in I implies (F ** G) . i = (F ** H) . i ) assume A25: i in I ; ::_thesis: (F ** G) . i = (F ** H) . i now__::_thesis:_(_(_i_=_j_&_(F_**_G)_._i_=_(F_**_H)_._i_)_or_(_i_<>_j_&_(F_**_G)_._i_=_(F_**_H)_._i_)_) percases ( i = j or i <> j ) ; caseA26: i = j ; ::_thesis: (F ** G) . i = (F ** H) . i then IFEQ (i,j,h,((id C) . i)) = h by FUNCOP_1:def_8; then A27: h = H . i by A15, A25; IFEQ (i,j,g,((id C) . i)) = g by A26, FUNCOP_1:def_8; then g = G . i by A14, A25; hence (F ** G) . i = (F . j) * h by A8, A11, A26, MSUALG_3:2 .= (F ** H) . i by A8, A26, A27, MSUALG_3:2 ; ::_thesis: verum end; caseA28: i <> j ; ::_thesis: (F ** G) . i = (F ** H) . i reconsider g9 = G . i as Function of (C . i),(A . i) by A25, PBOOLE:def_15; reconsider f9 = F . i as Function of (A . i),(B . i) by A25, PBOOLE:def_15; reconsider h9 = H . i as Function of (C . i),(A . i) by A25, PBOOLE:def_15; A29: IFEQ (i,j,h,((id C) . i)) = (id C) . i by A28, FUNCOP_1:def_8; IFEQ (i,j,g,((id C) . i)) = (id C) . i by A28, FUNCOP_1:def_8; then g9 = (id C) . i by A14, A25 .= h9 by A15, A25, A29 ; hence (F ** G) . i = f9 * h9 by A25, MSUALG_3:2 .= (F ** H) . i by A25, MSUALG_3:2 ; ::_thesis: verum end; end; end; hence (F ** G) . i = (F ** H) . i ; ::_thesis: verum end; take G ; ::_thesis: ex H being ManySortedFunction of C,A st ( F ** G = F ** H & G <> H ) take H ; ::_thesis: ( F ** G = F ** H & G <> H ) ( F ** G is ManySortedSet of I & F ** H is ManySortedSet of I ) by Lm1; hence F ** G = F ** H by A24, PBOOLE:3; ::_thesis: G <> H ex i being set st ( i in I & G . i <> H . i ) proof take i = j; ::_thesis: ( i in I & G . i <> H . i ) thus i in I by A8; ::_thesis: G . i <> H . i A30: h = IFEQ (i,j,h,((id C) . i)) by FUNCOP_1:def_8 .= H . i by A8, A15 ; g = IFEQ (i,j,g,((id C) . i)) by FUNCOP_1:def_8 .= G . i by A8, A14 ; hence G . i <> H . i by A12, A30; ::_thesis: verum end; hence G <> H ; ::_thesis: verum end; hence contradiction by A6; ::_thesis: verum end; begin theorem Th14: :: EXTENS_1:14 for S being non empty non void ManySortedSign for U1 being non-empty MSAlgebra over S for X being V2() ManySortedSet of the carrier of S for h1, h2 being ManySortedFunction of (FreeMSA X),U1 st h1 is_homomorphism FreeMSA X,U1 & h2 is_homomorphism FreeMSA X,U1 & h1 || (FreeGen X) = h2 || (FreeGen X) holds h1 = h2 proof let S be non empty non void ManySortedSign ; ::_thesis: for U1 being non-empty MSAlgebra over S for X being V2() ManySortedSet of the carrier of S for h1, h2 being ManySortedFunction of (FreeMSA X),U1 st h1 is_homomorphism FreeMSA X,U1 & h2 is_homomorphism FreeMSA X,U1 & h1 || (FreeGen X) = h2 || (FreeGen X) holds h1 = h2 let U1 be non-empty MSAlgebra over S; ::_thesis: for X being V2() ManySortedSet of the carrier of S for h1, h2 being ManySortedFunction of (FreeMSA X),U1 st h1 is_homomorphism FreeMSA X,U1 & h2 is_homomorphism FreeMSA X,U1 & h1 || (FreeGen X) = h2 || (FreeGen X) holds h1 = h2 let X be V2() ManySortedSet of the carrier of S; ::_thesis: for h1, h2 being ManySortedFunction of (FreeMSA X),U1 st h1 is_homomorphism FreeMSA X,U1 & h2 is_homomorphism FreeMSA X,U1 & h1 || (FreeGen X) = h2 || (FreeGen X) holds h1 = h2 let h1, h2 be ManySortedFunction of (FreeMSA X),U1; ::_thesis: ( h1 is_homomorphism FreeMSA X,U1 & h2 is_homomorphism FreeMSA X,U1 & h1 || (FreeGen X) = h2 || (FreeGen X) implies h1 = h2 ) assume that A1: h1 is_homomorphism FreeMSA X,U1 and A2: h2 is_homomorphism FreeMSA X,U1 and A3: h1 || (FreeGen X) = h2 || (FreeGen X) ; ::_thesis: h1 = h2 A4: h2 is_homomorphism FreeMSA X,U1 by A2; defpred S1[ SortSymbol of S, set , set ] means (h1 . \$1) . \$3 = \$2; A5: for s being SortSymbol of S for x, y being set st y in FreeGen (s,X) holds ( (h2 . s) . y = x iff S1[s,x,y] ) proof set FG = FreeGen X; let s be SortSymbol of S; ::_thesis: for x, y being set st y in FreeGen (s,X) holds ( (h2 . s) . y = x iff S1[s,x,y] ) let x, y be set ; ::_thesis: ( y in FreeGen (s,X) implies ( (h2 . s) . y = x iff S1[s,x,y] ) ) assume y in FreeGen (s,X) ; ::_thesis: ( (h2 . s) . y = x iff S1[s,x,y] ) then A6: y in (FreeGen X) . s by MSAFREE:def_16; A7: ( (h1 || (FreeGen X)) . s = (h1 . s) | ((FreeGen X) . s) & (h2 || (FreeGen X)) . s = (h2 . s) | ((FreeGen X) . s) ) by MSAFREE:def_1; ((h1 . s) | ((FreeGen X) . s)) . y = (h1 . s) . y by A6, FUNCT_1:49; hence ( (h2 . s) . y = x iff S1[s,x,y] ) by A3, A7, A6, FUNCT_1:49; ::_thesis: verum end; A8: for s being SortSymbol of S for x, y being set st y in FreeGen (s,X) holds ( (h1 . s) . y = x iff S1[s,x,y] ) ; A9: h1 is_homomorphism FreeMSA X,U1 by A1; thus h1 = h2 from MSAFREE1:sch_3(A9, A8, A4, A5); ::_thesis: verum end; theorem :: EXTENS_1:15 for S being non empty non void ManySortedSign for U1, U2 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 holds for U3 being non-empty MSAlgebra over S for h1, h2 being ManySortedFunction of U2,U3 st h1 ** F = h2 ** F holds h1 = h2 proof let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 holds for U3 being non-empty MSAlgebra over S for h1, h2 being ManySortedFunction of U2,U3 st h1 ** F = h2 ** F holds h1 = h2 let U1, U2 be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 holds for U3 being non-empty MSAlgebra over S for h1, h2 being ManySortedFunction of U2,U3 st h1 ** F = h2 ** F holds h1 = h2 let F be ManySortedFunction of U1,U2; ::_thesis: ( F is_epimorphism U1,U2 implies for U3 being non-empty MSAlgebra over S for h1, h2 being ManySortedFunction of U2,U3 st h1 ** F = h2 ** F holds h1 = h2 ) assume F is_epimorphism U1,U2 ; ::_thesis: for U3 being non-empty MSAlgebra over S for h1, h2 being ManySortedFunction of U2,U3 st h1 ** F = h2 ** F holds h1 = h2 then A1: F is "onto" by MSUALG_3:def_8; let U3 be non-empty MSAlgebra over S; ::_thesis: for h1, h2 being ManySortedFunction of U2,U3 st h1 ** F = h2 ** F holds h1 = h2 let h1, h2 be ManySortedFunction of U2,U3; ::_thesis: ( h1 ** F = h2 ** F implies h1 = h2 ) assume h1 ** F = h2 ** F ; ::_thesis: h1 = h2 hence h1 = h2 by A1, Th12; ::_thesis: verum end; theorem :: EXTENS_1:16 for S being non empty non void ManySortedSign for U2, U3 being non-empty MSAlgebra over S for F being ManySortedFunction of U2,U3 st F is_homomorphism U2,U3 holds ( F is_monomorphism U2,U3 iff for U1 being non-empty MSAlgebra over S for h1, h2 being ManySortedFunction of U1,U2 st h1 is_homomorphism U1,U2 & h2 is_homomorphism U1,U2 & F ** h1 = F ** h2 holds h1 = h2 ) proof let S be non empty non void ManySortedSign ; ::_thesis: for U2, U3 being non-empty MSAlgebra over S for F being ManySortedFunction of U2,U3 st F is_homomorphism U2,U3 holds ( F is_monomorphism U2,U3 iff for U1 being non-empty MSAlgebra over S for h1, h2 being ManySortedFunction of U1,U2 st h1 is_homomorphism U1,U2 & h2 is_homomorphism U1,U2 & F ** h1 = F ** h2 holds h1 = h2 ) let U2, U3 be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of U2,U3 st F is_homomorphism U2,U3 holds ( F is_monomorphism U2,U3 iff for U1 being non-empty MSAlgebra over S for h1, h2 being ManySortedFunction of U1,U2 st h1 is_homomorphism U1,U2 & h2 is_homomorphism U1,U2 & F ** h1 = F ** h2 holds h1 = h2 ) let F be ManySortedFunction of U2,U3; ::_thesis: ( F is_homomorphism U2,U3 implies ( F is_monomorphism U2,U3 iff for U1 being non-empty MSAlgebra over S for h1, h2 being ManySortedFunction of U1,U2 st h1 is_homomorphism U1,U2 & h2 is_homomorphism U1,U2 & F ** h1 = F ** h2 holds h1 = h2 ) ) assume A1: F is_homomorphism U2,U3 ; ::_thesis: ( F is_monomorphism U2,U3 iff for U1 being non-empty MSAlgebra over S for h1, h2 being ManySortedFunction of U1,U2 st h1 is_homomorphism U1,U2 & h2 is_homomorphism U1,U2 & F ** h1 = F ** h2 holds h1 = h2 ) set C = the Sorts of U3; set B = the Sorts of U2; thus ( F is_monomorphism U2,U3 implies for U1 being non-empty MSAlgebra over S for h1, h2 being ManySortedFunction of U1,U2 st h1 is_homomorphism U1,U2 & h2 is_homomorphism U1,U2 & F ** h1 = F ** h2 holds h1 = h2 ) ::_thesis: ( ( for U1 being non-empty MSAlgebra over S for h1, h2 being ManySortedFunction of U1,U2 st h1 is_homomorphism U1,U2 & h2 is_homomorphism U1,U2 & F ** h1 = F ** h2 holds h1 = h2 ) implies F is_monomorphism U2,U3 ) proof assume F is_monomorphism U2,U3 ; ::_thesis: for U1 being non-empty MSAlgebra over S for h1, h2 being ManySortedFunction of U1,U2 st h1 is_homomorphism U1,U2 & h2 is_homomorphism U1,U2 & F ** h1 = F ** h2 holds h1 = h2 then F is "1-1" by MSUALG_3:def_9; hence for U1 being non-empty MSAlgebra over S for h1, h2 being ManySortedFunction of U1,U2 st h1 is_homomorphism U1,U2 & h2 is_homomorphism U1,U2 & F ** h1 = F ** h2 holds h1 = h2 by Th13; ::_thesis: verum end; set I = the carrier of S; assume that A2: for U1 being non-empty MSAlgebra over S for h1, h2 being ManySortedFunction of U1,U2 st h1 is_homomorphism U1,U2 & h2 is_homomorphism U1,U2 & F ** h1 = F ** h2 holds h1 = h2 and A3: not F is_monomorphism U2,U3 ; ::_thesis: contradiction not F is "1-1" by A1, A3, MSUALG_3:def_9; then consider j being set such that A4: j in the carrier of S and A5: not F . j is one-to-one by MSUALG_3:1; set f = F . j; F . j is Function of ( the Sorts of U2 . j),( the Sorts of U3 . j) by A4, PBOOLE:def_15; then consider x1, x2 being set such that A6: x1 in the Sorts of U2 . j and A7: x2 in the Sorts of U2 . j and A8: (F . j) . x1 = (F . j) . x2 and A9: x1 <> x2 by A4, A5, FUNCT_2:19; ex U1 being non-empty MSAlgebra over S ex h1, h2 being ManySortedFunction of the Sorts of U1, the Sorts of U2 st ( h1 is_homomorphism U1,U2 & h2 is_homomorphism U1,U2 & F ** h1 = F ** h2 & h1 <> h2 ) proof take U1 = FreeMSA the Sorts of U2; ::_thesis: ex h1, h2 being ManySortedFunction of the Sorts of U1, the Sorts of U2 st ( h1 is_homomorphism U1,U2 & h2 is_homomorphism U1,U2 & F ** h1 = F ** h2 & h1 <> h2 ) reconsider FG = FreeGen the Sorts of U2 as GeneratorSet of U1 ; FG is V2() by MSAFREE:14; then reconsider FGj = FG . j, Bj = the Sorts of U2 . j as non empty set by A4; reconsider h = FGj --> x2 as Function of FGj,Bj by A7, FUNCOP_1:45; reconsider g = FGj --> x1 as Function of FGj,Bj by A6, FUNCOP_1:45; set r = Reverse the Sorts of U2; deffunc H1( set ) -> set = IFEQ (\$1,j,g,((Reverse the Sorts of U2) . \$1)); consider G being ManySortedSet of the carrier of S such that A10: for i being set st i in the carrier of S holds G . i = H1(i) from PBOOLE:sch_4(); deffunc H2( set ) -> set = IFEQ (\$1,j,h,((Reverse the Sorts of U2) . \$1)); consider H being ManySortedSet of the carrier of S such that A11: for i being set st i in the carrier of S holds H . i = H2(i) from PBOOLE:sch_4(); now__::_thesis:_for_G_being_ManySortedSet_of_the_carrier_of_S for_g,_h_being_Function_of_FGj,Bj_st_(_for_i_being_set_st_i_in_the_carrier_of_S_holds_ G_._i_=_IFEQ_(i,j,g,((Reverse_the_Sorts_of_U2)_._i))_)_holds_ G_is_Function-yielding let G be ManySortedSet of the carrier of S; ::_thesis: for g, h being Function of FGj,Bj st ( for i being set st i in the carrier of S holds G . i = IFEQ (i,j,g,((Reverse the Sorts of U2) . i)) ) holds G is Function-yielding let g, h be Function of FGj,Bj; ::_thesis: ( ( for i being set st i in the carrier of S holds G . i = IFEQ (i,j,g,((Reverse the Sorts of U2) . i)) ) implies G is Function-yielding ) assume A12: for i being set st i in the carrier of S holds G . i = IFEQ (i,j,g,((Reverse the Sorts of U2) . i)) ; ::_thesis: G is Function-yielding thus G is Function-yielding ::_thesis: verum proof let i be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( not i in dom G or G . i is set ) assume i in dom G ; ::_thesis: G . i is set then A13: i in the carrier of S ; now__::_thesis:_(_(_i_=_j_&_G_._i_is_set_)_or_(_i_<>_j_&_G_._i_is_set_)_) percases ( i = j or i <> j ) ; case i = j ; ::_thesis: G . i is set then IFEQ (i,j,g,((Reverse the Sorts of U2) . i)) = g by FUNCOP_1:def_8; hence G . i is set by A12, A13; ::_thesis: verum end; case i <> j ; ::_thesis: G . i is set then IFEQ (i,j,g,((Reverse the Sorts of U2) . i)) = (Reverse the Sorts of U2) . i by FUNCOP_1:def_8; hence G . i is set by A12, A13; ::_thesis: verum end; end; end; hence G . i is set ; ::_thesis: verum end; end; then reconsider G = G, H = H as ManySortedFunction of the carrier of S by A10, A11; now__::_thesis:_for_G_being_ManySortedFunction_of_the_carrier_of_S for_g,_h_being_Function_of_FGj,Bj_st_(_for_i_being_set_st_i_in_the_carrier_of_S_holds_ G_._i_=_IFEQ_(i,j,g,((Reverse_the_Sorts_of_U2)_._i))_)_holds_ G_is_ManySortedFunction_of_FG,_the_Sorts_of_U2 let G be ManySortedFunction of the carrier of S; ::_thesis: for g, h being Function of FGj,Bj st ( for i being set st i in the carrier of S holds G . i = IFEQ (i,j,g,((Reverse the Sorts of U2) . i)) ) holds G is ManySortedFunction of FG, the Sorts of U2 let g, h be Function of FGj,Bj; ::_thesis: ( ( for i being set st i in the carrier of S holds G . i = IFEQ (i,j,g,((Reverse the Sorts of U2) . i)) ) implies G is ManySortedFunction of FG, the Sorts of U2 ) assume A14: for i being set st i in the carrier of S holds G . i = IFEQ (i,j,g,((Reverse the Sorts of U2) . i)) ; ::_thesis: G is ManySortedFunction of FG, the Sorts of U2 thus G is ManySortedFunction of FG, the Sorts of U2 ::_thesis: verum proof let i be set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in the carrier of S or G . i is Element of K19(K20((FG . i),( the Sorts of U2 . i))) ) assume A15: i in the carrier of S ; ::_thesis: G . i is Element of K19(K20((FG . i),( the Sorts of U2 . i))) now__::_thesis:_(_(_i_=_j_&_G_._i_is_Element_of_K19(K20((FG_._i),(_the_Sorts_of_U2_._i)))_)_or_(_i_<>_j_&_G_._i_is_Element_of_K19(K20((FG_._i),(_the_Sorts_of_U2_._i)))_)_) percases ( i = j or i <> j ) ; caseA16: i = j ; ::_thesis: G . i is Element of K19(K20((FG . i),( the Sorts of U2 . i))) then IFEQ (i,j,g,((Reverse the Sorts of U2) . i)) = g by FUNCOP_1:def_8; hence G . i is Element of K19(K20((FG . i),( the Sorts of U2 . i))) by A14, A15, A16; ::_thesis: verum end; case i <> j ; ::_thesis: G . i is Element of K19(K20((FG . i),( the Sorts of U2 . i))) then IFEQ (i,j,g,((Reverse the Sorts of U2) . i)) = (Reverse the Sorts of U2) . i by FUNCOP_1:def_8; then G . i = (Reverse the Sorts of U2) . i by A14, A15; hence G . i is Element of K19(K20((FG . i),( the Sorts of U2 . i))) by A15, PBOOLE:def_15; ::_thesis: verum end; end; end; hence G . i is Element of K19(K20((FG . i),( the Sorts of U2 . i))) ; ::_thesis: verum end; end; then reconsider G = G, H = H as ManySortedFunction of FG, the Sorts of U2 by A10, A11; A17: FG is free by MSAFREE:16; then consider h1 being ManySortedFunction of U1,U2 such that A18: h1 is_homomorphism U1,U2 and A19: h1 || FG = G by MSAFREE:def_5; consider h2 being ManySortedFunction of U1,U2 such that A20: h2 is_homomorphism U1,U2 and A21: h2 || FG = H by A17, MSAFREE:def_5; take h1 ; ::_thesis: ex h2 being ManySortedFunction of the Sorts of U1, the Sorts of U2 st ( h1 is_homomorphism U1,U2 & h2 is_homomorphism U1,U2 & F ** h1 = F ** h2 & h1 <> h2 ) take h2 ; ::_thesis: ( h1 is_homomorphism U1,U2 & h2 is_homomorphism U1,U2 & F ** h1 = F ** h2 & h1 <> h2 ) thus ( h1 is_homomorphism U1,U2 & h2 is_homomorphism U1,U2 ) by A18, A20; ::_thesis: ( F ** h1 = F ** h2 & h1 <> h2 ) reconsider Fh1 = F ** h1, Fh2 = F ** h2 as ManySortedFunction of U1,U3 ; A22: Fh1 is_homomorphism U1,U3 by A1, A18, MSUALG_3:10; now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_ (F_**_(h1_||_FG))_._i_=_(F_**_(h2_||_FG))_._i let i be set ; ::_thesis: ( i in the carrier of S implies (F ** (h1 || FG)) . i = (F ** (h2 || FG)) . i ) assume A23: i in the carrier of S ; ::_thesis: (F ** (h1 || FG)) . i = (F ** (h2 || FG)) . i now__::_thesis:_(_(_i_=_j_&_(F_**_(h1_||_FG))_._i_=_(F_**_(h2_||_FG))_._i_)_or_(_i_<>_j_&_(F_**_(h1_||_FG))_._i_=_(F_**_(h2_||_FG))_._i_)_) percases ( i = j or i <> j ) ; caseA24: i = j ; ::_thesis: (F ** (h1 || FG)) . i = (F ** (h2 || FG)) . i then A25: F . j is Function of ( the Sorts of U2 . i),( the Sorts of U3 . i) by A4, PBOOLE:def_15; then reconsider fg = (F . j) * g as Function of FGj,( the Sorts of U3 . i) by A24, FUNCT_2:13; reconsider fh = (F . j) * h as Function of FGj,( the Sorts of U3 . i) by A24, A25, FUNCT_2:13; now__::_thesis:_for_x_being_set_st_x_in_FGj_holds_ fg_._x_=_fh_._x let x be set ; ::_thesis: ( x in FGj implies fg . x = fh . x ) assume A26: x in FGj ; ::_thesis: fg . x = fh . x hence fg . x = (F . j) . (g . x) by FUNCT_2:15 .= (F . j) . x2 by A8, A26, FUNCOP_1:7 .= (F . j) . (h . x) by A26, FUNCOP_1:7 .= fh . x by A26, FUNCT_2:15 ; ::_thesis: verum end; then A27: (F . j) * g = (F . j) * h by FUNCT_2:12; IFEQ (i,j,g,((Reverse the Sorts of U2) . i)) = g by A24, FUNCOP_1:def_8; then g = (h1 || FG) . i by A10, A19, A23; then A28: (F ** (h1 || FG)) . i = (F . j) * g by A4, A24, MSUALG_3:2; IFEQ (i,j,h,((Reverse the Sorts of U2) . i)) = h by A24, FUNCOP_1:def_8; then h = (h2 || FG) . i by A11, A21, A23; hence (F ** (h1 || FG)) . i = (F ** (h2 || FG)) . i by A4, A24, A27, A28, MSUALG_3:2; ::_thesis: verum end; caseA29: i <> j ; ::_thesis: (F ** (h1 || FG)) . i = (F ** (h2 || FG)) . i reconsider f9 = F . i as Function of ( the Sorts of U2 . i),( the Sorts of U3 . i) by A23, PBOOLE:def_15; reconsider h29 = (h2 || FG) . i as Function of (FG . i),( the Sorts of U2 . i) by A23, PBOOLE:def_15; A30: IFEQ (i,j,h,((Reverse the Sorts of U2) . i)) = (Reverse the Sorts of U2) . i by A29, FUNCOP_1:def_8; IFEQ (i,j,g,((Reverse the Sorts of U2) . i)) = (Reverse the Sorts of U2) . i by A29, FUNCOP_1:def_8; then (h1 || FG) . i = (Reverse the Sorts of U2) . i by A10, A19, A23 .= (h2 || FG) . i by A11, A21, A23, A30 ; hence (F ** (h1 || FG)) . i = f9 * h29 by A23, MSUALG_3:2 .= (F ** (h2 || FG)) . i by A23, MSUALG_3:2 ; ::_thesis: verum end; end; end; hence (F ** (h1 || FG)) . i = (F ** (h2 || FG)) . i ; ::_thesis: verum end; then A31: F ** (h1 || FG) = F ** (h2 || FG) by PBOOLE:3; A32: Fh2 is_homomorphism U1,U3 by A1, A20, MSUALG_3:10; (F ** h1) || FG = F ** (h1 || FG) by Th4 .= (F ** h2) || FG by A31, Th4 ; hence F ** h1 = F ** h2 by A22, A32, Th14; ::_thesis: h1 <> h2 now__::_thesis:_ex_i_being_set_st_ (_i_in_the_carrier_of_S_&_G_<>_H_) take i = j; ::_thesis: ( i in the carrier of S & G <> H ) thus i in the carrier of S by A4; ::_thesis: G <> H A33: now__::_thesis:_for_x_being_Element_of_FGj_holds_not_g_=_h let x be Element of FGj; ::_thesis: not g = h assume g = h ; ::_thesis: contradiction then g . x = x2 by FUNCOP_1:7; hence contradiction by A9, FUNCOP_1:7; ::_thesis: verum end; A34: h = IFEQ (i,j,h,((Reverse the Sorts of U2) . i)) by FUNCOP_1:def_8 .= H . i by A4, A11 ; g = IFEQ (i,j,g,((Reverse the Sorts of U2) . i)) by FUNCOP_1:def_8 .= G . i by A4, A10 ; hence G <> H by A34, A33; ::_thesis: verum end; hence h1 <> h2 by A19, A21; ::_thesis: verum end; hence contradiction by A2; ::_thesis: verum end; registration let S be non empty non void ManySortedSign ; let U1 be non-empty MSAlgebra over S; cluster Relation-like V2() the carrier of S -defined Function-like non empty total for GeneratorSet of U1; existence not for b1 being GeneratorSet of U1 holds b1 is V2() proof the Sorts of U1 is GeneratorSet of U1 by MSAFREE2:6; then consider G being GeneratorSet of U1 such that A1: G = the Sorts of U1 ; take G ; ::_thesis: G is V2() thus G is V2() by A1; ::_thesis: verum end; end; theorem :: EXTENS_1:17 for S being non empty non void ManySortedSign for U1 being MSAlgebra over S for A, B being MSSubset of U1 st A is ManySortedSubset of B holds GenMSAlg A is MSSubAlgebra of GenMSAlg B proof let S be non empty non void ManySortedSign ; ::_thesis: for U1 being MSAlgebra over S for A, B being MSSubset of U1 st A is ManySortedSubset of B holds GenMSAlg A is MSSubAlgebra of GenMSAlg B let U1 be MSAlgebra over S; ::_thesis: for A, B being MSSubset of U1 st A is ManySortedSubset of B holds GenMSAlg A is MSSubAlgebra of GenMSAlg B let A, B be MSSubset of U1; ::_thesis: ( A is ManySortedSubset of B implies GenMSAlg A is MSSubAlgebra of GenMSAlg B ) B is MSSubset of (GenMSAlg B) by MSUALG_2:def_17; then A1: B c= the Sorts of (GenMSAlg B) by PBOOLE:def_18; assume A is ManySortedSubset of B ; ::_thesis: GenMSAlg A is MSSubAlgebra of GenMSAlg B then A c= B by PBOOLE:def_18; then A c= the Sorts of (GenMSAlg B) by A1, PBOOLE:13; then A is MSSubset of (GenMSAlg B) by PBOOLE:def_18; hence GenMSAlg A is MSSubAlgebra of GenMSAlg B by MSUALG_2:def_17; ::_thesis: verum end; theorem :: EXTENS_1:18 for S being non empty non void ManySortedSign for U1 being MSAlgebra over S for U2 being MSSubAlgebra of U1 for B1 being MSSubset of U1 for B2 being MSSubset of U2 st B1 = B2 holds GenMSAlg B1 = GenMSAlg B2 proof let S be non empty non void ManySortedSign ; ::_thesis: for U1 being MSAlgebra over S for U2 being MSSubAlgebra of U1 for B1 being MSSubset of U1 for B2 being MSSubset of U2 st B1 = B2 holds GenMSAlg B1 = GenMSAlg B2 let U1 be MSAlgebra over S; ::_thesis: for U2 being MSSubAlgebra of U1 for B1 being MSSubset of U1 for B2 being MSSubset of U2 st B1 = B2 holds GenMSAlg B1 = GenMSAlg B2 let U2 be MSSubAlgebra of U1; ::_thesis: for B1 being MSSubset of U1 for B2 being MSSubset of U2 st B1 = B2 holds GenMSAlg B1 = GenMSAlg B2 let B1 be MSSubset of U1; ::_thesis: for B2 being MSSubset of U2 st B1 = B2 holds GenMSAlg B1 = GenMSAlg B2 let B2 be MSSubset of U2; ::_thesis: ( B1 = B2 implies GenMSAlg B1 = GenMSAlg B2 ) assume A1: B1 = B2 ; ::_thesis: GenMSAlg B1 = GenMSAlg B2 reconsider H = GenMSAlg B1 as MSSubAlgebra of U2 by A1, MSUALG_2:def_17; reconsider G = GenMSAlg B2 as MSSubAlgebra of U1 by MSUALG_2:6; B1 is MSSubset of G by A1, MSUALG_2:def_17; then A2: GenMSAlg B1 is MSSubAlgebra of G by MSUALG_2:def_17; B1 is MSSubset of H by MSUALG_2:def_17; then GenMSAlg B2 is MSSubAlgebra of GenMSAlg B1 by A1, MSUALG_2:def_17; hence GenMSAlg B1 = GenMSAlg B2 by A2, MSUALG_2:7; ::_thesis: verum end; theorem :: EXTENS_1:19 for S being non empty non void ManySortedSign for U1, U2 being non-empty MSAlgebra over S for Gen being GeneratorSet of U1 for h1, h2 being ManySortedFunction of U1,U2 st h1 is_homomorphism U1,U2 & h2 is_homomorphism U1,U2 & h1 || Gen = h2 || Gen holds h1 = h2 proof let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2 being non-empty MSAlgebra over S for Gen being GeneratorSet of U1 for h1, h2 being ManySortedFunction of U1,U2 st h1 is_homomorphism U1,U2 & h2 is_homomorphism U1,U2 & h1 || Gen = h2 || Gen holds h1 = h2 let U1, U2 be non-empty MSAlgebra over S; ::_thesis: for Gen being GeneratorSet of U1 for h1, h2 being ManySortedFunction of U1,U2 st h1 is_homomorphism U1,U2 & h2 is_homomorphism U1,U2 & h1 || Gen = h2 || Gen holds h1 = h2 let Gen be GeneratorSet of U1; ::_thesis: for h1, h2 being ManySortedFunction of U1,U2 st h1 is_homomorphism U1,U2 & h2 is_homomorphism U1,U2 & h1 || Gen = h2 || Gen holds h1 = h2 let h1, h2 be ManySortedFunction of U1,U2; ::_thesis: ( h1 is_homomorphism U1,U2 & h2 is_homomorphism U1,U2 & h1 || Gen = h2 || Gen implies h1 = h2 ) assume that A1: h1 is_homomorphism U1,U2 and A2: h2 is_homomorphism U1,U2 and A3: h1 || Gen = h2 || Gen ; ::_thesis: h1 = h2 defpred S1[ set , set ] means ex s being SortSymbol of S st ( \$1 = s & (h1 . s) . \$2 = (h2 . s) . \$2 ); set I = the carrier of S; consider A being ManySortedSet of the carrier of S such that A4: for i being set st i in the carrier of S holds for e being set holds ( e in A . i iff ( e in the Sorts of U1 . i & S1[i,e] ) ) from PBOOLE:sch_2(); A is ManySortedSubset of the Sorts of U1 proof let i be set ; :: according to PBOOLE:def_2,PBOOLE:def_18 ::_thesis: ( not i in the carrier of S or A . i c= the Sorts of U1 . i ) assume A5: i in the carrier of S ; ::_thesis: A . i c= the Sorts of U1 . i let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in A . i or e in the Sorts of U1 . i ) assume e in A . i ; ::_thesis: e in the Sorts of U1 . i hence e in the Sorts of U1 . i by A4, A5; ::_thesis: verum end; then reconsider A = A as MSSubset of U1 ; A is opers_closed proof let o be OperSymbol of S; :: according to MSUALG_2:def_6 ::_thesis: A is_closed_on o let y be set ; :: according to MSUALG_2:def_5,TARSKI:def_3 ::_thesis: ( not y in rng ((Den (o,U1)) | (( the Arity of S * (A #)) . o)) or y in ( the ResultSort of S * A) . o ) set r = the_result_sort_of o; set ar = the_arity_of o; assume y in rng ((Den (o,U1)) | (((A #) * the Arity of S) . o)) ; ::_thesis: y in ( the ResultSort of S * A) . o then consider x being set such that A6: x in dom ((Den (o,U1)) | (((A #) * the Arity of S) . o)) and A7: ((Den (o,U1)) | (((A #) * the Arity of S) . o)) . x = y by FUNCT_1:def_3; A8: x in ((A #) * the Arity of S) . o by A6, RELAT_1:57; then x in (A #) . ( the Arity of S . o) by FUNCT_2:15; then x in (A #) . (the_arity_of o) by MSUALG_1:def_1; then A9: x in product (A * (the_arity_of o)) by FINSEQ_2:def_5; reconsider x = x as Element of Args (o,U1) by A6; A10: y = (Den (o,U1)) . x by A7, A8, FUNCT_1:49; A11: dom (h1 # x) = dom (the_arity_of o) by MSUALG_3:6; A12: for n being set st n in dom (h1 # x) holds (h1 # x) . n = (h2 # x) . n proof let n be set ; ::_thesis: ( n in dom (h1 # x) implies (h1 # x) . n = (h2 # x) . n ) A13: dom x = dom (the_arity_of o) by MSUALG_3:6; assume A14: n in dom (h1 # x) ; ::_thesis: (h1 # x) . n = (h2 # x) . n then reconsider n9 = n as Nat by A11, ORDINAL1:def_12; dom x = dom (A * (the_arity_of o)) by A9, CARD_3:9; then x . n in (A * (the_arity_of o)) . n by A9, A11, A14, A13, CARD_3:9; then x . n in A . ((the_arity_of o) . n) by A11, A14, FUNCT_1:13; then x . n in A . ((the_arity_of o) /. n) by A11, A14, PARTFUN1:def_6; then ex s being SortSymbol of S st ( s = (the_arity_of o) /. n & (h1 . s) . (x . n) = (h2 . s) . (x . n) ) by A4; hence (h1 # x) . n = (h2 . ((the_arity_of o) /. n)) . (x . n9) by A11, A14, A13, MSUALG_3:def_6 .= (h2 # x) . n by A11, A14, A13, MSUALG_3:def_6 ; ::_thesis: verum end; (Den (o,U1)) . x is Element of ( the Sorts of U1 * the ResultSort of S) . o by MSUALG_1:def_5; then (Den (o,U1)) . x is Element of the Sorts of U1 . ( the ResultSort of S . o) by FUNCT_2:15; then A15: (Den (o,U1)) . x is Element of the Sorts of U1 . (the_result_sort_of o) by MSUALG_1:def_2; A16: dom (h2 # x) = dom (the_arity_of o) by MSUALG_3:6; (h1 . (the_result_sort_of o)) . y = (h1 . (the_result_sort_of o)) . ((Den (o,U1)) . x) by A7, A8, FUNCT_1:49 .= (Den (o,U2)) . (h1 # x) by A1, MSUALG_3:def_7 .= (Den (o,U2)) . (h2 # x) by A16, A12, FUNCT_1:2, MSUALG_3:6 .= (h2 . (the_result_sort_of o)) . ((Den (o,U1)) . x) by A2, MSUALG_3:def_7 .= (h2 . (the_result_sort_of o)) . y by A7, A8, FUNCT_1:49 ; then y in A . (the_result_sort_of o) by A4, A10, A15; then y in A . ( the ResultSort of S . o) by MSUALG_1:def_2; hence y in ( the ResultSort of S * A) . o by FUNCT_2:15; ::_thesis: verum end; then A17: U1 | A = MSAlgebra(# A,(Opers (U1,A)) #) by MSUALG_2:def_15; Gen is ManySortedSubset of the Sorts of (U1 | A) proof let i be set ; :: according to PBOOLE:def_2,PBOOLE:def_18 ::_thesis: ( not i in the carrier of S or Gen . i c= the Sorts of (U1 | A) . i ) assume A18: i in the carrier of S ; ::_thesis: Gen . i c= the Sorts of (U1 | A) . i reconsider s = i as SortSymbol of S by A18; Gen c= the Sorts of U1 by PBOOLE:def_18; then A19: Gen . i c= the Sorts of U1 . i by A18, PBOOLE:def_2; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Gen . i or x in the Sorts of (U1 | A) . i ) assume A20: x in Gen . i ; ::_thesis: x in the Sorts of (U1 | A) . i (h1 . s) . x = ((h1 . s) | (Gen . s)) . x by A20, FUNCT_1:49 .= ((h1 || Gen) . s) . x by MSAFREE:def_1 .= ((h2 . s) | (Gen . s)) . x by A3, MSAFREE:def_1 .= (h2 . s) . x by A20, FUNCT_1:49 ; hence x in the Sorts of (U1 | A) . i by A4, A17, A20, A19; ::_thesis: verum end; then A21: GenMSAlg Gen is MSSubAlgebra of U1 | A by MSUALG_2:def_17; the Sorts of (GenMSAlg Gen) = the Sorts of U1 by MSAFREE:def_4; then the Sorts of U1 is ManySortedSubset of A by A17, A21, MSUALG_2:def_9; then A22: the Sorts of U1 c= A by PBOOLE:def_18; now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_ h1_._i_=_h2_._i let i be set ; ::_thesis: ( i in the carrier of S implies h1 . i = h2 . i ) assume A23: i in the carrier of S ; ::_thesis: h1 . i = h2 . i then reconsider s = i as SortSymbol of S ; A24: dom (h1 . s) = the Sorts of U1 . i by FUNCT_2:def_1; A25: now__::_thesis:_for_x_being_set_st_x_in_dom_(h1_._s)_holds_ (h1_._s)_._x_=_(h2_._s)_._x A26: the Sorts of U1 . i c= A . i by A22, A23, PBOOLE:def_2; let x be set ; ::_thesis: ( x in dom (h1 . s) implies (h1 . s) . x = (h2 . s) . x ) assume x in dom (h1 . s) ; ::_thesis: (h1 . s) . x = (h2 . s) . x then ex t being SortSymbol of S st ( t = s & (h1 . t) . x = (h2 . t) . x ) by A4, A24, A26; hence (h1 . s) . x = (h2 . s) . x ; ::_thesis: verum end; dom (h2 . s) = the Sorts of U1 . i by FUNCT_2:def_1; hence h1 . i = h2 . i by A24, A25, FUNCT_1:2; ::_thesis: verum end; hence h1 = h2 by PBOOLE:3; ::_thesis: verum end;