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: ( 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;

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 A2: 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 i in dom (the_arity_of o) ; :: thesis: the Sorts of A . ((the_arity_of o) /. i) <> {}
then ( the Sorts of A . ((the_arity_of o) . i) = (the Sorts of A * (the_arity_of o)) . i & (the Sorts of A * (the_arity_of o)) . i in rng (the Sorts of A * (the_arity_of o)) & (the_arity_of o) /. i = (the_arity_of o) . i ) by A1, FUNCT_1:23, FUNCT_1:def 5, PARTFUN1:def 8;
hence the Sorts of A . ((the_arity_of o) /. i) <> {} by A1, A2, CARD_3:37; :: thesis: verum

end;

assume A3: 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 A1, CARD_3:37;
then consider x being set such that
A4: ( x in dom (the_arity_of o) & {} = (the Sorts of A * (the_arity_of o)) . x ) by A1, FUNCT_1:def 5;
reconsider x = x as Element of NAT by A4;
( (the_arity_of o) /. x = (the_arity_of o) . x & the Sorts of A . ((the_arity_of o) /. x) <> {} ) by A3, A4, PARTFUN1:def 8;
hence contradiction by A4, FUNCT_1:23; :: thesis: verum