deffunc H1( Element of S) -> Function = proj (Carrier A,$1),i;
consider F being ManySortedSet of 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 ;
:: according to PBOOLE:def 18 :: thesis: ( 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
;
:: thesis: 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
S by A2;
F . s = proj (Carrier A,s'),
i
by A1;
then reconsider F' =
F . s as
Function ;
A3:
not the
Sorts of
(A . i) . s is
empty
by A2;
A4:
dom F' =
dom (proj (Carrier A,s'),i)
by A1
.=
product (Carrier A,s')
by Def2
.=
the
Sorts of
(product A) . s
by PRALG_2:def 17
;
rng F' c= the
Sorts of
(A . i) . s
proof
let y be
set ;
:: according to TARSKI:def 3 :: thesis: ( not y in rng F' or y in the Sorts of (A . i) . s )
assume
y in rng F'
;
:: thesis: 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, Def2;
then reconsider x1 =
x1 as
Function ;
A8:
dom (Carrier A,s') = I
by PARTFUN1:def 4;
A9:
y = x1 . i
by A5, A6, Def2;
consider U0 being
MSAlgebra of
S such that A10:
(
U0 = A . i &
(Carrier A,s') . i = the
Sorts of
U0 . s' )
by PRALG_2:def 16;
thus
y in the
Sorts of
(A . i) . s
by A7, A8, A9, A10, CARD_3:18;
:: thesis: verum
end;
hence
F . s is
Function of
(the Sorts of (product A) . s),
(the Sorts of (A . i) . s)
by A3, A4, FUNCT_2:def 1, RELSET_1:11;
:: thesis: verum
end;
hence
F . s is
Element of
K10(
K11(
(the Sorts of (product A) . s),
(the Sorts of (A . i) . s)))
;
:: thesis: verum
end;
then reconsider F' = F as ManySortedFunction of (product A),(A . i) ;
take
F'
; :: thesis: for s being Element of S holds F' . s = proj (Carrier A,s),i
thus
for s being Element of S holds F' . s = proj (Carrier A,s),i
by A1; :: thesis: verum