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