let MS be non void 1 -element segmental ManySortedSign ; :: thesis: for i being OperSymbol of MS
for A being non-empty MSAlgebra over MS holds Args (i,A) = (len (the_arity_of i)) -tuples_on (the_sort_of A)
let i be OperSymbol of MS; :: thesis: for A being non-empty MSAlgebra over MS holds Args (i,A) = (len (the_arity_of i)) -tuples_on (the_sort_of A)
let A be non-empty MSAlgebra over MS; :: thesis: Args (i,A) = (len (the_arity_of i)) -tuples_on (the_sort_of A)
set m = len (the_arity_of i);
dom the Arity of MS = the carrier' of MS by FUNCT_2:def 1;
then A1: Args (i,A) = ( the Sorts of A #) . ( the Arity of MS . i) by FUNCT_1:13
.= product ( the Sorts of A * (the_arity_of i)) by FINSEQ_2:def 5 ;
A2: rng (the_arity_of i) c= the carrier of MS by FINSEQ_1:def 4;
then rng (the_arity_of i) c= dom the Sorts of A by PARTFUN1:def 2;
then A3: dom ( the Sorts of A * (the_arity_of i)) = dom (the_arity_of i) by RELAT_1:27;
A4: ex n being Nat st dom (the_arity_of i) = Seg n by FINSEQ_1:def 2;
thus Args (i,A) c= (len (the_arity_of i)) -tuples_on (the_sort_of A) :: according to XBOOLE_0:def 10 :: thesis: (len (the_arity_of i)) -tuples_on (the_sort_of A) c= Args (i,A)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Args (i,A) or x in (len (the_arity_of i)) -tuples_on (the_sort_of A) )
assume x in Args (i,A) ; :: thesis: x in (len (the_arity_of i)) -tuples_on (the_sort_of A)
then consider g being Function such that
A5: x = g and
A6: dom g = dom ( the Sorts of A * (the_arity_of i)) and
A7: for j being object st j in dom ( the Sorts of A * (the_arity_of i)) holds
g . j in ( the Sorts of A * (the_arity_of i)) . j by A1, CARD_3:def 5;
reconsider p = g as FinSequence by A4, A3, A6, FINSEQ_1:def 2;
rng p c= the_sort_of A

proof

let j be object ; :: according to TARSKI:def 3 :: thesis: ( not j in rng p or j in the_sort_of A )
assume j in rng p ; :: thesis: j in the_sort_of A
then consider u being object such that
A8: u in dom g and
A9: p . u = j by FUNCT_1:def 3;
(the_arity_of i) . u in rng (the_arity_of i) by A3, A6, A8, FUNCT_1:def 3;
then A10: the Sorts of A . ((the_arity_of i) . u) is Component of the Sorts of A by A2, PBOOLE:139;
g . u in ( the Sorts of A * (the_arity_of i)) . u by A6, A7, A8;
then g . u in the Sorts of A . ((the_arity_of i) . u) by A3, A6, A8, FUNCT_1:13;
hence j in the_sort_of A by A9, A10, Def12; :: thesis: verum

end;

then A11: p is FinSequence of the_sort_of A by FINSEQ_1:def 4;
len p = len (the_arity_of i) by A3, A6, FINSEQ_3:29;
then x is Element of (len (the_arity_of i)) -tuples_on (the_sort_of A) by A5, A11, FINSEQ_2:92;
hence x in (len (the_arity_of i)) -tuples_on (the_sort_of A) ; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (len (the_arity_of i)) -tuples_on (the_sort_of A) or x in Args (i,A) )
assume x in (len (the_arity_of i)) -tuples_on (the_sort_of A) ; :: thesis: x in Args (i,A)
then x in Funcs ((Seg (len (the_arity_of i))),(the_sort_of A)) by FINSEQ_2:93;
then consider g being Function such that
A12: x = g and
A13: dom g = Seg (len (the_arity_of i)) and
A14: rng g c= the_sort_of A by FUNCT_2:def 2;
A15: dom g = dom ( the Sorts of A * (the_arity_of i)) by A3, A13, FINSEQ_1:def 3;

now :: thesis: for x being object st x in dom ( the Sorts of A * (the_arity_of i)) holds
g . x in ( the Sorts of A * (the_arity_of i)) . x

let x be object ; :: thesis: ( x in dom ( the Sorts of A * (the_arity_of i)) implies g . x in ( the Sorts of A * (the_arity_of i)) . x )
assume A16: x in dom ( the Sorts of A * (the_arity_of i)) ; :: thesis: g . x in ( the Sorts of A * (the_arity_of i)) . x
then (the_arity_of i) . x in rng (the_arity_of i) by A3, FUNCT_1:def 3;
then A17: the Sorts of A . ((the_arity_of i) . x) is Component of the Sorts of A by A2, PBOOLE:139;
g . x in rng g by A15, A16, FUNCT_1:def 3;
then g . x in the_sort_of A by A14;
then g . x in the Sorts of A . ((the_arity_of i) . x) by A17, Def12;
hence g . x in ( the Sorts of A * (the_arity_of i)) . x by A3, A16, FUNCT_1:13; :: thesis: verum

end;

hence x in Args (i,A) by A1, A12, A15, CARD_3:9; :: thesis: verum