let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty disjoint_valued MSAlgebra over S
for B being non-empty MSAlgebra over S
for o being OperSymbol of S
for p, q being Element of Args (o,A)
for h being ManySortedFunction of A,B
for a being Element of A
for i being Nat st i in dom p & q = p +* (i,a) holds
h # q = (h # p) +* (i,(h . a))
let A be non-empty disjoint_valued MSAlgebra over S; :: thesis: for B being non-empty MSAlgebra over S
for o being OperSymbol of S
for p, q being Element of Args (o,A)
for h being ManySortedFunction of A,B
for a being Element of A
for i being Nat st i in dom p & q = p +* (i,a) holds
h # q = (h # p) +* (i,(h . a))
let B be non-empty MSAlgebra over S; :: thesis: for o being OperSymbol of S
for p, q being Element of Args (o,A)
for h being ManySortedFunction of A,B
for a being Element of A
for i being Nat st i in dom p & q = p +* (i,a) holds
h # q = (h # p) +* (i,(h . a))
let o be OperSymbol of S; :: thesis: for p, q being Element of Args (o,A)
for h being ManySortedFunction of A,B
for a being Element of A
for i being Nat st i in dom p & q = p +* (i,a) holds
h # q = (h # p) +* (i,(h . a))
let p, q be Element of Args (o,A); :: thesis: for h being ManySortedFunction of A,B
for a being Element of A
for i being Nat st i in dom p & q = p +* (i,a) holds
h # q = (h # p) +* (i,(h . a))
let h be ManySortedFunction of A,B; :: thesis: for a being Element of A
for i being Nat st i in dom p & q = p +* (i,a) holds
h # q = (h # p) +* (i,(h . a))
let a be Element of A; :: thesis: for i being Nat st i in dom p & q = p +* (i,a) holds
h # q = (h # p) +* (i,(h . a))
let i be Nat; :: thesis: ( i in dom p & q = p +* (i,a) implies h # q = (h # p) +* (i,(h . a)) )
assume Z0: i in dom p ; :: thesis: ( not q = p +* (i,a) or h # q = (h # p) +* (i,(h . a)) )
assume Z1: q = p +* (i,a) ; :: thesis: h # q = (h # p) +* (i,(h . a))
A1: ( dom (h # q) = dom (the_arity_of o) & dom (the_arity_of o) = dom (h # p) & dom (h # p) = dom ((h # p) +* (i,(h . a))) & dom q = dom (the_arity_of o) & dom (the_arity_of o) = dom p ) by MSUALG_3:6, FUNCT_7:30;

now :: thesis: for j being object st j in dom (h # q) holds
(h # q) . j = ((h # p) +* (i,(h . a))) . j

let j be object ; :: thesis: ( j in dom (h # q) implies (h # q) . b₁ = ((h # p) +* (i,(h . a))) . b₁ )
assume A2: j in dom (h # q) ; :: thesis: (h # q) . b₁ = ((h # p) +* (i,(h . a))) . b₁
then reconsider k = j as Nat ;
A3: ( (h # q) . k = (h . ((the_arity_of o) /. k)) . (q . k) & (h # p) . k = (h . ((the_arity_of o) /. k)) . (p . k) ) by A1, A2, MSUALG_3:def 6;
q . i = a by Z0, Z1, FUNCT_7:31;
then a in the Sorts of A . ((the_arity_of o) /. i) by Z0, A1, MSUALG_6:2;
then the_sort_of a = (the_arity_of o) /. i by SORT;
then A5: (h . ((the_arity_of o) /. i)) . a = h . a by ABBR;

per cases ( j = i or j <> i ) ;

suppose A4: j = i ; :: thesis: (h # q) . b₁ = ((h # p) +* (i,(h . a))) . b₁

hence (h # q) . j = (h . ((the_arity_of o) /. k)) . a by Z1, A1, A2, A3, FUNCT_7:31
.= ((h # p) +* (i,(h . a))) . j by A4, A5, A1, A2, FUNCT_7:31 ;
:: thesis: verum

end;

suppose A6: j <> i ; :: thesis: (h # q) . b₁ = ((h # p) +* (i,(h . a))) . b₁

hence (h # q) . j = (h . ((the_arity_of o) /. k)) . (p . k) by Z1, A3, FUNCT_7:32
.= ((h # p) +* (i,(h . a))) . j by A3, A6, FUNCT_7:32 ;
:: thesis: verum

end;

end;

end;

hence h # q = (h # p) +* (i,(h . a)) by A1, FUNCT_1:2; :: thesis: verum