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 (Frege (A ?. o)) = product (doms (A ?. o)) by PARTFUN1:def 4;
A3: dom (A ?. o) = I by PARTFUN1:def 4;
A4: SubFuncs (rng (A ?. o)) = rng (A ?. o)

proof

thus SubFuncs (rng (A ?. o)) c= rng (A ?. o) by FUNCT_6:27; :: according to XBOOLE_0:def 10 :: thesis:
let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A5: x in rng (A ?. o) ; :: thesis:
then ex j being set st
( j in dom (A ?. o) & x = (A ?. o) . j ) by FUNCT_1:def 5;
hence x in SubFuncs (rng (A ?. o)) by A5, FUNCT_6:def 1; :: thesis:

end;

A6: dom (doms (A ?. o)) = (A ?. o) " (SubFuncs (rng (A ?. o))) by FUNCT_6:def 2
.= dom (A ?. o) by A4, RELAT_1:169 ;
hence dom f = I by A1, A2, A3, CARD_3:18; :: thesis:
thus A7: for i being Element of I holds f . i in Args o,(A . i) :: thesis:

proof

let i be Element of I; :: thesis:
A8: (A ?. o) . i = Den o,(A . i) by Th14;
f . i in (doms (A ?. o)) . i by A1, A2, A3, A6, CARD_3:18;
then f . i in dom (Den o,(A . i)) by A3, A8, FUNCT_6:31;
hence f . i in Args o,(A . i) by FUNCT_2:def 1; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng f ; :: thesis:
then consider y being set such that
A9: ( y in dom f & x = f . y ) by FUNCT_1:def 5;
reconsider y = y as Element of I by A1, A2, A3, A6, A9, CARD_3:18;
A10: x in Args o,(A . y) by A7, A9;
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;
A12: ( dom the Arity of S = the carrier' of S & rng the Arity of S c= the carrier of S * ) by FUNCT_2:def 1, RELAT_1:def 19;
then A13: dom ((the Sorts of (A . y) # ) * the Arity of S) = dom the Arity of S by PARTFUN1:def 4;
Args o,(A . y) = ((the Sorts of (A . y) # ) * the Arity of S) . o by MSUALG_1:def 9
.= (the Sorts of (A . y) # ) . (the Arity of S . o) by A12, A13, FUNCT_1:22
.= (the Sorts of (A . y) # ) . (the_arity_of o) by MSUALG_1:def 6
.= product (the Sorts of (A . y) * (the_arity_of o)) by PBOOLE:def 19 ;
then consider g being Function such that
A14: ( g = x & dom g = dom (the Sorts of (A . y) * (the_arity_of o)) & ( for i being set 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;
A15: ( dom (the_arity_of o) = dom (the_arity_of o) & rng (the_arity_of o) c= the carrier of S ) by FINSEQ_1:def 4;
A16: dom the Sorts of (A . y) = the carrier of S by PARTFUN1:def 4;
then A17: ( dom (the Sorts of (A . y) * (the_arity_of o)) = dom (the_arity_of o) & rng (the Sorts of (A . y) * (the_arity_of o)) c= rng the Sorts of (A . y) ) by A15, RELAT_1:45, RELAT_1:46;
A18: rng g c= |.(A . y).|

proof

let i be set ; :: according to TARSKI:def 3 :: thesis:
assume i in rng g ; :: thesis:
then consider j being set such that
A19: ( j in dom g & g . j = i ) by FUNCT_1:def 5;
i in (the Sorts of (A . y) * (the_arity_of o)) . j by A14, A19;
then A20: i in the Sorts of (A . y) . ((the_arity_of o) . j) by A14, A19, FUNCT_1:22;
(the_arity_of o) . j in rng (the_arity_of o) by A14, A17, A19, FUNCT_1:def 5;
then the Sorts of (A . y) . ((the_arity_of o) . j) in rng the Sorts of (A . y) by A15, A16, FUNCT_1:def 5;
hence i in |.(A . y).| by A20, 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:92;
then rng g c= |.A.| by A18, XBOOLE_1:1;
hence x in Funcs (dom (the_arity_of o)),|.A.| by A14, A17, FUNCT_2:def 2; :: thesis: