defpred S1[ object , object ] means for o being OperSymbol of S st $1 = o holds
$2 = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o))));
set X = the carrier' of S;
set AS = ((SORTS A) #) * the Arity of S;
set RS = (SORTS A) * the ResultSort of S;
A1:
for x being object st x in the carrier' of S holds
ex y being object st S1[x,y]
proof
let x be
object ;
( x in the carrier' of S implies ex y being object st S1[x,y] )
assume
x in the
carrier' of
S
;
ex y being object st S1[x,y]
then reconsider o =
x as
OperSymbol of
S ;
take
IFEQ (
(the_arity_of o),
{},
(commute (A ?. o)),
(Commute (Frege (A ?. o))))
;
S1[x, IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o))))]
let o1 be
OperSymbol of
S;
( x = o1 implies IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) = IFEQ ((the_arity_of o1),{},(commute (A ?. o1)),(Commute (Frege (A ?. o1)))) )
assume
x = o1
;
IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) = IFEQ ((the_arity_of o1),{},(commute (A ?. o1)),(Commute (Frege (A ?. o1))))
hence
IFEQ (
(the_arity_of o),
{},
(commute (A ?. o)),
(Commute (Frege (A ?. o))))
= IFEQ (
(the_arity_of o1),
{},
(commute (A ?. o1)),
(Commute (Frege (A ?. o1))))
;
verum
end;
consider f being Function such that
A2:
( dom f = the carrier' of S & ( for x being object st x in the carrier' of S holds
S1[x,f . x] ) )
from CLASSES1:sch 1(A1);
reconsider f = f as ManySortedSet of the carrier' of S by A2, PARTFUN1:def 2, RELAT_1:def 18;
for x being object st x in dom f holds
f . x is Function
then reconsider f = f as ManySortedFunction of the carrier' of S by FUNCOP_1:def 6;
hereby ( not I <> {} implies ex b1 being ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S st verum )
assume
I <> {}
;
ex f being ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S st
for o being OperSymbol of S holds f . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o))))then reconsider I9 =
I as non
empty set ;
reconsider A9 =
A as
MSAlgebra-Family of
I9,
S ;
for
x being
object st
x in the
carrier' of
S holds
f . x is
Function of
((((SORTS A) #) * the Arity of S) . x),
(((SORTS A) * the ResultSort of S) . x)
proof
let x be
object ;
( x in the carrier' of S implies f . x is Function of ((((SORTS A) #) * the Arity of S) . x),(((SORTS A) * the ResultSort of S) . x) )
assume
x in the
carrier' of
S
;
f . x is Function of ((((SORTS A) #) * the Arity of S) . x),(((SORTS A) * the ResultSort of S) . x)
then reconsider o =
x as
OperSymbol of
S ;
set ar =
the_arity_of o;
set C =
Commute (Frege (A ?. o));
set F =
Frege (A ?. o);
set Ar = the
Arity of
S;
set Rs = the
ResultSort of
S;
set Cr = the
carrier of
S;
set co =
commute (A ?. o);
A5:
rng (the_arity_of o) c= the
carrier of
S
by FINSEQ_1:def 4;
A6:
dom the
Arity of
S = the
carrier' of
S
by FUNCT_2:def 1;
then
dom (((SORTS A) #) * the Arity of S) = dom the
Arity of
S
by PARTFUN1:def 2;
then A7:
(((SORTS A) #) * the Arity of S) . o =
((SORTS A) #) . ( the Arity of S . o)
by A6, FUNCT_1:12
.=
((SORTS A) #) . (the_arity_of o)
by MSUALG_1:def 1
.=
product ((SORTS A) * (the_arity_of o))
by FINSEQ_2:def 5
;
A8:
dom the
ResultSort of
S = the
carrier' of
S
by FUNCT_2:def 1;
then
dom ((SORTS A) * the ResultSort of S) = dom the
ResultSort of
S
by PARTFUN1:def 2;
then A9:
((SORTS A) * the ResultSort of S) . o =
(SORTS A) . ( the ResultSort of S . o)
by A8, FUNCT_1:12
.=
(SORTS A) . (the_result_sort_of o)
by MSUALG_1:def 2
.=
product (Carrier (A,(the_result_sort_of o)))
by Def10
;
dom (SORTS A) = the
carrier of
S
by PARTFUN1:def 2;
then A10:
dom ((SORTS A) * (the_arity_of o)) = dom (the_arity_of o)
by A5, RELAT_1:27;
per cases
( the_arity_of o = {} or the_arity_of o <> {} )
;
suppose A11:
the_arity_of o = {}
;
f . x is Function of ((((SORTS A) #) * the Arity of S) . x),(((SORTS A) * the ResultSort of S) . x)set rs =
the_result_sort_of o;
A12:
rng (A ?. o) c= Funcs (
{{}},
|.A9.|)
proof
let j be
object ;
TARSKI:def 3 ( not j in rng (A ?. o) or j in Funcs ({{}},|.A9.|) )
assume
j in rng (A ?. o)
;
j in Funcs ({{}},|.A9.|)
then consider a being
object such that A13:
a in dom (A ?. o)
and A14:
(A ?. o) . a = j
by FUNCT_1:def 3;
reconsider i =
a as
Element of
I9 by A13, PARTFUN1:def 2;
set So = the
Sorts of
(A9 . i);
|.(A9 . i).| in { |.(A9 . d).| where d is Element of I9 : verum }
;
then A15:
|.(A9 . i).| c= union { |.(A9 . d).| where d is Element of I9 : verum }
by ZFMISC_1:74;
dom the
Sorts of
(A9 . i) = the
carrier of
S
by PARTFUN1:def 2;
then
the
Sorts of
(A9 . i) . (the_result_sort_of o) in rng the
Sorts of
(A9 . i)
by FUNCT_1:def 3;
then A16:
the
Sorts of
(A9 . i) . (the_result_sort_of o) c= union (rng the Sorts of (A9 . i))
by ZFMISC_1:74;
(
rng (Den (o,(A9 . i))) c= Result (
o,
(A9 . i)) &
Result (
o,
(A9 . i))
= the
Sorts of
(A9 . i) . (the_result_sort_of o) )
by Th3, RELAT_1:def 19;
then A17:
rng (Den (o,(A9 . i))) c= |.A9.|
by A15, A16;
A18:
(
dom (Den (o,(A9 . i))) = Args (
o,
(A9 . i)) &
Args (
o,
(A9 . i))
= {{}} )
by A11, Th4, FUNCT_2:def 1;
j = Den (
o,
(A9 . i))
by A14, Th7;
hence
j in Funcs (
{{}},
|.A9.|)
by A18, A17, FUNCT_2:def 2;
verum
end;
dom (A ?. o) = I
by PARTFUN1:def 2;
then A19:
A ?. o in Funcs (
I,
(Funcs ({{}},|.A9.|)))
by A12, FUNCT_2:def 2;
then
commute (A ?. o) in Funcs (
{{}},
(Funcs (I,|.A9.|)))
by FUNCT_6:55;
then A20:
ex
h being
Function st
(
h = commute (A ?. o) &
dom h = {{}} &
rng h c= Funcs (
I,
|.A9.|) )
by FUNCT_2:def 2;
A21:
rng (commute (A ?. o)) c= ((SORTS A) * the ResultSort of S) . o
proof
let j be
object ;
TARSKI:def 3 ( not j in rng (commute (A ?. o)) or j in ((SORTS A) * the ResultSort of S) . o )
A22:
dom (Carrier (A,(the_result_sort_of o))) = I
by PARTFUN1:def 2;
assume A23:
j in rng (commute (A ?. o))
;
j in ((SORTS A) * the ResultSort of S) . o
then consider a being
object such that A24:
a in dom (commute (A ?. o))
and A25:
(commute (A ?. o)) . a = j
by FUNCT_1:def 3;
reconsider h =
j as
Function by A25;
A26:
for
b being
object st
b in dom (Carrier (A,(the_result_sort_of o))) holds
h . b in (Carrier (A,(the_result_sort_of o))) . b
proof
let b be
object ;
( b in dom (Carrier (A,(the_result_sort_of o))) implies h . b in (Carrier (A,(the_result_sort_of o))) . b )
assume
b in dom (Carrier (A,(the_result_sort_of o)))
;
h . b in (Carrier (A,(the_result_sort_of o))) . b
then reconsider i =
b as
Element of
I9 by PARTFUN1:def 2;
A27:
ex
U0 being
MSAlgebra over
S st
(
U0 = A . i &
(Carrier (A,(the_result_sort_of o))) . i = the
Sorts of
U0 . (the_result_sort_of o) )
by Def9;
dom (Den (o,(A9 . i))) =
Args (
o,
(A9 . i))
by FUNCT_2:def 1
.=
{{}}
by A11, Th4
;
then A28:
(Den (o,(A9 . i))) . a in rng (Den (o,(A9 . i)))
by A20, A24, FUNCT_1:def 3;
(A ?. o) . i = Den (
o,
(A9 . i))
by Th7;
then A29:
(Den (o,(A9 . i))) . a = h . i
by A19, A20, A24, A25, FUNCT_6:56;
rng (Den (o,(A9 . i))) c= Result (
o,
(A9 . i))
by RELAT_1:def 19;
then
h . i in Result (
o,
(A9 . i))
by A29, A28;
hence
h . b in (Carrier (A,(the_result_sort_of o))) . b
by A27, Th3;
verum
end;
ex
k being
Function st
(
k = h &
dom k = I &
rng k c= |.A9.| )
by A20, A23, FUNCT_2:def 2;
hence
j in ((SORTS A) * the ResultSort of S) . o
by A9, A22, A26, CARD_3:9;
verum
end; A30:
(((SORTS A) #) * the Arity of S) . o = {{}}
by A7, A11, CARD_3:10;
f . x =
IFEQ (
(the_arity_of o),
{},
(commute (A ?. o)),
(Commute (Frege (A ?. o))))
by A2
.=
commute (A ?. o)
by A11, FUNCOP_1:def 8
;
hence
f . x is
Function of
((((SORTS A) #) * the Arity of S) . x),
(((SORTS A) * the ResultSort of S) . x)
by A30, A20, A21, FUNCT_2:2;
verum end; suppose A31:
the_arity_of o <> {}
;
f . x is Function of ((((SORTS A) #) * the Arity of S) . x),(((SORTS A) * the ResultSort of S) . x)A32:
dom (Commute (Frege (A ?. o))) = (((SORTS A) #) * the Arity of S) . o
proof
thus
dom (Commute (Frege (A ?. o))) c= (((SORTS A) #) * the Arity of S) . o
XBOOLE_0:def 10 (((SORTS A) #) * the Arity of S) . o c= dom (Commute (Frege (A ?. o)))proof
let j be
object ;
TARSKI:def 3 ( not j in dom (Commute (Frege (A ?. o))) or j in (((SORTS A) #) * the Arity of S) . o )
assume
j in dom (Commute (Frege (A ?. o)))
;
j in (((SORTS A) #) * the Arity of S) . o
then consider g being
Function such that A33:
g in dom (Frege (A ?. o))
and A34:
j = commute g
by Def1;
set cg =
commute g;
A35:
rng g c= Funcs (
(dom (the_arity_of o)),
|.A9.|)
by A33, Th10;
A36:
dom g = I9
by A33, Th10;
then A37:
g in Funcs (
I,
(Funcs ((dom (the_arity_of o)),|.A9.|)))
by A35, FUNCT_2:def 2;
then
commute g in Funcs (
(dom (the_arity_of o)),
(Funcs (I,|.A9.|)))
by A31, FUNCT_6:55;
then A38:
ex
h being
Function st
(
h = commute g &
dom h = dom (the_arity_of o) &
rng h c= Funcs (
I,
|.A9.|) )
by FUNCT_2:def 2;
for
y being
object st
y in dom ((SORTS A) * (the_arity_of o)) holds
(commute g) . y in ((SORTS A) * (the_arity_of o)) . y
proof
let y be
object ;
( y in dom ((SORTS A) * (the_arity_of o)) implies (commute g) . y in ((SORTS A) * (the_arity_of o)) . y )
assume A39:
y in dom ((SORTS A) * (the_arity_of o))
;
(commute g) . y in ((SORTS A) * (the_arity_of o)) . y
then
(the_arity_of o) . y in rng (the_arity_of o)
by A10, FUNCT_1:def 3;
then reconsider s =
(the_arity_of o) . y as
SortSymbol of
S by A5;
(commute g) . y in rng (commute g)
by A10, A38, A39, FUNCT_1:def 3;
then consider h being
Function such that A40:
h = (commute g) . y
and A41:
dom h = I
and
rng h c= |.A9.|
by A38, FUNCT_2:def 2;
A42:
for
z being
object st
z in dom (Carrier (A,s)) holds
h . z in (Carrier (A,s)) . z
proof
let z be
object ;
( z in dom (Carrier (A,s)) implies h . z in (Carrier (A,s)) . z )
assume
z in dom (Carrier (A,s))
;
h . z in (Carrier (A,s)) . z
then reconsider i =
z as
Element of
I9 by PARTFUN1:def 2;
A43:
dom (( the Sorts of (A9 . i) #) * the Arity of S) = the
carrier' of
S
by PARTFUN1:def 2;
A44:
Args (
o,
(A9 . i)) =
(( the Sorts of (A9 . i) #) * the Arity of S) . o
by MSUALG_1:def 4
.=
( the Sorts of (A9 . i) #) . ( the Arity of S . o)
by A43, FUNCT_1:12
.=
( the Sorts of (A9 . i) #) . (the_arity_of o)
by MSUALG_1:def 1
.=
product ( the Sorts of (A9 . i) * (the_arity_of o))
by FINSEQ_2:def 5
;
g . i in rng g
by A36, FUNCT_1:def 3;
then consider f being
Function such that A45:
f = g . i
and
dom f = dom (the_arity_of o)
and
rng f c= |.A9.|
by A35, FUNCT_2:def 2;
A46:
ex
U0 being
MSAlgebra over
S st
(
U0 = A . i &
(Carrier (A,s)) . i = the
Sorts of
U0 . s )
by Def9;
dom the
Sorts of
(A9 . i) = the
carrier of
S
by PARTFUN1:def 2;
then A47:
dom ( the Sorts of (A9 . i) * (the_arity_of o)) = dom (the_arity_of o)
by A5, RELAT_1:27;
then A48:
( the Sorts of (A9 . i) * (the_arity_of o)) . y = the
Sorts of
(A9 . i) . s
by A10, A39, FUNCT_1:12;
g . i in Args (
o,
(A9 . i))
by A33, Th10;
then
f . y in ( the Sorts of (A9 . i) * (the_arity_of o)) . y
by A10, A39, A45, A44, A47, CARD_3:9;
hence
h . z in (Carrier (A,s)) . z
by A10, A37, A39, A40, A46, A45, A48, FUNCT_6:56;
verum
end;
A49:
dom (Carrier (A,s)) = I
by PARTFUN1:def 2;
((SORTS A) * (the_arity_of o)) . y =
(SORTS A) . s
by A39, FUNCT_1:12
.=
product (Carrier (A,s))
by Def10
;
hence
(commute g) . y in ((SORTS A) * (the_arity_of o)) . y
by A49, A40, A41, A42, CARD_3:9;
verum
end;
hence
j in (((SORTS A) #) * the Arity of S) . o
by A7, A10, A34, A38, CARD_3:9;
verum
end;
let i be
object ;
TARSKI:def 3 ( not i in (((SORTS A) #) * the Arity of S) . o or i in dom (Commute (Frege (A ?. o))) )
assume
i in (((SORTS A) #) * the Arity of S) . o
;
i in dom (Commute (Frege (A ?. o)))
then consider g being
Function such that A50:
g = i
and A51:
dom g = dom ((SORTS A) * (the_arity_of o))
and A52:
for
x being
object st
x in dom ((SORTS A) * (the_arity_of o)) holds
g . x in ((SORTS A) * (the_arity_of o)) . x
by A7, CARD_3:def 5;
A53:
rng g c= Funcs (
I,
|.A9.|)
proof
let a be
object ;
TARSKI:def 3 ( not a in rng g or a in Funcs (I,|.A9.|) )
assume
a in rng g
;
a in Funcs (I,|.A9.|)
then consider b being
object such that A54:
b in dom g
and A55:
g . b = a
by FUNCT_1:def 3;
(the_arity_of o) . b in rng (the_arity_of o)
by A10, A51, A54, FUNCT_1:def 3;
then reconsider cr =
(the_arity_of o) . b as
SortSymbol of
S by A5;
A56:
((SORTS A) * (the_arity_of o)) . b =
(SORTS A) . cr
by A51, A54, FUNCT_1:12
.=
product (Carrier (A,cr))
by Def10
;
a in ((SORTS A) * (the_arity_of o)) . b
by A51, A52, A54, A55;
then consider h being
Function such that A57:
h = a
and A58:
dom h = dom (Carrier (A,cr))
and A59:
for
j being
object st
j in dom (Carrier (A,cr)) holds
h . j in (Carrier (A,cr)) . j
by A56, CARD_3:def 5;
A60:
rng h c= |.A9.|
proof
let j be
object ;
TARSKI:def 3 ( not j in rng h or j in |.A9.| )
assume
j in rng h
;
j in |.A9.|
then consider c being
object such that A61:
c in dom h
and A62:
h . c = j
by FUNCT_1:def 3;
reconsider i =
c as
Element of
I9 by A58, A61, PARTFUN1:def 2;
( ex
U0 being
MSAlgebra over
S st
(
U0 = A . i &
(Carrier (A,cr)) . i = the
Sorts of
U0 . cr ) &
dom the
Sorts of
(A9 . i) = the
carrier of
S )
by Def9, PARTFUN1:def 2;
then A63:
(Carrier (A,cr)) . i in rng the
Sorts of
(A9 . i)
by FUNCT_1:def 3;
h . i in (Carrier (A,cr)) . i
by A58, A59, A61;
then A64:
h . i in |.(A9 . i).|
by A63, TARSKI:def 4;
|.(A9 . i).| in { |.(A9 . d).| where d is Element of I9 : verum }
;
hence
j in |.A9.|
by A62, A64, TARSKI:def 4;
verum
end;
dom (Carrier (A,cr)) = I
by PARTFUN1:def 2;
hence
a in Funcs (
I,
|.A9.|)
by A57, A58, A60, FUNCT_2:def 2;
verum
end;
then A65:
g in Funcs (
(dom (the_arity_of o)),
(Funcs (I,|.A9.|)))
by A10, A51, FUNCT_2:def 2;
then A66:
commute (commute g) = g
by A31, FUNCT_6:57;
commute g in Funcs (
I,
(Funcs ((dom (the_arity_of o)),|.A9.|)))
by A31, A65, FUNCT_6:55;
then A67:
ex
h being
Function st
(
h = commute g &
dom h = I &
rng h c= Funcs (
(dom (the_arity_of o)),
|.A9.|) )
by FUNCT_2:def 2;
A68:
for
j being
object st
j in dom (doms (A ?. o)) holds
(commute g) . j in (doms (A ?. o)) . j
proof
set cg =
commute g;
let j be
object ;
( j in dom (doms (A ?. o)) implies (commute g) . j in (doms (A ?. o)) . j )
assume
j in dom (doms (A ?. o))
;
(commute g) . j in (doms (A ?. o)) . j
then reconsider ii =
j as
Element of
I9 by Th11;
set So = the
Sorts of
(A9 . ii);
reconsider h =
(commute g) . ii as
Function ;
h in rng (commute g)
by A67, FUNCT_1:def 3;
then A69:
ex
s being
Function st
(
s = h &
dom s = dom (the_arity_of o) &
rng s c= |.A9.| )
by A67, FUNCT_2:def 2;
A70:
dom ( the Sorts of (A9 . ii) * (the_arity_of o)) = dom (the_arity_of o)
by Th3;
A71:
for
a being
object st
a in dom ( the Sorts of (A9 . ii) * (the_arity_of o)) holds
h . a in ( the Sorts of (A9 . ii) * (the_arity_of o)) . a
proof
let a be
object ;
( a in dom ( the Sorts of (A9 . ii) * (the_arity_of o)) implies h . a in ( the Sorts of (A9 . ii) * (the_arity_of o)) . a )
assume A72:
a in dom ( the Sorts of (A9 . ii) * (the_arity_of o))
;
h . a in ( the Sorts of (A9 . ii) * (the_arity_of o)) . a
then
(the_arity_of o) . a in rng (the_arity_of o)
by A70, FUNCT_1:def 3;
then reconsider s =
(the_arity_of o) . a as
SortSymbol of
S by A5;
A73:
( the Sorts of (A9 . ii) * (the_arity_of o)) . a = the
Sorts of
(A9 . ii) . s
by A72, FUNCT_1:12;
g . a in rng g
by A10, A51, A70, A72, FUNCT_1:def 3;
then consider k being
Function such that A74:
k = g . a
and
dom k = I
and
rng k c= |.A9.|
by A53, FUNCT_2:def 2;
A75:
( ex
U0 being
MSAlgebra over
S st
(
U0 = A9 . ii &
(Carrier (A,s)) . ii = the
Sorts of
U0 . s ) &
dom (Carrier (A,s)) = I )
by Def9, PARTFUN1:def 2;
A76:
((SORTS A) * (the_arity_of o)) . a =
(SORTS A) . s
by A10, A70, A72, FUNCT_1:12
.=
product (Carrier (A,s))
by Def10
;
(
k . ii = h . a &
k in ((SORTS A) * (the_arity_of o)) . a )
by A10, A52, A65, A70, A72, A74, FUNCT_6:56;
hence
h . a in ( the Sorts of (A9 . ii) * (the_arity_of o)) . a
by A73, A76, A75, CARD_3:9;
verum
end;
(
(doms (A ?. o)) . ii = Args (
o,
(A9 . ii)) &
Args (
o,
(A9 . ii))
= product ( the Sorts of (A9 . ii) * (the_arity_of o)) )
by Th3, Th11;
hence
(commute g) . j in (doms (A ?. o)) . j
by A70, A69, A71, CARD_3:9;
verum
end;
(
dom (Frege (A ?. o)) = product (doms (A ?. o)) &
dom (doms (A ?. o)) = I9 )
by Th11, PARTFUN1:def 2;
then
commute g in dom (Frege (A ?. o))
by A67, A68, CARD_3:9;
hence
i in dom (Commute (Frege (A ?. o)))
by A50, A66, Def1;
verum
end; set rs =
the_result_sort_of o;
set CA =
Carrier (
A,
(the_result_sort_of o));
A77:
rng (Commute (Frege (A ?. o))) c= ((SORTS A) * the ResultSort of S) . o
proof
let x be
object ;
TARSKI:def 3 ( not x in rng (Commute (Frege (A ?. o))) or x in ((SORTS A) * the ResultSort of S) . o )
A78:
dom (Carrier (A,(the_result_sort_of o))) = I
by PARTFUN1:def 2;
assume
x in rng (Commute (Frege (A ?. o)))
;
x in ((SORTS A) * the ResultSort of S) . o
then consider g being
object such that A79:
g in dom (Commute (Frege (A ?. o)))
and A80:
(Commute (Frege (A ?. o))) . g = x
by FUNCT_1:def 3;
consider f being
Function such that A81:
f in dom (Frege (A ?. o))
and A82:
g = commute f
by A79, Def1;
reconsider g =
g as
Function by A82;
(
dom f = I9 &
rng f c= Funcs (
(dom (the_arity_of o)),
|.A9.|) )
by A81, Th10;
then
f in Funcs (
I,
(Funcs ((dom (the_arity_of o)),|.A9.|)))
by FUNCT_2:def 2;
then
commute g = f
by A31, A82, FUNCT_6:57;
then A83:
x = (Frege (A ?. o)) . f
by A79, A80, Def1;
then reconsider h =
x as
Function ;
A84:
(Frege (A ?. o)) . f in rng (Frege (A ?. o))
by A81, FUNCT_1:def 3;
A85:
for
j being
object st
j in dom (Carrier (A,(the_result_sort_of o))) holds
h . j in (Carrier (A,(the_result_sort_of o))) . j
proof
let j be
object ;
( j in dom (Carrier (A,(the_result_sort_of o))) implies h . j in (Carrier (A,(the_result_sort_of o))) . j )
assume
j in dom (Carrier (A,(the_result_sort_of o)))
;
h . j in (Carrier (A,(the_result_sort_of o))) . j
then reconsider i =
j as
Element of
I9 by PARTFUN1:def 2;
A86:
dom ( the Sorts of (A9 . i) * the ResultSort of S) = dom the
ResultSort of
S
by A8, PARTFUN1:def 2;
A87:
ex
U0 being
MSAlgebra over
S st
(
U0 = A9 . i &
(Carrier (A,(the_result_sort_of o))) . i = the
Sorts of
U0 . (the_result_sort_of o) )
by Def9;
Result (
o,
(A9 . i)) =
( the Sorts of (A9 . i) * the ResultSort of S) . o
by MSUALG_1:def 5
.=
the
Sorts of
(A9 . i) . ( the ResultSort of S . o)
by A8, A86, FUNCT_1:12
.=
(Carrier (A,(the_result_sort_of o))) . i
by A87, MSUALG_1:def 2
;
hence
h . j in (Carrier (A,(the_result_sort_of o))) . j
by A83, A84, Th9;
verum
end;
dom h = I9
by A83, A84, Th9;
hence
x in ((SORTS A) * the ResultSort of S) . o
by A9, A78, A85, CARD_3:9;
verum
end; f . x =
IFEQ (
(the_arity_of o),
{},
(commute (A ?. o)),
(Commute (Frege (A ?. o))))
by A2
.=
Commute (Frege (A ?. o))
by A31, FUNCOP_1:def 8
;
hence
f . x is
Function of
((((SORTS A) #) * the Arity of S) . x),
(((SORTS A) * the ResultSort of S) . x)
by A32, A77, FUNCT_2:2;
verum end;
end; then reconsider f =
f as
ManySortedFunction of
((SORTS A) #) * the
Arity of
S,
(SORTS A) * the
ResultSort of
S by PBOOLE:def 15;
take f =
f;
for o being OperSymbol of S holds f . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o))))let o be
OperSymbol of
S;
f . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o))))thus
f . o = IFEQ (
(the_arity_of o),
{},
(commute (A ?. o)),
(Commute (Frege (A ?. o))))
by A2;
verum
end;
assume
I = {}
; ex b1 being ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S st verum
set f = the ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S;
take
the ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S
; verum