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
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 A1: 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
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
A2: ( Args o,A = product (the Sorts of A * (the_arity_of o)) & dom (the Sorts of A * (the_arity_of o)) = dom (the_arity_of o) ) by PRALG_2:10;
A3: dom a = dom (the_arity_of o) by A1, Th2;
A4: dom (a +* i,x) = dom a by FUNCT_7:32;

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 A5: 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;
A6: ( (the_arity_of o) /. k = (the_arity_of o) . k & (the Sorts of A * (the_arity_of o)) . k = the Sorts of A . ((the_arity_of o) . k) ) by A3, A5, FUNCT_1:23, PARTFUN1:def 8;
then A7: (the Sorts of A * (the_arity_of o)) . j <> {} by A1, A3, A5, Th3;

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

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

then (a +* i,x) . j = x by A5, FUNCT_7:33;
hence (a +* i,x) . j in (the Sorts of A * (the_arity_of o)) . j by A6, A7, A8; :: 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 A1, A2, A3, A5, CARD_3:18; :: thesis: verum

end;

end;

end;

hence a +* i,x in Args o,A by A2, A3, A4, CARD_3:18; :: thesis: verum