let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for A being MSAlgebra of 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 of 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 of 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:10;
A2: Args o,A = product (the Sorts of A * (the_arity_of o)) by PRALG_2:10;

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:23;
A6: (the_arity_of o) /. i = (the_arity_of o) . i by A4, PARTFUN1:def 8;
(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 5;
hence the Sorts of A . ((the_arity_of o) /. i) <> {} by A2, A3, A5, A6, CARD_3:37; :: 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:37;
then consider x being set 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 5;
reconsider x = x as Element of NAT by A8;
A10: (the_arity_of o) /. x = (the_arity_of o) . x by A8, PARTFUN1:def 8;
the Sorts of A . ((the_arity_of o) /. x) <> {} by A7, A8;
hence contradiction by A8, A9, A10, FUNCT_1:23; :: thesis: verum