let J be non empty non void Signature; :: thesis: for S being J -extension Signature

for T being MSAlgebra over J

for I being set st I c= the carrier of S \ the carrier of J holds

for X being ManySortedSet of I ex Q being MSAlgebra over S st

( Q is T -extension & the Sorts of Q | I = X )

let S be J -extension Signature; :: thesis: for T being MSAlgebra over J

for I being set st I c= the carrier of S \ the carrier of J holds

for X being ManySortedSet of I ex Q being MSAlgebra over S st

( Q is T -extension & the Sorts of Q | I = X )

let T be MSAlgebra over J; :: thesis: for I being set st I c= the carrier of S \ the carrier of J holds

for X being ManySortedSet of I ex Q being MSAlgebra over S st

( Q is T -extension & the Sorts of Q | I = X )

let I be set ; :: thesis: ( I c= the carrier of S \ the carrier of J implies for X being ManySortedSet of I ex Q being MSAlgebra over S st

( Q is T -extension & the Sorts of Q | I = X ) )

assume A1: I c= the carrier of S \ the carrier of J ; :: thesis: for X being ManySortedSet of I ex Q being MSAlgebra over S st

( Q is T -extension & the Sorts of Q | I = X )

let X be ManySortedSet of I; :: thesis: ex Q being MSAlgebra over S st

( Q is T -extension & the Sorts of Q | I = X )

set U = ( the ManySortedSet of the carrier of S +* the Sorts of T) +* X;

A2: J is Subsignature of S by Def2;

dom (( the ManySortedSet of the carrier of S +* the Sorts of T) +* X) = (dom ( the ManySortedSet of the carrier of S +* the Sorts of T)) \/ (dom X) by FUNCT_4:def 1

.= ((dom the ManySortedSet of the carrier of S) \/ (dom the Sorts of T)) \/ (dom X) by FUNCT_4:def 1

.= ((dom the ManySortedSet of the carrier of S) \/ (dom the Sorts of T)) \/ I by PARTFUN1:def 2

.= ((dom the ManySortedSet of the carrier of S) \/ the carrier of J) \/ I by PARTFUN1:def 2

.= ( the carrier of S \/ the carrier of J) \/ I by PARTFUN1:def 2

.= the carrier of S \/ I by A2, INSTALG1:10, XBOOLE_1:12

.= the carrier of S by A1, XBOOLE_1:1, XBOOLE_1:12 ;

then reconsider U = ( the ManySortedSet of the carrier of S +* the Sorts of T) +* X as ManySortedSet of the carrier of S by RELAT_1:def 18, PARTFUN1:def 2;

