let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for A being MSAlgebra over S
for a being Function st a in Args (o,A) holds
for i being 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 over S
for a being Function st a in Args (o,A) holds
for i being Nat
for x being Element of A,((the_arity_of o) /. i) holds a +* (i,x) in Args (o,A)
let A be MSAlgebra over S; :: thesis: for a being Function st a in Args (o,A) holds
for i being 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:3;
let a be Function; :: thesis: ( a in Args (o,A) implies for i being 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 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 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:3;
A5: now :: thesis: for j being object st j in dom a holds
(a +* (i,x)) . j in ( the Sorts of A * (the_arity_of o)) . j
let j be object ; :: thesis: ( j in dom a implies (a +* (i,x)) . b1 in ( the Sorts of A * (the_arity_of o)) . b1 )
assume A6: j in dom a ; :: thesis: (a +* (i,x)) . b1 in ( the Sorts of A * (the_arity_of o)) . b1
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:13;
A8: (the_arity_of o) /. k = (the_arity_of o) . k by A3, A6, PARTFUN1:def 6;
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)) . b1 in ( the Sorts of A * (the_arity_of o)) . b1
then (a +* (i,x)) . j = x by A6, FUNCT_7:31;
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)) . b1 in ( the Sorts of A * (the_arity_of o)) . b1
then (a +* (i,x)) . j = a . j by FUNCT_7:32;
hence (a +* (i,x)) . j in ( the Sorts of A * (the_arity_of o)) . j by A2, A4, A1, A3, A6, CARD_3:9; :: thesis: verum
end;
end;
end;
dom (a +* (i,x)) = dom a by FUNCT_7:30;
hence a +* (i,x) in Args (o,A) by A4, A1, A3, A5, CARD_3:9; :: thesis: verum