let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for A being MSAlgebra over S holds
( Args (o,A) <> {} iff for i being Element of NAT st i in dom (the_arity_of o) holds
the Sorts of A . ((the_arity_of o) /. i) <> {} )
let o be OperSymbol of S; :: thesis: for A being MSAlgebra over S holds
( Args (o,A) <> {} iff for i being Element of NAT st i in dom (the_arity_of o) holds
the Sorts of A . ((the_arity_of o) /. i) <> {} )
let A be MSAlgebra over S; :: thesis: ( Args (o,A) <> {} iff for i being Element of NAT st i in dom (the_arity_of o) holds
the Sorts of A . ((the_arity_of o) /. i) <> {} )
A1: dom ( the Sorts of A * (the_arity_of o)) = dom (the_arity_of o) by PRALG_2:3;
A2: Args (o,A) = product ( the Sorts of A * (the_arity_of o)) by PRALG_2:3;

hereby :: thesis: ( ( for i being Element of NAT st i in dom (the_arity_of o) holds
the Sorts of A . ((the_arity_of o) /. i) <> {} ) implies Args (o,A) <> {} )

assume A3: Args (o,A) <> {} ; :: thesis: for i being Element of NAT st i in dom (the_arity_of o) holds
the Sorts of A . ((the_arity_of o) /. i) <> {}
let i be Element of NAT ; :: thesis: ( i in dom (the_arity_of o) implies the Sorts of A . ((the_arity_of o) /. i) <> {} )
assume A4: i in dom (the_arity_of o) ; :: thesis: the Sorts of A . ((the_arity_of o) /. i) <> {}
then A5: the Sorts of A . ((the_arity_of o) . i) = ( the Sorts of A * (the_arity_of o)) . i by FUNCT_1:13;
A6: (the_arity_of o) /. i = (the_arity_of o) . i by A4, PARTFUN1:def 6;
( the Sorts of A * (the_arity_of o)) . i in rng ( the Sorts of A * (the_arity_of o)) by A1, A4, FUNCT_1:def 3;
hence the Sorts of A . ((the_arity_of o) /. i) <> {} by A2, A3, A5, A6, CARD_3:26; :: thesis: verum

end;

assume A7: for i being Element of NAT st i in dom (the_arity_of o) holds
the Sorts of A . ((the_arity_of o) /. i) <> {} ; :: thesis: Args (o,A) <> {}
assume Args (o,A) = {} ; :: thesis: contradiction
then {} in rng ( the Sorts of A * (the_arity_of o)) by A2, CARD_3:26;
then consider x being object such that
A8: x in dom (the_arity_of o) and
A9: {} = ( the Sorts of A * (the_arity_of o)) . x by A1, FUNCT_1:def 3;
reconsider x = x as Element of NAT by A8;
A10: (the_arity_of o) /. x = (the_arity_of o) . x by A8, PARTFUN1:def 6;
the Sorts of A . ((the_arity_of o) /. x) <> {} by A7, A8;
hence contradiction by A8, A9, A10, FUNCT_1:13; :: thesis: verum