let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for U0 being MSAlgebra over 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 over 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 over 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 )
reconsider a = the Arity of S . o as Element of the carrier of S * ;
A1: rng a c= the carrier of S by FINSEQ_1:def 4;
A2: dom B0 = the carrier of S by PARTFUN1:def 2;
then A3: dom (B0 * a) = dom a by A1, RELAT_1:27;
assume A4: B0 c= B1 ; :: thesis: ((B0 #) * the Arity of S) . o c= ((B1 #) * the Arity of S) . o
A5: for x being object st x in dom (B0 * a) holds
(B0 * a) . x c= (B1 * a) . x

proof

let x be object ; :: thesis: ( x in dom (B0 * a) implies (B0 * a) . x c= (B1 * a) . x )
assume A6: x in dom (B0 * a) ; :: thesis: (B0 * a) . x c= (B1 * a) . x
then a . x in rng a by A3, FUNCT_1:def 3;
then B0 . (a . x) c= B1 . (a . x) by A4, A1;
then (B0 * a) . x c= B1 . (a . x) by A3, A6, FUNCT_1:13;
hence (B0 * a) . x c= (B1 * a) . x by A3, A6, FUNCT_1:13; :: thesis: verum

end;

A7: dom the Arity of S = the carrier' of S by FUNCT_2:def 1;
then dom ((B0 #) * the Arity of S) = dom the Arity of S by PARTFUN1:def 2;
then ((B0 #) * the Arity of S) . o = (B0 #) . a by A7, FUNCT_1:12;
then A8: ((B0 #) * the Arity of S) . o = product (B0 * a) by FINSEQ_2:def 5;
dom ((B1 #) * the Arity of S) = dom the Arity of S by A7, PARTFUN1:def 2;
then ((B1 #) * the Arity of S) . o = (B1 #) . a by A7, FUNCT_1:12;
then A9: ((B1 #) * the Arity of S) . o = product (B1 * a) by FINSEQ_2:def 5;
dom B1 = the carrier of S by PARTFUN1:def 2;
then dom (B1 * a) = dom a by A1, RELAT_1:27;
hence ((B0 #) * the Arity of S) . o c= ((B1 #) * the Arity of S) . o by A8, A9, A2, A1, A5, CARD_3:27, RELAT_1:27; :: thesis: verum