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

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