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 f being Function st f in dom (Frege (A ?. o)) holds
( dom f = I & ( for i being Element of I holds f . i in Args (o,(A . i)) ) & rng f c= Funcs ((dom (the_arity_of o)),|.A.|) )
let S be non empty non void ManySortedSign ; for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for f being Function st f in dom (Frege (A ?. o)) holds
( dom f = I & ( for i being Element of I holds f . i in Args (o,(A . i)) ) & rng f c= Funcs ((dom (the_arity_of o)),|.A.|) )
let A be MSAlgebra-Family of I,S; for o being OperSymbol of S
for f being Function st f in dom (Frege (A ?. o)) holds
( dom f = I & ( for i being Element of I holds f . i in Args (o,(A . i)) ) & rng f c= Funcs ((dom (the_arity_of o)),|.A.|) )
let o be OperSymbol of S; for f being Function st f in dom (Frege (A ?. o)) holds
( dom f = I & ( for i being Element of I holds f . i in Args (o,(A . i)) ) & rng f c= Funcs ((dom (the_arity_of o)),|.A.|) )
let f be Function; ( f in dom (Frege (A ?. o)) implies ( dom f = I & ( for i being Element of I holds f . i in Args (o,(A . i)) ) & rng f c= Funcs ((dom (the_arity_of o)),|.A.|) ) )
assume A1:
f in dom (Frege (A ?. o))
; ( dom f = I & ( for i being Element of I holds f . i in Args (o,(A . i)) ) & rng f c= Funcs ((dom (the_arity_of o)),|.A.|) )
A2:
dom (A ?. o) = I
by PARTFUN1:def 2;
A3:
dom (Frege (A ?. o)) = product (doms (A ?. o))
by PARTFUN1:def 2;
A4:
dom (doms (A ?. o)) = dom (A ?. o)
by FUNCT_6:def 2;
hence
dom f = I
by A1, A3, A2, CARD_3:9; ( ( for i being Element of I holds f . i in Args (o,(A . i)) ) & rng f c= Funcs ((dom (the_arity_of o)),|.A.|) )
thus A5:
for i being Element of I holds f . i in Args (o,(A . i))
rng f c= Funcs ((dom (the_arity_of o)),|.A.|)proof
let i be
Element of
I;
f . i in Args (o,(A . i))
(
(A ?. o) . i = Den (
o,
(A . i)) &
f . i in (doms (A ?. o)) . i )
by A1, A3, A2, A4, Th7, CARD_3:9;
then
f . i in dom (Den (o,(A . i)))
by A2, FUNCT_6:22;
hence
f . i in Args (
o,
(A . i))
by FUNCT_2:def 1;
verum
end;
let x be object ; TARSKI:def 3 ( not x in rng f or x in Funcs ((dom (the_arity_of o)),|.A.|) )
assume
x in rng f
; x in Funcs ((dom (the_arity_of o)),|.A.|)
then consider y being object such that
A6:
y in dom f
and
A7:
x = f . y
by FUNCT_1:def 3;
reconsider y = y as Element of I by A1, A3, A2, A4, A6, CARD_3:9;
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;
A8:
dom the Arity of S = the carrier' of S
by FUNCT_2:def 1;
then A9:
dom (( the Sorts of (A . y) #) * the Arity of S) = dom the Arity of S
by PARTFUN1:def 2;
A10: Args (o,(A . y)) =
(( the Sorts of (A . y) #) * the Arity of S) . o
by MSUALG_1:def 4
.=
( the Sorts of (A . y) #) . ( the Arity of S . o)
by A8, A9, FUNCT_1:12
.=
( the Sorts of (A . y) #) . (the_arity_of o)
by MSUALG_1:def 1
.=
product ( the Sorts of (A . y) * (the_arity_of o))
by FINSEQ_2:def 5
;
x in Args (o,(A . y))
by A5, A7;
then consider g being Function such that
A11:
g = x
and
A12:
dom g = dom ( the Sorts of (A . y) * (the_arity_of o))
and
A13:
for i being object 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;
A14:
( rng (the_arity_of o) c= the carrier of S & dom the Sorts of (A . y) = the carrier of S )
by FINSEQ_1:def 4, PARTFUN1:def 2;
then A15:
dom ( the Sorts of (A . y) * (the_arity_of o)) = dom (the_arity_of o)
by RELAT_1:27;
A16:
rng g c= |.(A . y).|
proof
let i be
object ;
TARSKI:def 3 ( not i in rng g or i in |.(A . y).| )
assume
i in rng g
;
i in |.(A . y).|
then consider j being
object such that A17:
j in dom g
and A18:
g . j = i
by FUNCT_1:def 3;
(the_arity_of o) . j in rng (the_arity_of o)
by A12, A15, A17, FUNCT_1:def 3;
then A19:
the
Sorts of
(A . y) . ((the_arity_of o) . j) in rng the
Sorts of
(A . y)
by A14, FUNCT_1:def 3;
i in ( the Sorts of (A . y) * (the_arity_of o)) . j
by A12, A13, A17, A18;
then
i in the
Sorts of
(A . y) . ((the_arity_of o) . j)
by A12, A17, FUNCT_1:12;
hence
i in |.(A . y).|
by A19, TARSKI:def 4;
verum
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:74;
then
rng g c= |.A.|
by A16;
hence
x in Funcs ((dom (the_arity_of o)),|.A.|)
by A11, A12, A15, FUNCT_2:def 2; verum