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:
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 )
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'
;
:: 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 ;
y = x1 . i
by A5, A6, Def2;
hence
y in the
Sorts of
(A . i) . s
by A7, A4, CARD_3:18;
:: thesis: verum
end;
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
;
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;
:: 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