deffunc H1( object ) -> set = pr1 (F . $1);
consider X being ManySortedSet of I such that
A1:
for i being object st i in I holds
X . i = H1(i)
from PBOOLE:sch 4();
X is ManySortedFunction of A,B
proof
let i be
object ;
PBOOLE:def 15 ( not i in I or X . i is Element of bool [:(A . i),(B . i):] )
assume A2:
i in I
;
X . i is Element of bool [:(A . i),(B . i):]
then reconsider Bi =
B . i as non
empty set ;
A3:
X . i = pr1 (F . i)
by A1, A2;
then reconsider Xi =
X . i as
Function ;
A4:
F . i is
Function of
(A . i),
([|B,C|] . i)
by A2, PBOOLE:def 15;
A5:
rng Xi c= Bi
proof
let q be
object ;
TARSKI:def 3 ( not q in rng Xi or q in Bi )
assume
q in rng Xi
;
q in Bi
then consider x being
object such that A6:
x in dom Xi
and A7:
Xi . x = q
by FUNCT_1:def 3;
x in dom (F . i)
by A3, A6, MCART_1:def 12;
then A8:
(
Xi . x = ((F . i) . x) `1 &
(F . i) . x in rng (F . i) )
by A3, FUNCT_1:def 3, MCART_1:def 12;
rng (F . i) c= [|B,C|] . i
by A4, RELAT_1:def 19;
then A9:
rng (F . i) c= [:(B . i),(C . i):]
by A2, PBOOLE:def 16;
assume
not
q in Bi
;
contradiction
hence
contradiction
by A7, A9, A8, MCART_1:10;
verum
end;
dom (F . i) = A . i
by A2, A4, FUNCT_2:def 1;
then
dom Xi = A . i
by A3, MCART_1:def 12;
hence
X . i is
Element of
bool [:(A . i),(B . i):]
by A5, FUNCT_2:def 1, RELSET_1:4;
verum
end;
then reconsider X = X as ManySortedFunction of A,B ;
take
X
; for i being set st i in I holds
X . i = pr1 (F . i)
thus
for i being set st i in I holds
X . i = pr1 (F . i)
by A1; verum