set C = the ManySortedFunction of (U #) * the Arity of S,U * the ResultSort of S +* the Charact of T;

dom ( the ManySortedFunction of (U #) * the Arity of S,U * the ResultSort of S +* the Charact of T) = (dom the ManySortedFunction of (U #) * the Arity of S,U * the ResultSort of S) \/ (dom the Charact of T) by FUNCT_4:def 1

.= the carrier' of S \/ (dom the Charact of T) by PARTFUN1:def 2

.= the carrier' of S \/ the carrier' of J by PARTFUN1:def 2

.= the carrier' of S by A2, INSTALG1:10, XBOOLE_1:12 ;

then reconsider C = the ManySortedFunction of (U #) * the Arity of S,U * the ResultSort of S +* the Charact of T as ManySortedSet of the carrier' of S by RELAT_1:def 18, PARTFUN1:def 2;

A3: ( dom X = I & I misses the carrier of J ) by A1, XBOOLE_1:63, XBOOLE_1:79, PARTFUN1:def 2;

C is ManySortedFunction of (U #) * the Arity of S,U * the ResultSort of S

take Q = MSAlgebra(# U,C #); :: thesis: ( Q is T -extension & the Sorts of Q | I = X )

thus Q is T -extension :: thesis: the Sorts of Q | I = X

hence the Sorts of Q | I = X ; :: thesis: verum

for T being MSAlgebra over J

for I being set st I c= the carrier of S \ the carrier of J holds

for X being ManySortedSet of I ex Q being MSAlgebra over S st

( Q is T -extension & the Sorts of Q | I = X )

let S be J -extension Signature; :: thesis: for T being MSAlgebra over J

for I being set st I c= the carrier of S \ the carrier of J holds

for X being ManySortedSet of I ex Q being MSAlgebra over S st

( Q is T -extension & the Sorts of Q | I = X )

let T be MSAlgebra over J; :: thesis: for I being set st I c= the carrier of S \ the carrier of J holds

for X being ManySortedSet of I ex Q being MSAlgebra over S st

( Q is T -extension & the Sorts of Q | I = X )

let I be set ; :: thesis: ( I c= the carrier of S \ the carrier of J implies for X being ManySortedSet of I ex Q being MSAlgebra over S st

( Q is T -extension & the Sorts of Q | I = X ) )

assume A1: I c= the carrier of S \ the carrier of J ; :: thesis: for X being ManySortedSet of I ex Q being MSAlgebra over S st

( Q is T -extension & the Sorts of Q | I = X )

let X be ManySortedSet of I; :: thesis: ex Q being MSAlgebra over S st

( Q is T -extension & the Sorts of Q | I = X )

set U = ( the ManySortedSet of the carrier of S +* the Sorts of T) +* X;

A2: J is Subsignature of S by Def2;

dom (( the ManySortedSet of the carrier of S +* the Sorts of T) +* X) = (dom ( the ManySortedSet of the carrier of S +* the Sorts of T)) \/ (dom X) by FUNCT_4:def 1

.= ((dom the ManySortedSet of the carrier of S) \/ (dom the Sorts of T)) \/ (dom X) by FUNCT_4:def 1

.= ((dom the ManySortedSet of the carrier of S) \/ (dom the Sorts of T)) \/ I by PARTFUN1:def 2

.= ((dom the ManySortedSet of the carrier of S) \/ the carrier of J) \/ I by PARTFUN1:def 2

.= ( the carrier of S \/ the carrier of J) \/ I by PARTFUN1:def 2

.= the carrier of S \/ I by A2, INSTALG1:10, XBOOLE_1:12

.= the carrier of S by A1, XBOOLE_1:1, XBOOLE_1:12 ;

then reconsider U = ( the ManySortedSet of the carrier of S +* the Sorts of T) +* X as ManySortedSet of the carrier of S by RELAT_1:def 18, PARTFUN1:def 2;

set C = the ManySortedFunction of (U #) * the Arity of S,U * the ResultSort of S +* the Charact of T;

dom ( the ManySortedFunction of (U #) * the Arity of S,U * the ResultSort of S +* the Charact of T) = (dom the ManySortedFunction of (U #) * the Arity of S,U * the ResultSort of S) \/ (dom the Charact of T) by FUNCT_4:def 1

.= the carrier' of S \/ (dom the Charact of T) by PARTFUN1:def 2

.= the carrier' of S \/ the carrier' of J by PARTFUN1:def 2

.= the carrier' of S by A2, INSTALG1:10, XBOOLE_1:12 ;

then reconsider C = the ManySortedFunction of (U #) * the Arity of S,U * the ResultSort of S +* the Charact of T as ManySortedSet of the carrier' of S by RELAT_1:def 18, PARTFUN1:def 2;

A3: ( dom X = I & I misses the carrier of J ) by A1, XBOOLE_1:63, XBOOLE_1:79, PARTFUN1:def 2;

C is ManySortedFunction of (U #) * the Arity of S,U * the ResultSort of S

proof

then reconsider C = C as ManySortedFunction of (U #) * the Arity of S,U * the ResultSort of S ;
let o be object ; :: according to PBOOLE:def 15 :: thesis: ( not o in the carrier' of S or C . o is Element of bool [:(((U #) * the Arity of S) . o),((U * the ResultSort of S) . o):] )

assume A4: o in the carrier' of S ; :: thesis: C . o is Element of bool [:(((U #) * the Arity of S) . o),((U * the ResultSort of S) . o):]

then reconsider w = o as OperSymbol of S ;

end;assume A4: o in the carrier' of S ; :: thesis: C . o is Element of bool [:(((U #) * the Arity of S) . o),((U * the ResultSort of S) . o):]

then reconsider w = o as OperSymbol of S ;

per cases
( o in the carrier' of J or o nin the carrier' of J )
;

end;

suppose A5:
o in the carrier' of J
; :: thesis: C . o is Element of bool [:(((U #) * the Arity of S) . o),((U * the ResultSort of S) . o):]

then reconsider u = o as OperSymbol of J ;

o in dom the Charact of T by A5, PARTFUN1:def 2;

then A6: C . o = the Charact of T . o by FUNCT_4:13;

( the Arity of J = the Arity of S | the carrier' of J & the ResultSort of J = the ResultSort of S | the carrier' of J ) by A2, INSTALG1:12;

then A7: ( the Arity of J . o = the Arity of S . o & the ResultSort of J . o = the ResultSort of S . o ) by A5, FUNCT_1:49;

A8: ( ( the Sorts of T #) . (the_arity_of u) = product ( the Sorts of T * (the_arity_of u)) & (U #) . (the_arity_of w) = product (U * (the_arity_of w)) ) by FINSEQ_2:def 5;

A9: ( dom the Sorts of T = the carrier of J & rng (the_arity_of u) c= the carrier of J ) by PARTFUN1:def 2;

U * (the_arity_of w) = ( the ManySortedSet of the carrier of S +* the Sorts of T) * (the_arity_of w) by A3, A7, A9, XBOOLE_1:63, FUNCT_7:11

.= the Sorts of T * (the_arity_of u) by A9, A7, AOFA_I00:3 ;

then A10: ( the Sorts of T #) . (the_arity_of u) = (U #) . (the_arity_of w) by A8;

A11: ( rng the ResultSort of S c= the carrier of S & rng the ResultSort of J c= the carrier of J & the carrier of J = dom the Sorts of T ) by PARTFUN1:def 2;

rng the ResultSort of J misses dom X by A3, XBOOLE_1:63;

then A12: U * the ResultSort of J = ( the ManySortedSet of the carrier of S +* the Sorts of T) * the ResultSort of J by FUNCT_7:11

.= the Sorts of T * the ResultSort of J by A11, AOFA_I00:3 ;

( (( the Sorts of T #) * the Arity of J) . o = ( the Sorts of T #) . (the_arity_of u) & ((U #) * the Arity of S) . o = (U #) . (the_arity_of w) & ( the Sorts of T * the ResultSort of S) . o = the Sorts of T . ( the ResultSort of S . o) & ( the Sorts of T * the ResultSort of J) . o = the Sorts of T . ( the ResultSort of J . o) & (U * the ResultSort of S) . o = U . ( the ResultSort of S . o) & (U * the ResultSort of J) . o = U . ( the ResultSort of J . o) ) by A4, A5, FUNCT_2:15;

hence C . o is Element of bool [:(((U #) * the Arity of S) . o),((U * the ResultSort of S) . o):] by A6, A7, A10, A12; :: thesis: verum

end;o in dom the Charact of T by A5, PARTFUN1:def 2;

then A6: C . o = the Charact of T . o by FUNCT_4:13;

( the Arity of J = the Arity of S | the carrier' of J & the ResultSort of J = the ResultSort of S | the carrier' of J ) by A2, INSTALG1:12;

then A7: ( the Arity of J . o = the Arity of S . o & the ResultSort of J . o = the ResultSort of S . o ) by A5, FUNCT_1:49;

A8: ( ( the Sorts of T #) . (the_arity_of u) = product ( the Sorts of T * (the_arity_of u)) & (U #) . (the_arity_of w) = product (U * (the_arity_of w)) ) by FINSEQ_2:def 5;

A9: ( dom the Sorts of T = the carrier of J & rng (the_arity_of u) c= the carrier of J ) by PARTFUN1:def 2;

U * (the_arity_of w) = ( the ManySortedSet of the carrier of S +* the Sorts of T) * (the_arity_of w) by A3, A7, A9, XBOOLE_1:63, FUNCT_7:11

.= the Sorts of T * (the_arity_of u) by A9, A7, AOFA_I00:3 ;

then A10: ( the Sorts of T #) . (the_arity_of u) = (U #) . (the_arity_of w) by A8;

A11: ( rng the ResultSort of S c= the carrier of S & rng the ResultSort of J c= the carrier of J & the carrier of J = dom the Sorts of T ) by PARTFUN1:def 2;

rng the ResultSort of J misses dom X by A3, XBOOLE_1:63;

then A12: U * the ResultSort of J = ( the ManySortedSet of the carrier of S +* the Sorts of T) * the ResultSort of J by FUNCT_7:11

.= the Sorts of T * the ResultSort of J by A11, AOFA_I00:3 ;

( (( the Sorts of T #) * the Arity of J) . o = ( the Sorts of T #) . (the_arity_of u) & ((U #) * the Arity of S) . o = (U #) . (the_arity_of w) & ( the Sorts of T * the ResultSort of S) . o = the Sorts of T . ( the ResultSort of S . o) & ( the Sorts of T * the ResultSort of J) . o = the Sorts of T . ( the ResultSort of J . o) & (U * the ResultSort of S) . o = U . ( the ResultSort of S . o) & (U * the ResultSort of J) . o = U . ( the ResultSort of J . o) ) by A4, A5, FUNCT_2:15;

hence C . o is Element of bool [:(((U #) * the Arity of S) . o),((U * the ResultSort of S) . o):] by A6, A7, A10, A12; :: thesis: verum

suppose
o nin the carrier' of J
; :: thesis: C . o is Element of bool [:(((U #) * the Arity of S) . o),((U * the ResultSort of S) . o):]

then
o nin dom the Charact of T
;

then C . o = the ManySortedFunction of (U #) * the Arity of S,U * the ResultSort of S . o by FUNCT_4:11;

hence C . o is Element of bool [:(((U #) * the Arity of S) . o),((U * the ResultSort of S) . o):] ; :: thesis: verum

end;then C . o = the ManySortedFunction of (U #) * the Arity of S,U * the ResultSort of S . o by FUNCT_4:11;

hence C . o is Element of bool [:(((U #) * the Arity of S) . o),((U * the ResultSort of S) . o):] ; :: thesis: verum

take Q = MSAlgebra(# U,C #); :: thesis: ( Q is T -extension & the Sorts of Q | I = X )

thus Q is T -extension :: thesis: the Sorts of Q | I = X

proof

dom X = I
by PARTFUN1:def 2;
A13:
Q | J = Q | (J,(id the carrier of J),(id the carrier' of J))
by INSTALG1:def 4;

id the carrier of J, id the carrier' of J form_morphism_between J,S by A2, INSTALG1:def 2;

then ( the Sorts of (Q | J) = the Sorts of Q * (id the carrier of J) & the Charact of (Q | J) = the Charact of Q * (id the carrier' of J) ) by A13, INSTALG1:def 3;

then A14: ( the Sorts of (Q | J) = the Sorts of Q | the carrier of J & the Charact of (Q | J) = the Charact of Q | the carrier' of J ) by RELAT_1:65;

A15: ( dom the Sorts of T = the carrier of J & dom the Charact of T = the carrier' of J ) by PARTFUN1:def 2;

the Sorts of (Q | J) = ( the ManySortedSet of the carrier of S +* the Sorts of T) | the carrier of J by A3, A14, FUNCT_4:72

.= the Sorts of T by A15 ;

hence Q | J = MSAlgebra(# the Sorts of T, the Charact of T #) by A14, A15; :: according to AOFA_L00:def 19 :: thesis: verum

end;id the carrier of J, id the carrier' of J form_morphism_between J,S by A2, INSTALG1:def 2;

then ( the Sorts of (Q | J) = the Sorts of Q * (id the carrier of J) & the Charact of (Q | J) = the Charact of Q * (id the carrier' of J) ) by A13, INSTALG1:def 3;

then A14: ( the Sorts of (Q | J) = the Sorts of Q | the carrier of J & the Charact of (Q | J) = the Charact of Q | the carrier' of J ) by RELAT_1:65;

A15: ( dom the Sorts of T = the carrier of J & dom the Charact of T = the carrier' of J ) by PARTFUN1:def 2;

the Sorts of (Q | J) = ( the ManySortedSet of the carrier of S +* the Sorts of T) | the carrier of J by A3, A14, FUNCT_4:72

.= the Sorts of T by A15 ;

hence Q | J = MSAlgebra(# the Sorts of T, the Charact of T #) by A14, A15; :: according to AOFA_L00:def 19 :: thesis: verum

hence the Sorts of Q | I = X ; :: thesis: verum