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 ;
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)) = () \/ () & () \/ () = {} \/ () ) by ;
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 ;
hence Union X c= Union (X extended_by ({}, the carrier of S)) by ; :: thesis: verum