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 4;
A3:
SubFuncs (rng (A ?. o)) = rng (A ?. o)
A5:
dom (Frege (A ?. o)) = product (doms (A ?. o))
by PARTFUN1:def 4;
A6: dom (doms (A ?. o)) =
(A ?. o) " (SubFuncs (rng (A ?. o)))
by FUNCT_6:def 2
.=
dom (A ?. o)
by A3, RELAT_1:169
;
hence
dom f = I
by A1, A5, A2, CARD_3:18; ( ( 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 A7:
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, A5, A2, A6, Th14, CARD_3:18;
then
f . i in dom (Den (o,(A . i)))
by A2, FUNCT_6:31;
hence
f . i in Args (
o,
(A . i))
by FUNCT_2:def 1;
verum
end;
let x be set ; 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 set such that
A8:
y in dom f
and
A9:
x = f . y
by FUNCT_1:def 5;
reconsider y = y as Element of I by A1, A5, A2, A6, A8, CARD_3:18;
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;
A10:
dom the Arity of S = the carrier' of S
by FUNCT_2:def 1;
then A11:
dom (( the Sorts of (A . y) #) * the Arity of S) = dom the Arity of S
by PARTFUN1:def 4;
A12: Args (o,(A . y)) =
(( the Sorts of (A . y) #) * the Arity of S) . o
by MSUALG_1:def 9
.=
( the Sorts of (A . y) #) . ( the Arity of S . o)
by A10, A11, FUNCT_1:22
.=
( the Sorts of (A . y) #) . (the_arity_of o)
by MSUALG_1:def 6
.=
product ( the Sorts of (A . y) * (the_arity_of o))
by PBOOLE:def 19
;
x in Args (o,(A . y))
by A7, A9;
then consider g being Function such that
A13:
g = x
and
A14:
dom g = dom ( the Sorts of (A . y) * (the_arity_of o))
and
A15:
for i being set 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 A12, CARD_3:def 5;
A16:
( 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 4;
then A17:
dom ( the Sorts of (A . y) * (the_arity_of o)) = dom (the_arity_of o)
by RELAT_1:46;
A18:
rng g c= |.(A . y).|
proof
let i be
set ;
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
set such that A19:
j in dom g
and A20:
g . j = i
by FUNCT_1:def 5;
(the_arity_of o) . j in rng (the_arity_of o)
by A14, A17, A19, FUNCT_1:def 5;
then A21:
the
Sorts of
(A . y) . ((the_arity_of o) . j) in rng the
Sorts of
(A . y)
by A16, FUNCT_1:def 5;
i in ( the Sorts of (A . y) * (the_arity_of o)) . j
by A14, A15, A19, A20;
then
i in the
Sorts of
(A . y) . ((the_arity_of o) . j)
by A14, A19, FUNCT_1:22;
hence
i in |.(A . y).|
by A21, 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:92;
then
rng g c= |.A.|
by A18, XBOOLE_1:1;
hence
x in Funcs ((dom (the_arity_of o)),|.A.|)
by A13, A14, A17, FUNCT_2:def 2; verum