deffunc H2( OperSymbol of S) -> set = product ((NForms R) * (the_arity_of $1));
deffunc H3( OperSymbol of S, Element of H2($1)) -> set = nf (((Den ($1,(Free (S,X)))) . $2),(R . (the_result_sort_of $1)));
consider f being ManySortedFunction of the carrier' of S such that
A1:
for o being OperSymbol of S holds
( dom (f . o) = H2(o) & ( for x being Element of H2(o) holds (f . o) . x = H3(o,x) ) )
from MSAFREE4:sch 7();
f is ManySortedFunction of ((NForms R) #) * the Arity of S,(NForms R) * the ResultSort of S
proof
let i be
object ;
PBOOLE:def 15 ( not i in the carrier' of S or f . i is Element of bool [:((((NForms R) #) * the Arity of S) . i),(((NForms R) * the ResultSort of S) . i):] )
assume
i in the
carrier' of
S
;
f . i is Element of bool [:((((NForms R) #) * the Arity of S) . i),(((NForms R) * the ResultSort of S) . i):]
then reconsider o =
i as
OperSymbol of
S ;
dom (f . o) = H2(
o)
by A1;
then A2:
dom (f . o) =
((NForms R) #) . (the_arity_of o)
by FINSEQ_2:def 5
.=
(((NForms R) #) * the Arity of S) . o
by FUNCT_2:15
;
rng (f . o) c= ((NForms R) * the ResultSort of S) . o
proof
let x be
object ;
TARSKI:def 3 ( not x in rng (f . o) or x in ((NForms R) * the ResultSort of S) . o )
assume
x in rng (f . o)
;
x in ((NForms R) * the ResultSort of S) . o
then consider y being
object such that A3:
(
y in dom (f . o) &
x = (f . o) . y )
by FUNCT_1:def 3;
reconsider y =
y as
Element of
H2(
o)
by A1, A3;
A4:
x = H3(
o,
y)
by A1, A3;
(NForms R) * (the_arity_of o) c= the
Sorts of
(Free (S,X)) * (the_arity_of o)
by Th15, PBOOLE:def 18;
then
product ((NForms R) * (the_arity_of o)) c= product ( the Sorts of (Free (S,X)) * (the_arity_of o))
by Th16;
then
product ((NForms R) * (the_arity_of o)) c= Args (
o,
(Free (S,X)))
by PRALG_2:3;
then
(Den (o,(Free (S,X)))) . y in Result (
o,
(Free (S,X)))
by FUNCT_2:5;
then reconsider a =
(Den (o,(Free (S,X)))) . y as
Element of
(Free (S,X)),
(the_result_sort_of o) by FUNCT_2:15;
nf (
a,
(R . (the_result_sort_of o)))
in { (nf (z,(R . (the_result_sort_of o)))) where z is Element of (Free (S,X)),(the_result_sort_of o) : verum }
;
then
nf (
a,
(R . (the_result_sort_of o)))
in (NForms R) . (the_result_sort_of o)
by Def19;
hence
x in ((NForms R) * the ResultSort of S) . o
by A4, FUNCT_2:15;
verum
end;
hence
f . i is
Function of
((((NForms R) #) * the Arity of S) . i),
(((NForms R) * the ResultSort of S) . i)
by A2, FUNCT_2:2;
verum
end;
then reconsider f = f as ManySortedFunction of ((NForms R) #) * the Arity of S,(NForms R) * the ResultSort of S ;
reconsider A = MSAlgebra(# (NForms R),f #) as strict non-empty MSAlgebra over S by MSUALG_1:def 3;
take
A
; ( the Sorts of A = NForms R & ( for o being OperSymbol of S
for a being Element of Args (o,A) holds (Den (o,A)) . a = nf (((Den (o,(Free (S,X)))) . a),(R . (the_result_sort_of o))) ) )
thus
the Sorts of A = NForms R
; for o being OperSymbol of S
for a being Element of Args (o,A) holds (Den (o,A)) . a = nf (((Den (o,(Free (S,X)))) . a),(R . (the_result_sort_of o)))
let o be OperSymbol of S; for a being Element of Args (o,A) holds (Den (o,A)) . a = nf (((Den (o,(Free (S,X)))) . a),(R . (the_result_sort_of o)))
let a be Element of Args (o,A); (Den (o,A)) . a = nf (((Den (o,(Free (S,X)))) . a),(R . (the_result_sort_of o)))
Args (o,A) = product ( the Sorts of A * (the_arity_of o))
by PRALG_2:3;
hence
(Den (o,A)) . a = nf (((Den (o,(Free (S,X)))) . a),(R . (the_result_sort_of o)))
by A1; verum