let I be non empty set ; :: thesis:
let S be non empty non void ManySortedSign ; :: thesis:
let A be MSAlgebra-Family of I,S; :: thesis:
let o be OperSymbol of S; :: thesis:
let f be Function; :: thesis:
assume A1: f in dom (Frege (A ?. o)) ; :: thesis:
A2: dom (A ?. o) = I by PARTFUN1:def 2;
A3: dom (Frege (A ?. o)) = product (doms (A ?. o)) by PARTFUN1:def 2;
A4: dom (doms (A ?. o)) = dom (A ?. o) by FUNCT_6:def 2;
hence dom f = I by A1, A3, A2, CARD_3:9; :: thesis:
thus A5: for i being Element of I holds f . i in Args (o,(A . i)) :: thesis:

proof

let i be Element of I; :: thesis:
( (A ?. o) . i = Den (o,(A . i)) & f . i in (doms (A ?. o)) . i ) by A1, A3, A2, A4, Th7, CARD_3:9;
then f . i in dom (Den (o,(A . i))) by A2, FUNCT_6:22;
hence f . i in Args (o,(A . i)) by FUNCT_2:def 1; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng f ; :: thesis:
then consider y being object such that
A6: y in dom f and
A7: x = f . y by FUNCT_1:def 3;
reconsider y = y as Element of I by A1, A3, A2, A4, A6, CARD_3:9;
set X = the carrier' of S;
set AS = ( the Sorts of (A . y) #) * the Arity of S;
set Ar = the Arity of S;
set Cr = the carrier of S;
set So = the Sorts of (A . y);
set a = the_arity_of o;
A8: dom the Arity of S = the carrier' of S by FUNCT_2:def 1;
then A9: dom (( the Sorts of (A . y) #) * the Arity of S) = dom the Arity of S by PARTFUN1:def 2;
A10: Args (o,(A . y)) = (( the Sorts of (A . y) #) * the Arity of S) . o by MSUALG_1:def 4
.= ( the Sorts of (A . y) #) . ( the Arity of S . o) by A8, A9, FUNCT_1:12
.= ( the Sorts of (A . y) #) . (the_arity_of o) by MSUALG_1:def 1
.= product ( the Sorts of (A . y) * (the_arity_of o)) by FINSEQ_2:def 5 ;
x in Args (o,(A . y)) by A5, A7;
then consider g being Function such that
A11: g = x and
A12: dom g = dom ( the Sorts of (A . y) * (the_arity_of o)) and
A13: for i being object st i in dom ( the Sorts of (A . y) * (the_arity_of o)) holds
g . i in ( the Sorts of (A . y) * (the_arity_of o)) . i by A10, CARD_3:def 5;
A14: ( rng (the_arity_of o) c= the carrier of S & dom the Sorts of (A . y) = the carrier of S ) by FINSEQ_1:def 4, PARTFUN1:def 2;
then A15: dom ( the Sorts of (A . y) * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27;
A16: rng g c= |.(A . y).|

proof

let i be object ; :: according to TARSKI:def 3 :: thesis:
assume i in rng g ; :: thesis:
then consider j being object such that
A17: j in dom g and
A18: g . j = i by FUNCT_1:def 3;
(the_arity_of o) . j in rng (the_arity_of o) by A12, A15, A17, FUNCT_1:def 3;
then A19: the Sorts of (A . y) . ((the_arity_of o) . j) in rng the Sorts of (A . y) by A14, FUNCT_1:def 3;
i in ( the Sorts of (A . y) * (the_arity_of o)) . j by A12, A13, A17, A18;
then i in the Sorts of (A . y) . ((the_arity_of o) . j) by A12, A17, FUNCT_1:12;
hence i in |.(A . y).| by A19, TARSKI:def 4; :: thesis:

end;

|.(A . y).| in { |.(A . i).| where i is Element of I : verum } ;
then |.(A . y).| c= union { |.(A . i).| where i is Element of I : verum } by ZFMISC_1:74;
then rng g c= |.A.| by A16;
hence x in Funcs ((dom (the_arity_of o)),|.A.|) by A11, A12, A15, FUNCT_2:def 2; :: thesis: