defpred S1[ object , object ] means ex v being Vertex of IIG st
( v = $1 & $2 in Constants (SCS,v) );
set SW = SortsWithConstants IIG;
A1:
now for i being object st i in SortsWithConstants IIG holds
ex y being object st S1[i,y]let i be
object ;
( i in SortsWithConstants IIG implies ex y being object st S1[i,y] )A2:
SortsWithConstants IIG = { v where v is SortSymbol of IIG : v is with_const_op }
by MSAFREE2:def 1;
assume A3:
i in SortsWithConstants IIG
;
ex y being object st S1[i,y]then reconsider x =
i as
Vertex of
IIG ;
consider v being
Vertex of
IIG such that A4:
v = x
and A5:
v is
with_const_op
by A3, A2;
consider o being
OperSymbol of
IIG such that A6:
the
Arity of
IIG . o = {}
and A7:
the
ResultSort of
IIG . o = v
by A5, MSUALG_2:def 1;
A8:
dom the
ResultSort of
IIG = the
carrier' of
IIG
by FUNCT_2:def 1;
set y = the
Element of
rng (Den (o,SCS));
Result (
o,
SCS) =
( the Sorts of SCS * the ResultSort of IIG) . o
by MSUALG_1:def 5
.=
the
Sorts of
SCS . ( the ResultSort of IIG . o)
by A8, FUNCT_1:13
;
then reconsider y9 = the
Element of
rng (Den (o,SCS)) as
Element of the
Sorts of
SCS . v by A7;
reconsider y = the
Element of
rng (Den (o,SCS)) as
object ;
take y =
y;
S1[i,y]
ex
A being non
empty set st
(
A = the
Sorts of
SCS . v &
Constants (
SCS,
v)
= { a where a is Element of A : ex o being OperSymbol of IIG st
( the Arity of IIG . o = {} & the ResultSort of IIG . o = v & a in rng (Den (o,SCS)) ) } )
by MSUALG_2:def 3;
then
y9 in Constants (
SCS,
x)
by A4, A6, A7;
hence
S1[
i,
y]
;
verum end;
consider f being ManySortedSet of SortsWithConstants IIG such that
A9:
for i being object st i in SortsWithConstants IIG holds
S1[i,f . i]
from PBOOLE:sch 3(A1);
take
f
; for x being Vertex of IIG st x in dom f holds
f . x in Constants (SCS,x)
let x be Vertex of IIG; ( x in dom f implies f . x in Constants (SCS,x) )
assume
x in dom f
; f . x in Constants (SCS,x)
then
x in SortsWithConstants IIG
;
then
S1[x,f . x]
by A9;
hence
f . x in Constants (SCS,x)
; verum