let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for A being MSAlgebra of S
for a being Function st a in Args o,A holds
for i being Element of NAT
for x being Element of A,((the_arity_of o) /. i) holds a +* i,x in Args o,A
let o be OperSymbol of S; :: thesis: for A being MSAlgebra of S
for a being Function st a in Args o,A holds
for i being Element of NAT
for x being Element of A,((the_arity_of o) /. i) holds a +* i,x in Args o,A
let A be MSAlgebra of S; :: thesis: for a being Function st a in Args o,A holds
for i being Element of NAT
for x being Element of A,((the_arity_of o) /. i) holds a +* i,x in Args o,A
A1: dom (the Sorts of A * (the_arity_of o)) = dom (the_arity_of o) by PRALG_2:10;
let a be Function; :: thesis: ( a in Args o,A implies for i being Element of NAT
for x being Element of A,((the_arity_of o) /. i) holds a +* i,x in Args o,A )
assume A2: a in Args o,A ; :: thesis: for i being Element of NAT
for x being Element of A,((the_arity_of o) /. i) holds a +* i,x in Args o,A
A3: dom a = dom (the_arity_of o) by A2, Th2;
let i be Element of NAT ; :: thesis: for x being Element of A,((the_arity_of o) /. i) holds a +* i,x in Args o,A
let x be Element of A,((the_arity_of o) /. i); :: thesis: a +* i,x in Args o,A
A4: Args o,A = product (the Sorts of A * (the_arity_of o)) by PRALG_2:10;

A5: now

let j be set ; :: thesis: ( j in dom a implies (a +* i,x) . b₁ in (the Sorts of A * (the_arity_of o)) . b₁ )
assume A6: j in dom a ; :: thesis: (a +* i,x) . b₁ in (the Sorts of A * (the_arity_of o)) . b₁
then reconsider k = j as Element of NAT by A3;
A7: (the Sorts of A * (the_arity_of o)) . k = the Sorts of A . ((the_arity_of o) . k) by A3, A6, FUNCT_1:23;
A8: (the_arity_of o) /. k = (the_arity_of o) . k by A3, A6, PARTFUN1:def 8;
then A9: (the Sorts of A * (the_arity_of o)) . j <> {} by A2, A3, A6, A7, Th3;

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

suppose A10: j = i ; :: thesis: (a +* i,x) . b₁ in (the Sorts of A * (the_arity_of o)) . b₁

then (a +* i,x) . j = x by A6, FUNCT_7:33;
hence (a +* i,x) . j in (the Sorts of A * (the_arity_of o)) . j by A8, A7, A9, A10; :: thesis: verum

end;

suppose j <> i ; :: thesis: (a +* i,x) . b₁ in (the Sorts of A * (the_arity_of o)) . b₁

then (a +* i,x) . j = a . j by FUNCT_7:34;
hence (a +* i,x) . j in (the Sorts of A * (the_arity_of o)) . j by A2, A4, A1, A3, A6, CARD_3:18; :: thesis: verum

end;

end;

end;

dom (a +* i,x) = dom a by FUNCT_7:32;
hence a +* i,x in Args o,A by A4, A1, A3, A5, CARD_3:18; :: thesis: verum