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 ;
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 ;
then B0 . (a . x) c= B1 . (a . x) by A4, A1;
then (B0 * a) . x c= B1 . (a . x) by ;
hence (B0 * a) . x c= (B1 * a) . x by ; :: 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 ;
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 ;
then ((B1 #) * the Arity of S) . o = (B1 #) . a by ;
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 ;
hence ((B0 #) * the Arity of S) . o c= ((B1 #) * the Arity of S) . o by ; :: thesis: verum