let J be non empty non void Signature; 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; 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; 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 ; ( 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
; 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; 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
let o be
object ;
PBOOLE:def 15 ( 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
;
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 )
;
suppose A5:
o in the
carrier' of
J
;
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;
verum end;
end;
then reconsider C = C as ManySortedFunction of (U #) * the Arity of S,U * the ResultSort of S ;
take Q = MSAlgebra(# U,C #); ( Q is T -extension & the Sorts of Q | I = X )
thus
Q is T -extension
the Sorts of Q | I = Xproof
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;
AOFA_L00:def 19 verum
end;
dom X = I
by PARTFUN1:def 2;
hence
the Sorts of Q | I = X
; verum