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:10;
dom (SORTS A) = the carrier of S by PARTFUN1:def 4;
then A3: rng (the_arity_of o) c= dom (SORTS A) ;

now

let c be set ; :: thesis:
assume c in rng x1 ; :: thesis:
then consider n being set such that
A4: n in dom x1 and
A5: x1 . n = c by FUNCT_1:def 5;
A6: n in dom ((SORTS A) * (the_arity_of o)) by A2, A1, A4, CARD_3:18;
then n in dom (the_arity_of o) by A3, RELAT_1:46;
then (the_arity_of o) . n in rng (the_arity_of o) by FUNCT_1:def 5;
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:18;
then x1 . n in (SORTS A) . s1 by A6, FUNCT_1:22;
then x1 . n in product (Carrier A,s1) by PRALG_2:def 17;
then consider g being Function such that
A7: g = x1 . n and
A8: dom g = dom (Carrier A,s1) and
A9: for i9 being set st i9 in dom (Carrier A,s1) holds
g . i9 in (Carrier A,s1) . i9 by CARD_3:def 5;

now

let c1 be set ; :: thesis:
assume c1 in rng g ; :: thesis:
then consider i1 being set such that
A10: i1 in dom g and
A11: g . i1 = c1 by FUNCT_1:def 5;
reconsider i1 = i1 as Element of I by A8, A10, PARTFUN1:def 4;
ex U0 being MSAlgebra of S st
( U0 = A . i1 & (Carrier A,s1) . i1 = the Sorts of U0 . s1 ) by PRALG_2:def 16;
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 } by TARSKI:def 3;
dom g = I by A8, PARTFUN1:def 4;
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 } ) by TARSKI:def 3;
dom x = dom ((SORTS A) * (the_arity_of o)) by A2, CARD_3:18
.= dom (the_arity_of o) by A3, RELAT_1:46 ;
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: