let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for U0 being MSAlgebra of S
for A, B being MSSubset of U0 st B in SubSort A holds
(((MSSubSort A) # ) * the Arity of S) . o c= ((B # ) * the Arity of S) . o
let o be OperSymbol of S; :: thesis: for U0 being MSAlgebra of S
for A, B being MSSubset of U0 st B in SubSort A holds
(((MSSubSort A) # ) * the Arity of S) . o c= ((B # ) * the Arity of S) . o
let U0 be MSAlgebra of S; :: thesis: for A, B being MSSubset of U0 st B in SubSort A holds
(((MSSubSort A) # ) * the Arity of S) . o c= ((B # ) * the Arity of S) . o
let A, B be MSSubset of U0; :: thesis: ( B in SubSort A implies (((MSSubSort A) # ) * the Arity of S) . o c= ((B # ) * the Arity of S) . o )
assume A1: B in SubSort A ; :: thesis: (((MSSubSort A) # ) * the Arity of S) . o c= ((B # ) * the Arity of S) . o
MSSubSort A c= B

proof

let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in the carrier of S or (MSSubSort A) . i c= B . i )
assume i in the carrier of S ; :: thesis: (MSSubSort A) . i c= B . i
then reconsider s = i as SortSymbol of S ;
( (MSSubSort A) . s = meet (SubSort A,s) & B . s in SubSort A,s ) by A1, Def14, Def15;
hence (MSSubSort A) . i c= B . i by SETFAM_1:4; :: thesis: verum

end;

hence (((MSSubSort A) # ) * the Arity of S) . o c= ((B # ) * the Arity of S) . o by Th3; :: thesis: verum