let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for U0 being MSAlgebra of S
for B0, B1 being MSSubset of U0 st B0 c= B1 holds
((B0 # ) * the Arity of S) . o c= ((B1 # ) * the Arity of S) . o
let o be OperSymbol of S; :: thesis: for U0 being MSAlgebra of S
for B0, B1 being MSSubset of U0 st B0 c= B1 holds
((B0 # ) * the Arity of S) . o c= ((B1 # ) * the Arity of S) . o
let U0 be MSAlgebra of S; :: thesis: for B0, B1 being MSSubset of U0 st B0 c= B1 holds
((B0 # ) * the Arity of S) . o c= ((B1 # ) * the Arity of S) . o
let B0, B1 be MSSubset of U0; :: thesis: ( B0 c= B1 implies ((B0 # ) * the Arity of S) . o c= ((B1 # ) * the Arity of S) . o )
assume A1: B0 c= B1 ; :: thesis: ((B0 # ) * the Arity of S) . o c= ((B1 # ) * the Arity of S) . o
A2: ( rng the Arity of S c= the carrier of S * & dom the Arity of S = the carrier' of S ) by FUNCT_2:def 1, RELAT_1:def 19;
then A3: ( dom ((B0 # ) * the Arity of S) = dom the Arity of S & dom ((B1 # ) * the Arity of S) = dom the Arity of S ) by PARTFUN1:def 4;
reconsider a = the Arity of S . o as Element of the carrier of S * ;
( ((B0 # ) * the Arity of S) . o = (B0 # ) . a & ((B1 # ) * the Arity of S) . o = (B1 # ) . a ) by A2, A3, FUNCT_1:22;
then A5: ( ((B0 # ) * the Arity of S) . o = product (B0 * a) & ((B1 # ) * the Arity of S) . o = product (B1 * a) ) by PBOOLE:def 19;
A6: ( dom B0 = the carrier of S & dom B1 = the carrier of S ) by PARTFUN1:def 4;
A7: rng a c= the carrier of S by FINSEQ_1:def 4;
then A8: ( dom (B0 * a) = dom a & dom (B1 * a) = dom a ) by A6, RELAT_1:46;
for x being set st x in dom (B0 * a) holds
(B0 * a) . x c= (B1 * a) . x

proof

let x be set ; :: thesis: ( x in dom (B0 * a) implies (B0 * a) . x c= (B1 * a) . x )
assume A9: x in dom (B0 * a) ; :: thesis: (B0 * a) . x c= (B1 * a) . x
then a . x in rng a by A8, FUNCT_1:def 5;
then B0 . (a . x) c= B1 . (a . x) by A1, A7, PBOOLE:def 5;
then (B0 * a) . x c= B1 . (a . x) by A8, A9, FUNCT_1:23;
hence (B0 * a) . x c= (B1 * a) . x by A8, A9, FUNCT_1:23; :: thesis: verum

end;

hence ((B0 # ) * the Arity of S) . o c= ((B1 # ) * the Arity of S) . o by A5, A8, CARD_3:38; :: thesis: verum