deffunc H1( Element of ) -> set = proj (Carrier A,$1),i;
consider F being ManySortedSet of the carrier of S such that
A1:
for s being Element of holds F . s = H1(s)
from PBOOLE:sch 5();
F is ManySortedFunction of ,(product A)
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 s' =
s as
Element of
by A2;
F . s = proj (Carrier A,s'),
i
by A1;
then reconsider F' =
F . s as
Function ;
A3:
rng F' c= the
Sorts of
(A . i) . s
proof
let y be
set ;
TARSKI:def 3 ( not y in rng F' or y in the Sorts of (A . i) . s )
A4:
(
dom (Carrier A,s') = I & ex
U0 being
MSAlgebra of
S st
(
U0 = A . i &
(Carrier A,s') . i = the
Sorts of
U0 . s' ) )
by PARTFUN1:def 4, PRALG_2:def 16;
assume
y in rng F'
;
y in the Sorts of (A . i) . s
then
y in rng (proj (Carrier A,s'),i)
by A1;
then consider x1 being
set such that A5:
x1 in dom (proj (Carrier A,s'),i)
and A6:
y = (proj (Carrier A,s'),i) . x1
by FUNCT_1:def 5;
A7:
x1 in product (Carrier A,s')
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 F' =
dom (proj (Carrier A,s'),i)
by A1
.=
product (Carrier A,s')
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 F' = F as ManySortedFunction of ,(product A) ;
take
F'
; for s being Element of holds F' . s = proj (Carrier A,s),i
thus
for s being Element of holds F' . s = proj (Carrier A,s),i
by A1; verum