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