let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra of 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 of 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 10;
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 23;
A1: Args o,B = ((SB # ) * the Arity of S) . o by MSUALG_1:def 9;
( SB c= SA & Args o,A = ((SA # ) * the Arity of S) . o ) by MSUALG_1:def 9, PBOOLE:def 23;
hence Args o,B c= Args o,A by A1, MSUALG_2:3; :: thesis: verum