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 b1 -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 ;
per cases ( s in the carrier of J or s nin the carrier of J ) ;
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;
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;
end;