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 x be Element of Args (o,(product A)); :: thesis:
set C = union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } ;
consider x1 being Function such that
A1: x1 = x ;
x in Args (o,(product A)) ;
then A2: x in product ( the Sorts of (product A) * (the_arity_of o)) by PRALG_2:3;
dom (SORTS A) = the carrier of S by PARTFUN1:def 2;
then A3: rng (the_arity_of o) c= dom (SORTS A) ;

now :: thesis:

let c be object ; :: thesis:
assume c in rng x1 ; :: thesis:
then consider n being object such that
A4: n in dom x1 and
A5: x1 . n = c by FUNCT_1:def 3;
A6: n in dom ((SORTS A) * (the_arity_of o)) by A2, A1, A4, CARD_3:9;
then n in dom (the_arity_of o) by A3, RELAT_1:27;
then (the_arity_of o) . n in rng (the_arity_of o) by FUNCT_1:def 3;
then reconsider s1 = (the_arity_of o) . n as Element of the carrier of S ;
x1 . n in ((SORTS A) * (the_arity_of o)) . n by A2, A1, A6, CARD_3:9;
then x1 . n in (SORTS A) . s1 by A6, FUNCT_1:12;
then x1 . n in product (Carrier (A,s1)) by PRALG_2:def 10;
then consider g being Function such that
A7: g = x1 . n and
A8: dom g = dom (Carrier (A,s1)) and
A9: for i9 being object st i9 in dom (Carrier (A,s1)) holds
g . i9 in (Carrier (A,s1)) . i9 by CARD_3:def 5;

now :: thesis:

let c1 be object ; :: thesis:
assume c1 in rng g ; :: thesis:
then consider i1 being object such that
A10: i1 in dom g and
A11: g . i1 = c1 by FUNCT_1:def 3;
reconsider i1 = i1 as Element of I by A8, A10;
ex U0 being MSAlgebra over S st
( U0 = A . i1 & (Carrier (A,s1)) . i1 = the Sorts of U0 . s1 ) by PRALG_2:def 9;
then A12: g . i1 in the Sorts of (A . i1) . s1 by A8, A9, A10;
the Sorts of (A . i1) . s1 in { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } ;
hence c1 in union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } by A11, A12, TARSKI:def 4; :: thesis:

end;

then A13: rng g c= union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } ;
dom g = I by A8, PARTFUN1:def 2;
hence c in Funcs (I,(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )) by A5, A7, A13, FUNCT_2:def 2; :: thesis:

end;

then A14: rng x1 c= Funcs (I,(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )) ;
dom x = dom ((SORTS A) * (the_arity_of o)) by A2, CARD_3:9
.= dom (the_arity_of o) by A3, RELAT_1:27 ;
hence x in Funcs ((dom (the_arity_of o)),(Funcs (I,(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )))) by A1, A14, FUNCT_2:def 2; :: thesis: