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
set ;
PBOOLE:def 18 ( 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
set ;
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 of
S st
(
U0 = A . i &
(Carrier A,s9) . i = the
Sorts of
U0 . s9 ) )
by PARTFUN1:def 4, PRALG_2:def 16;
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
set such that A5:
x1 in dom (proj (Carrier A,s9),i)
and A6:
y = (proj (Carrier A,s9),i) . x1
by FUNCT_1:def 5;
A7:
x1 in product (Carrier A,s9)
by A5, CARD_3:def 17;
then reconsider x1 =
x1 as
Function ;
y = x1 . i
by A5, A6, CARD_3:def 17;
hence
y in the
Sorts of
(A . i) . s
by A7, A4, CARD_3:18;
verum
end;
dom F9 =
dom (proj (Carrier A,s9),i)
by A1
.=
product (Carrier A,s9)
by CARD_3:def 17
.=
the
Sorts of
(product A) . s
by PRALG_2:def 17
;
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:11;
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