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 . i') . s') where i' is Element of I, s' is Element of the carrier of S : verum } ;
dom (SORTS A) = the carrier of S by PARTFUN1:def 4;
then A1: rng (the_arity_of o) c= dom (SORTS A) ;
x in Args o,(product A) ;
then A2: x in product (the Sorts of (product A) * (the_arity_of o)) by PRALG_2:10;
then A3: dom x = dom ((SORTS A) * (the_arity_of o)) by CARD_3:18
.= dom (the_arity_of o) by A1, RELAT_1:46 ;
consider x1 being Function such that
A4: x1 = x ;

let c be set ; :: thesis:
assume c in rng x1 ; :: thesis:
then consider n being set such that
A5: ( n in dom x1 & x1 . n = c ) by FUNCT_1:def 5;
A6: n in dom ((SORTS A) * (the_arity_of o)) by A2, A4, A5, CARD_3:18;
then n in dom (the_arity_of o) by A1, 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, A4, 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 & dom g = dom (Carrier A,s1) & ( for i' being set st i' in dom (Carrier A,s1) holds
g . i' in (Carrier A,s1) . i' ) ) by CARD_3:def 5;
A8: dom g = I by A7, PARTFUN1:def 4;

let c1 be set ; :: thesis:
assume c1 in rng g ; :: thesis:
then consider i1 being set such that
A9: ( i1 in dom g & g . i1 = c1 ) by FUNCT_1:def 5;
reconsider i1 = i1 as Element of I by A7, A9, PARTFUN1:def 4;
consider U0 being MSAlgebra of S such that
A10: ( U0 = A . i1 & (Carrier A,s1) . i1 = the Sorts of U0 . s1 ) by PRALG_2:def 16;
A11: g . i1 in the Sorts of (A . i1) . s1 by A7, A9, A10;
the Sorts of (A . i1) . s1 in { (the Sorts of (A . i') . s') where i' is Element of I, s' is Element of the carrier of S : verum } ;
hence c1 in union { (the Sorts of (A . i') . s') where i' is Element of I, s' is Element of the carrier of S : verum } by A9, A11, TARSKI:def 4; :: thesis:

end;

then rng g c= union { (the Sorts of (A . i') . s') where i' is Element of I, s' is Element of the carrier of S : verum } by TARSKI:def 3;
hence c in Funcs I,(union { (the Sorts of (A . i') . s') where i' is Element of I, s' is Element of the carrier of S : verum } ) by A5, A7, A8, FUNCT_2:def 2; :: thesis:

end;

then rng x1 c= Funcs I,(union { (the Sorts of (A . i') . s') where i' is Element of I, s' is Element of the carrier of S : verum } ) by TARSKI:def 3;
hence x in Funcs (dom (the_arity_of o)),(Funcs I,(union { (the Sorts of (A . i') . s') where i' is Element of I, s' is Element of the carrier of S : verum } )) by A3, A4, FUNCT_2:def 2; :: thesis: