let J be non void Signature; :: thesis: for T being MSAlgebra over J

for X being ManySortedSubset of the Sorts of T

for S being non void J -extension Signature

for Q being b_{1} -extension MSAlgebra over S holds X extended_by ({}, the carrier of S) is ManySortedSubset of the Sorts of Q

let T be MSAlgebra over J; :: thesis: for X being ManySortedSubset of the Sorts of T

for S being non void J -extension Signature

for Q being T -extension MSAlgebra over S holds X extended_by ({}, the carrier of S) is ManySortedSubset of the Sorts of Q

let X be ManySortedSubset of the Sorts of T; :: thesis: for S being non void J -extension Signature

for Q being T -extension MSAlgebra over S holds X extended_by ({}, the carrier of S) is ManySortedSubset of the Sorts of Q

let S be non void J -extension Signature; :: thesis: for Q being T -extension MSAlgebra over S holds X extended_by ({}, the carrier of S) is ManySortedSubset of the Sorts of Q

let Q be T -extension MSAlgebra over S; :: thesis: X extended_by ({}, the carrier of S) is ManySortedSubset of the Sorts of Q

let x be object ; :: according to PBOOLE:def 2,PBOOLE:def 18 :: thesis: ( not x in the carrier of S or (X extended_by ({}, the carrier of S)) . x c= the Sorts of Q . x )

assume A1: x in the carrier of S ; :: thesis: (X extended_by ({}, the carrier of S)) . x c= the Sorts of Q . x

then reconsider s = x as SortSymbol of S ;

for X being ManySortedSubset of the Sorts of T

for S being non void J -extension Signature

for Q being b

let T be MSAlgebra over J; :: thesis: for X being ManySortedSubset of the Sorts of T

for S being non void J -extension Signature

for Q being T -extension MSAlgebra over S holds X extended_by ({}, the carrier of S) is ManySortedSubset of the Sorts of Q

let X be ManySortedSubset of the Sorts of T; :: thesis: for S being non void J -extension Signature

for Q being T -extension MSAlgebra over S holds X extended_by ({}, the carrier of S) is ManySortedSubset of the Sorts of Q

let S be non void J -extension Signature; :: thesis: for Q being T -extension MSAlgebra over S holds X extended_by ({}, the carrier of S) is ManySortedSubset of the Sorts of Q

let Q be T -extension MSAlgebra over S; :: thesis: X extended_by ({}, the carrier of S) is ManySortedSubset of the Sorts of Q

let x be object ; :: according to PBOOLE:def 2,PBOOLE:def 18 :: thesis: ( not x in the carrier of S or (X extended_by ({}, the carrier of S)) . x c= the Sorts of Q . x )

assume A1: x in the carrier of S ; :: thesis: (X extended_by ({}, the carrier of S)) . x c= the Sorts of Q . x

then reconsider s = x as SortSymbol of S ;

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

end;

suppose A2:
s in the carrier of J
; :: thesis: (X extended_by ({}, the carrier of S)) . x c= the Sorts of Q . x

then
s in dom X
by PARTFUN1:def 2;

then s in dom (X | the carrier of S) by RELAT_1:57;

then A3: (X extended_by ({}, the carrier of S)) . x = (X | the carrier of S) . x by FUNCT_4:13

.= X . x by A1, FUNCT_1:49 ;

X . x c= the Sorts of T . x by A2, PBOOLE:def 18, PBOOLE:def 2;

hence (X extended_by ({}, the carrier of S)) . x c= the Sorts of Q . x by A2, A3, Th16; :: thesis: verum

end;then s in dom (X | the carrier of S) by RELAT_1:57;

then A3: (X extended_by ({}, the carrier of S)) . x = (X | the carrier of S) . x by FUNCT_4:13

.= X . x by A1, FUNCT_1:49 ;

X . x c= the Sorts of T . x by A2, PBOOLE:def 18, PBOOLE:def 2;

hence (X extended_by ({}, the carrier of S)) . x c= the Sorts of Q . x by A2, A3, Th16; :: thesis: verum

suppose A4:
s nin the carrier of J
; :: thesis: (X extended_by ({}, the carrier of S)) . x c= the Sorts of Q . x

A5:
J is Subsignature of S
by Def2;

dom (X | the carrier of S) = (dom X) /\ the carrier of S by RELAT_1:61

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

.= the carrier of J by A5, XBOOLE_1:28, INSTALG1:10 ;

then (X extended_by ({}, the carrier of S)) . x = ( the carrier of S --> {}) . x by A4, FUNCT_4:11

.= {} ;

hence (X extended_by ({}, the carrier of S)) . x c= the Sorts of Q . x ; :: thesis: verum

end;dom (X | the carrier of S) = (dom X) /\ the carrier of S by RELAT_1:61

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

.= the carrier of J by A5, XBOOLE_1:28, INSTALG1:10 ;

then (X extended_by ({}, the carrier of S)) . x = ( the carrier of S --> {}) . x by A4, FUNCT_4:11

.= {} ;

hence (X extended_by ({}, the carrier of S)) . x c= the Sorts of Q . x ; :: thesis: verum