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 holds Union (X extended_by ({}, the carrier of S)) = Union X
let T be MSAlgebra over J; :: thesis: for X being ManySortedSubset of the Sorts of T
for S being non void J -extension Signature holds Union (X extended_by ({}, the carrier of S)) = Union X
let X be ManySortedSubset of the Sorts of T; :: thesis: for S being non void J -extension Signature holds Union (X extended_by ({}, the carrier of S)) = Union X
let S be non void J -extension Signature; :: thesis: Union (X extended_by ({}, the carrier of S)) = Union X
set Y = X extended_by ({}, the carrier of S);
A1: J is Subsignature of S by Def2;
dom X = the carrier of J by PARTFUN1:def 2;
then A2: X | the carrier of S = X by A1, RELAT_1:68, INSTALG1:10;
then rng (X extended_by ({}, the carrier of S)) c= (rng ( the carrier of S --> {})) \/ (rng X) by FUNCT_4:17;
then ( Union (X extended_by ({}, the carrier of S)) c= union ({{}} \/ (rng X)) & union ({{}} \/ (rng X)) = (union {{}}) \/ (Union X) & (union {{}}) \/ (Union X) = {} \/ (Union X) ) by ZFMISC_1:77, ZFMISC_1:78;
hence Union (X extended_by ({}, the carrier of S)) c= Union X ; :: according to XBOOLE_0:def 10 :: thesis: Union X c= Union (X extended_by ({}, the carrier of S))
X c= X extended_by ({}, the carrier of S) by A2, FUNCT_4:25;
hence Union X c= Union (X extended_by ({}, the carrier of S)) by RELAT_1:11, ZFMISC_1:77; :: thesis: verum