let S be non empty non void ManySortedSign ; :: thesis: for U0 being MSAlgebra of S
for A being MSSubAlgebra of U0
for o being OperSymbol of S
for x being set st x in Args o,A holds
x in Args o,U0
let U0 be MSAlgebra of S; :: thesis: for A being MSSubAlgebra of U0
for o being OperSymbol of S
for x being set st x in Args o,A holds
x in Args o,U0
let A be MSSubAlgebra of U0; :: thesis: for o being OperSymbol of S
for x being set st x in Args o,A holds
x in Args o,U0
let o be OperSymbol of S; :: thesis: for x being set st x in Args o,A holds
x in Args o,U0
let x be set ; :: thesis: ( x in Args o,A implies x in Args o,U0 )
assume A1: x in Args o,A ; :: thesis: x in Args o,U0
reconsider B0 = the Sorts of A as MSSubset of U0 by MSUALG_2:def 10;
U0 is MSSubAlgebra of U0 by MSUALG_2:6;
then reconsider B1 = the Sorts of U0 as MSSubset of U0 by MSUALG_2:def 10;
B0 c= B1 by PBOOLE:def 23;
then ((B0 # ) * the Arity of S) . o c= ((B1 # ) * the Arity of S) . o by MSUALG_2:3;
hence x in Args o,U0 by A1; :: thesis: verum