let I be non empty set ; for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for x being Element of Args (o,(product A)) holds 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 } ))))
let S be non empty non void ManySortedSign ; for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for x being Element of Args (o,(product A)) holds 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 } ))))
let A be MSAlgebra-Family of I,S; for o being OperSymbol of S
for x being Element of Args (o,(product A)) holds 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 } ))))
let o be OperSymbol of S; for x being Element of Args (o,(product A)) holds 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 } ))))
let x be Element of Args (o,(product A)); 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 } ))))
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 for c being object st c in rng x1 holds
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 } ))let c be
object ;
( c in rng x1 implies 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 } )) )assume
c in rng x1
;
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 } ))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 for c1 being object st c1 in rng g holds
c1 in union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } let c1 be
object ;
( c1 in rng g implies c1 in union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )assume
c1 in rng g
;
c1 in union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } 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;
verum 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;
verum 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; verum