let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for U0 being MSAlgebra over 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 over 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 over 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 object ; :: according to PBOOLE:def 2 :: 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, Def13, Def14;
hence (MSSubSort A) . i c= B . i by SETFAM_1:3; :: thesis: verum

end;

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