let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra over S
for B being MSSubAlgebra of A
for o being OperSymbol of S holds Args (o,B) c= Args (o,A)
let A be MSAlgebra over S; :: thesis: for B being MSSubAlgebra of A
for o being OperSymbol of S holds Args (o,B) c= Args (o,A)
let B be MSSubAlgebra of A; :: thesis: for o being OperSymbol of S holds Args (o,B) c= Args (o,A)
reconsider SB = the Sorts of B as MSSubset of A by MSUALG_2:def 9;
let o be OperSymbol of S; :: thesis: Args (o,B) c= Args (o,A)
reconsider SA = the Sorts of A as MSSubset of A by PBOOLE:def 18;
A1: Args (o,B) = ((SB #) * the Arity of S) . o by MSUALG_1:def 4;
( SB c= SA & Args (o,A) = ((SA #) * the Arity of S) . o ) by MSUALG_1:def 4, PBOOLE:def 18;
hence Args (o,B) c= Args (o,A) by A1, MSUALG_2:2; :: thesis: verum