deffunc H1( Element of S) -> set = proj ((Carrier (A,$1)),i);
consider F being ManySortedSet of the carrier of S such that
A1:
for s being Element of S holds F . s = H1(s)
from PBOOLE:sch 5();
F is ManySortedFunction of (product A),(A . i)
proof
let s be
object ;
PBOOLE:def 15 ( not s in the carrier of S or F . s is Element of K10(K11(( the Sorts of (product A) . s),( the Sorts of (A . i) . s))) )
assume A2:
s in the
carrier of
S
;
F . s is Element of K10(K11(( the Sorts of (product A) . s),( the Sorts of (A . i) . s)))
F . s is
Function of
( the Sorts of (product A) . s),
( the Sorts of (A . i) . s)
proof
reconsider s9 =
s as
Element of
S by A2;
F . s = proj (
(Carrier (A,s9)),
i)
by A1;
then reconsider F9 =
F . s as
Function ;
A3:
rng F9 c= the
Sorts of
(A . i) . s
proof
let y be
object ;
TARSKI:def 3 ( not y in rng F9 or y in the Sorts of (A . i) . s )
A4:
(
dom (Carrier (A,s9)) = I & ex
U0 being
MSAlgebra over
S st
(
U0 = A . i &
(Carrier (A,s9)) . i = the
Sorts of
U0 . s9 ) )
by PARTFUN1:def 2, PRALG_2:def 9;
assume
y in rng F9
;
y in the Sorts of (A . i) . s
then
y in rng (proj ((Carrier (A,s9)),i))
by A1;
then consider x1 being
object such that A5:
x1 in dom (proj ((Carrier (A,s9)),i))
and A6:
y = (proj ((Carrier (A,s9)),i)) . x1
by FUNCT_1:def 3;
A7:
x1 in product (Carrier (A,s9))
by A5;
then reconsider x1 =
x1 as
Function ;
y = x1 . i
by A5, A6, CARD_3:def 16;
hence
y in the
Sorts of
(A . i) . s
by A7, A4, CARD_3:9;
verum
end;
dom F9 =
dom (proj ((Carrier (A,s9)),i))
by A1
.=
product (Carrier (A,s9))
by CARD_3:def 16
.=
the
Sorts of
(product A) . s
by PRALG_2:def 10
;
hence
F . s is
Function of
( the Sorts of (product A) . s),
( the Sorts of (A . i) . s)
by A2, A3, FUNCT_2:def 1, RELSET_1:4;
verum
end;
hence
F . s is
Element of
K10(
K11(
( the Sorts of (product A) . s),
( the Sorts of (A . i) . s)))
;
verum
end;
then reconsider F9 = F as ManySortedFunction of (product A),(A . i) ;
take
F9
; for s being Element of S holds F9 . s = proj ((Carrier (A,s)),i)
thus
for s being Element of S holds F9 . s = proj ((Carrier (A,s)),i)
by A1; verum