let S1 be OrderSortedSign; :: thesis: for OU0 being OSAlgebra of S1
for o being OperSymbol of S1
for A, B being OSSubset of OU0 st B in OSSubSort A holds
(((OSMSubSort A) #) * the Arity of S1) . o c= ((B #) * the Arity of S1) . o
let OU0 be OSAlgebra of S1; :: thesis: for o being OperSymbol of S1
for A, B being OSSubset of OU0 st B in OSSubSort A holds
(((OSMSubSort A) #) * the Arity of S1) . o c= ((B #) * the Arity of S1) . o
let o be OperSymbol of S1; :: thesis: for A, B being OSSubset of OU0 st B in OSSubSort A holds
(((OSMSubSort A) #) * the Arity of S1) . o c= ((B #) * the Arity of S1) . o
let A, B be OSSubset of OU0; :: thesis: ( B in OSSubSort A implies (((OSMSubSort A) #) * the Arity of S1) . o c= ((B #) * the Arity of S1) . o )
assume A1: B in OSSubSort A ; :: thesis: (((OSMSubSort A) #) * the Arity of S1) . o c= ((B #) * the Arity of S1) . o
OSMSubSort A c= B

proof

let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in the carrier of S1 or (OSMSubSort A) . i c= B . i )
assume i in the carrier of S1 ; :: thesis: (OSMSubSort A) . i c= B . i
then reconsider s = i as SortSymbol of S1 ;
( (OSMSubSort A) . s = meet (OSSubSort (A,s)) & B . s in OSSubSort (A,s) ) by A1, Def10, Def11;
hence (OSMSubSort A) . i c= B . i by SETFAM_1:3; :: thesis: verum

end;

hence (((OSMSubSort A) #) * the Arity of S1) . o c= ((B #) * the Arity of S1) . o by MSUALG_2:2; :: thesis: verum